A Petri net (also known as a place/transition net or P/T net) is one of several mathematical representations of discrete distributed systems. As a modeling language, it graphically depicts the structure of a distributed system as a directed bipartite graph with annotations. As such, a Petri net has place nodes, transition nodes, and directed arcs connecting places with transitions. Petri nets were invented in 1962 by Carl Adam Petri in his PhD thesis.
A Petri net consists of places, transitions and directed arcs. Arcs run between places and transitions - not between places and places or transitions and transitions. The places from which an arc run to a transition are called the input places of the transition; the places to which arcs run from a transition are called the output places of the transition.
Places may contain any number of tokens. A distribution of tokens over the places of a net is called a marking. Transitions act on input tokens by a process known as firing. A transition is enabled if it can fire, i.e., there are tokens in every input place. When a transition fires, it consumes the tokens from its input places, performs some processing task, and places a specified number of tokens into each of its output places. It does this atomically, i.e. in one single non-preemptible step.
Execution of Petri nets is nondeterministic. This means two things:
A Petri net is a 6-tuple , where (see Desel and Juhás Desel, Jörg and Juhás, Gabriel "What Is a Petri Net? -- Informal Answers for the Informed Reader", Hartmut Ehrig et al. (Eds.): Unifying Petri Nets, LNCS 2128, pp. 1-25, 2001.)
A variety of other formal definitions exist. This definition is for a place-transition net. Most other definitions do not include arc weights or capacity restrictions.
A state-transition list, , which can be shortened to simply is called a firing sequence if each and every transition satisfies the firing criteria (i.e. there are enough tokens in the input for every transition). In this case, the state-transition list of is called a trajectory, and is called reachable from through the firing sequence of . Mathematically written: . All firing sequences that can be reached from a net and an initial marking are noted as .
The state-transition matrix is by large, and represents the amount of tokens taken by each transition from each place. Similarly, represents the amount of tokens given by each transition to each place. The sum of the two, can be used for calculating the above mentioned equation of which can now be simply written as , where is a vector of how many times each transition fired in the sequence. Note that just because the equation can be satisfied, does not mean that it can actually be carried out - for that there should be enough tokens for each transition to fire, i.e. the satisfiability of the equation is required but not sufficient to say that state can be reached from state .
All states that can be reached from a net with an initial marking are denoted as . The reachability problem is then the following: is it true that ? Where is, e.g. a wrong state such as an elevator moving while the door is open.
The reachability of the states can be represented with a reachability graph where a directed graph' points represent states (i.e. M), and arcs represent transitions between two such states. The graph is constructed as follows: the starting state () is taken, and all possible transitions are explored from this state, then the transitions from these states, and so on. The way the graph should be constructed is through breadth-first search, as the graph may be infinitely large, and so depth-first search would not find all possible states even if given infinite time. Note, that if the graph is inherently bounded, its reachability graph will always have a finite amount of states.
While reachability seems to a be a good tool to find erroneous states, such as an elevator moving while the door is open, for practical problems the constructed graph usually has far too many states to calculate. To alleviate this problem, the LTL logic is usually used in conjunction with the tableau method to prove that such states cannot be reached. LTL uses the semi-decision technique to find if indeed a state can be reached, by finding a set of necessary conditions for the state to be reached then proving that those conditions cannot be satisfied.
Note that these are increasingly stringent requirements such that if a transition is e.g. live, is automatically and live as well. As an example, (b) Example Petri net is live with the given inital state, but with a different (e.g. totally empty) initial state, all of its transitions can be dead. On the other hand, (a) Example Petri net's transitions are all live no matter what the initial state is - they are not live, since when the state is (0,2) or (2,0), one of its transitons can not be fired, since the net is 2-bounded.
A Petri net is live if and only if every transition within it is live.
Boundedness of a certain place in an inherently bounded net can be mimiced in an non-inherently bounded net by doing a place-transformation, where a new place (called counter-place) is made, and all transitions that put x tokens to the original place take x tokens from the counter-place, and all transitions that take away x tokens from the original place put x tokens to the counter-place. The number of tokens in must now satisfy the equation place+counter-place=boundedness. Thus, doing a place-transformation for all places in a bounded net, and restricting the starting state to conform to the above noted equality, a bounded net can easily be transformed to a non-bounded net. Therefore any analysis that is used on inherently non-bounded nets can be used on bounded nets (but not the other way around).
In general, inherent boundedness and other (non-)inherent properties are problematic not because they are hard to explain, but because there is no consensus in the mathematical community about what exactly should the definition of the Petri net be. In this article, boundedness is defined as an inherent property. In this section it has been shown that this property is not needed, as it can be circumvented. There are many such properties (e.g. colours).
The term high-level Petri net is used for many Petri net formalisms that extend the basic P/T net formalism. This includes colored Petri nets, hierarchical Petri nets, and all other extensions sketched in this section.
A short list of possible extensions:
There are many more extensions to Petri nets, however, it is important to keep in mind, that as the complexity of the net increases in terms of extended properties, the harder it is to use standard tools to evaluate certain properties of the net. For this reason, it is a good idea to use the most simple net type possible for a given modelling task.
The theoretical properties of Petri nets have been studied extensively. A main motivation for the use of Petri nets in concurrent systems modelling is the possibility to formally state and decide certain desirable system properties, such as liveness (e.g. the system can never lock up) and boundedness (e.g. loosely, system resources such as CPUs are bounded). Naturally, the same property in a different context might mean a different thing.
A marking of a Petri net is reachable if, starting in the initial marking, a sequence of transition firings exists that produces it. A Petri net is bounded if there is a maximum to the number of tokens in its reachable markings.
Boundedness is decidable by looking at covering, by constructing the Karp-Miller Tree. Reachability is known to be decidable, however in at least exponential time. All known general algorithms so far, however, employ non-primitive recursive space. Further details may be found in this survey and in Kurt Jensen Coloured Petri Nets, and in M. Ajmone Marsan et al. Modelling with Generalized Stochastic Petri Nets.
In addition, Hewitt has argued that Petri nets lack locality because input tokens of a transition disappear simultaneously, which limits the realism of the model. He acknowledged the counterargument that the proper use of Petri nets is to obey the single event restriction which is that every transition should model a single event. An example of such a transition would be one with two input places, one representing the month being September 2005, and the other representing the date being September 30, 2005. If the event being modeled were the passing of midnight on that day, obviously both tokens would disappear at the same time. However obeying the single event restriction drastically limits the applications of Petri nets.
See the list of Petri net tools.
Formal methods | Computational models | Specification languages | Concurrency | Diagrams
شبكات بيتري | Petri-Netz | Red de Petri | Réseau de Petri | Petri-háló | Petrinet | Sieć Petriego | Rede de Petri | Reţea Petri | Мережа Петрі | Petri网
This article is licensed under the GNU Free Documentation License.
It uses material from the
"Petri net".
Home Page • arts • business • computers • games • health • hospitals • home • kids & teens • news • physicians • recreation• reference • regional • science • shopping • society • sports • world