Petri net
From Free net encyclopedia
Msoos (Talk | contribs)
/* Basic mathematical properties */ reachability graph added
Next diff →
Current revision
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.
Image:Animated Petri net commons.gif
Contents |
Basic Petri nets
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:
- multiple transitions can be enabled at the same time, any one of which can fire
- none are required to fire - they fire at will, between time 0 and infinity, or not at all(!) i.e. it is totally possible that nothing fires at all.
Since firing is non-deterministic, Petri nets are well suited for modeling the concurrent behavior of distributed systems.
A Formal definition
A Petri net is a 6-tuple <math>(S,T,F,M_0,W,K)</math>, where (see Desel and Juhás Template:Ref)
- <math>S</math>, is a set of places.
- <math>T</math>, is a set of transitions.
- <math>F</math>, is a set of arcs known as a flow relation. The set <math>F</math> is subject to the constraint that no arc may connect two places or two transitions, or more formally: <math>F \subseteq (S \times T) \cup (T \times S)</math>.
- <math>M_0 : S \to \mathbb{N}</math> is an initial marking, where for each place <math>s \in S</math>, there are <math>n \in \mathbb{N}</math> tokens.
- <math>W : F \to \mathbb{N^+}</math> is a set of arc weights, which assigns to each arc <math>f \in F</math> some <math>n \in \mathbb{N^+}</math> denoting how many tokens are consumed from a place by a transition, or alternatively, how many tokens are produced by a transition and put into each place.
- <math>K : S \to \mathbb{N^+}</math> is a set of capacity restrictions, which assigns to each place <math>s \in S</math> some positive number <math>n \in \mathbb{N^+}</math> denoting the maximum number of tokens that can occupy that place.
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.
Basic mathematical properties
The state of a Petri net can be represented as an M vector, where the 1st value of the vector is the amount of tokens in the 1st place of the net, the 2nd is amount of tokens in the 2nd place, and so on. Such a representation fully describes the state of a Petri net.
A state-transition list, <math>\vec \sigma = \langle M_{i_0} t_{i_1} M_{i_1} \ldots t_{i_n} M_{i_n} \rangle</math>, which can be shortened to simply <math>\vec \sigma = \langle t_{i_1} \ldots t_{i_n} \rangle</math> 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 <math>\langle M_{i_0} M_{i_1} \ldots M_{i_n} \rangle</math> is called a trajectory, and <math>M_{i_n}</math> is called reachable from <math>M_{i_0}</math> through the firing sequence of <math>\vec \sigma</math>. Mathematically written: <math>M_{i_0} [ \vec \sigma > M_{i_n}</math>. All firing sequences that can be reached from a net <math>N</math> and an initial marking <math>M_{0}</math> are noted as <math>L(N,M_{0})</math>.
The state-transition matrix <math>W^-</math> is <math>|T|</math> by <math>|S|</math> large, and represents the amount of tokens taken by each transition from each place. Similarly, <math>W^+</math> represents the amount of tokens given by each transition to each place. The sum of the two, <math>W=W^+ - W^-</math> can be used for calculating the above mentioned equation of <math>M_{i_0} [ \vec \sigma > M_{i_n}</math> which can now be simply written as <math>M_0 - M_n = W^T \cdot \sigma</math>, where <math>\sigma</math> 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 <math>M_n</math> can be reached from state <math>M_0</math>.
Image:Detailed petri net.png <math>W^{+}=\begin{bmatrix} * & t1 & t2 \\ p1 & 0 & 1 \\ p2 & 1 & 0 \\ p3 & 1& 0 \\ p4 & 0 & 1 \end{bmatrix} </math> <math> W^{-}=\begin{bmatrix} * & t1 & t2 \\ p1 & 1 & 0 \\ p2 & 0 & 1 \\ p3 & 0 & 1 \\ p4 & 0 & 0 \end{bmatrix} </math> <math>W=\begin{bmatrix} * & t1 & t2 \\ p1 & -1 & 1 \\ p2 & 1 & -1 \\ p3 & 1 & -1 \\ p4 & 0 & 1 \end{bmatrix}</math> <math>M_{0}=\begin{bmatrix} 1 & 0 & 2 & 1 \end{bmatrix}</math>
All states that can be reached from a net <math>N</math> with an initial marking <math>M_{0}</math> are denoted as <math>R(N,M_{0})</math>. The reachability problem is then the following: is it true that <math>M_{w} \in R(N,M_{0})</math>? Where <math>M_{w}</math> is, e.g. a wrong state such as an elevator moving while the door is open.
Reachability
Image:Reachability graph for petri net.png
The reachability of the states can be represented with a reachability graph where a directed graph' points represent states (i.e. M), and arcs transitions between two such states. The graph is constructed as follows: the starting state (<math>M_0</math>) 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, the constructed graph has far too many states for practical problems. For these reasons, the LTL logic with tableau method is usually used to prove that such states cannot be reached. This logic 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 can not be satisfied.
Liveness
A Petri net (<math>N,M_0</math>)'s transition t is
- <math>L_0</math> live, or dead iff(=if and only if) it can not be fired, i.e. it is not in any <math>\vec \sigma \in L(N,M_0)</math>
- <math>L_1</math> live iff it can possibly be fired, i.e. it is in a firing sequence <math>\vec \sigma</math> where <math>\vec \sigma \in L(N,M_0)</math>
- <math>L_2</math> live iff for any k positive whole number, t can be fired at least k times in a firing sequence <math>\vec \sigma</math> where <math>\vec \sigma \in L(N,M_0)</math>
- <math>L_3</math> live iff there exists a firing sequence <math>\vec \sigma \in L(N,M_0)</math> where t is fired infinitely
- <math>L_4</math> live or simply live iff in any reachable state m(i.e. <math>\forall M \in R(N,M_0)</math>) t is <math>L_1</math> live
Note that these are increasingly stringent requirements such that if a transition is e.g. <math>L_3</math> live, is automatically <math>L_1</math> and <math>L_2</math> live as well. As an example, the example (b) Petri Net is live with the given inital state. Example (a) Petri net is actually live no matter what initial state is set.
A Petri net is <math>L_k</math> live iff every transition within it is <math>L_k</math> live.
Boundedness
There are Petri nets where the places are bounded for a maximum number of tokens - in this case, boundedness is an inherent property. However, Petri nets can be defined without the boundedness as an inherent property - in these cases, boundedness is a possible property of the Petri net. A non-inherently bounded Petri net is k-bounded if in no reachable state can at any place contain more than k tokens. A Petri net is safe if it is 1-bounded. Naturally, boundedness in this case is dependent on the initial <math>M_{0}</math> marking (i.e. we can put 10 tokens into each place initially, making it impossible that the net is 2-bounded). Also note that the inherently not bounded example (b) Petri net is not bounded as P4 can possess infinite amounts of tokens, if the firing sequence (T1,T2) is repeated infinitely. However, example (a) Petri net, which is inherently bounded to k=2 for all places, is shown at every possible state.
Image:Place transformation petri net.png 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 <math>M_{0}</math> 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 <math>M_{0}</math> 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).
Extensions
There are many extensions to Petri nets. Some of them are completely backwards-compatible (e.g. colored Petri nets) with the original Petri net, some add properties that cannot be modelled in the original Petri net (e.g. timed Petri nets). If they can be modelled in the original Petri net, they are not real extensions, instead are convenient ways of showing the same thing, and can be transformed with mathematical formulas back to the original Petri net, without losing any meaning. Extensions that cannot be transformed are sometimes very powerful, but usually lack the amount of mathematical tools available to analyze normal Petri nets.
The term high-level Petri net is used for many Petri net formalisms that extend the basic P/T net formalsism. This includes colored Petri nets, hierarchical Petri nets, and all other extensions sketched in this section.
A short list of possible extensions:
- In a standard Petri net, tokens are indistinguishable. In a coloured Petri net, every token has a value. In popular tools for coloured Petri nets such as CPN Tools, the values of tokens are typed, and can be tested and manipulated with a functional programming language. A subsidiary of coloured Petri nets are the well-formed Petri nets, where the arc and guard expressions are restricted to make it easier to analyise the net.
- Another popular extension of Petri nets is hierarchy: Hierarchy in the form of different views supporting levels of refinement and abstraction were studied by Fehling. Another form of hierarchy is found in so-called object Petri nets or object systems where a Petri net can contain Petri nets as its tokens inducing a hierarchy of nested Petri nets that communicate by synchronisation of transitions on different levels. See [1] for an informal introduction to object Petri nets.
- A Vector Addition System with States (VASS) can be seen as a generalization of a Petri net. Consider a finite state automaton where each transition is labeled by a transition from the Petri net. The Petri net is then synchronized with the finite state automaton, i.e., a transition in the automaton is taken at the same time as the corresponding transition in the Petri net. It is only possible to take a transition in the automaton if the corresponding transition in the Petri net is enabled, and it is only possible to fire a transition in the Petri net if there is a transition from the current state in the automaton labeled by it. (The definition of VASS is usually formulated slightly differently.)
- Prioritized Petri nets add priorities to transitions, whereby a transition cannot fire, if a higher-priority transition is enabled (i.e. can fire). Thus, transitions are in priority groups, and e.g. priority group 3 can only fire if all transitions are disabled in groups 1 and 2. Within a priority group, firing is still non-deterministic.
- The non-deterministic property has been a very valuable one, as it lets the user abstract a large number of properties (depending on what the net is used for). In certain cases, however, the need arises to also model the timing, not only the structure of a model. For these cases, timed Petri nets have evolved, where there are transitions that are timed, and possibly transitions which are not timed (if there are, transitions that are not timed have a higher priority than timed ones). This way, the property of time can also be modelled (not only the structure). A subsidiary of timed petri nets are the stochastic Petri nets that add non-deterministic time through adjustable randomness of the transitions. The exponential random distribution is usually used to 'time' these nets. In this case, the nets' reachability graph can be used as a markov chain.
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.
Petri net theory
The theoretical properties of Petri nets have been studied extensively.
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 [2] and in Kurt Jensen Coloured Petri Nets, and in M. Ajmone Marsan et al. Modelling with Generalized Stochastic Petri Nets.
Main Petri net types
Image:Petri net types.svg There are six main types of petri net:
- State Machine (SM) - here, every transition has one incoming arc, and one outgoing arc. This means, that there can not be concurrency, but there can be conflict (i.e. Where should the token from the place go? To one transition or the other?). Mathematically: <math>\forall t\in T: |t\bullet|=|\bullet t|=1</math>
- Marked Graph (MG) - here, every place has one incoming arc, and one outgoing arc. This means, that there can not be conflict, but there can be concurrency. Mathematically: <math>\forall p\in P: |p\bullet|=|\bullet p|=1</math>
- Free choice (FC) - here, an arc is either the only arc going from the place, or it is the only arc going to a transition. I.e. there can be both concurrency and conflict, but not at the same time. Mathematically: <math>\forall p\in P: (|p\bullet|\leq 1) \vee (\bullet (p\bullet)=\{p\})</math>
- Extended free choice (EFC) - a Petri net that can be transformed into an FC.
- Asymmetric choice (AC) - concurrecy and conflict (in sum, confusion), but not asymmetrically.Mathematically: <math>\forall p_1,p_2\in P: (p_1\bullet \cap p_2\bullet\neq 0) \to [(p_1\bullet\subseteq p_2\bullet) \vee (p_2\subseteq p_1\bullet)]</math>
- Petri Net (PN) - confusion is allowed (i.e. everything is allowed)
Subsequent models of concurrency
Subsequent to the invention of Petri nets other models of concurrency, which are based on message passing and feature compositionality (e.g. the Actor model and the various process calculi), have been introduced. Robin Milner and Carl Hewitt have argued that the lack of compositionality is a serious limitation of Petri nets because the deficiency limits modularity.
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.
Application areas
- Software design
- Workflow management
- Data analysis
- Concurrent programming
- Reliability engineering
- Diagnosis for finding the original error in the line of error -> error state -> visible error
Programming tools
See the list of Petri net tools.
See also
References
- {{cite book
| first = Janette | last = Cardoso | authorlink = Janette Cardoso | coauthors = Heloisa Camargo | year = | title = Fuzziness in Petri Nets | publisher = Physica-Verlag | id = ISBN 3-7908-1158-0
}}
- Template:NoteDesel, 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.
- {{cite book
| first = Kurt | last = Jensen | authorlink = Kurt Jensen | year = | title = Coloured Petri Nets | publisher = Springer Verlag | id = ISBN 3-540-62867-3
}}
- {{cite book
| first = James Lyle | last = Peterson | authorlink = James Lyle Peterson | year = | title = Petri Net Theory and the Modeling of Systems | publisher = Prentice Hall | id = ISBN 0136619835
}}
- {{cite book
| first = Wolfgang | last = Reisig | authorlink = Wolfgang Reisig | year = | title = A Primer in Petri Net Design | publisher = Springer-Verlag | id = ISBN 3-540-52044-9
}}
- {{cite book
| first = Robert-Christoph | last = Riemann | authorlink = Robert-Christoph Riemann | year = | title = Modelling of Concurrent Systems: Structural and Semantical Methods in the High Level Petri Net Calculus | publisher = Herbert Utz Verlag | id = ISBN 3-89675-629-X
}}
- {{cite book
| first = Harald | last = Störrle | authorlink = Harald Störrle | year = | title = Models of Software Architecture - Design and Analysis with UML and Petri-Nets | publisher = Books on Demand | id = ISBN 3-8311-1330-0
}}
- {{cite book
| first = Mengchu | last = Zhou | authorlink = Mengchu Zhou | coauthors = Frank Dicesare | year = | title = Petri Net Synthesis for Discrete Event Control of Manufacturing Systems | publisher = Kluwer Academic Publishers | id = ISBN 0792392892
}}
- {{cite book
| first = Mengchu | last = Zhou | authorlink = Mengchu Zhou | year = | title = Modeling, Simulation, & Control of Flexible Manufacturing Systems: A Petri Net Approach | publisher = World Scientific Publishing | id = ISBN 981023029X
}}
External links
- Petri Nets World
- Petri Net Markup Language
- exchangeable Routing Language
- Citations from CiteSeerde:Petri-Netz
es:Red de Petri fr:Réseau de Petri hu:Petri-háló nl:Petrinet pl:Sieć Petriego pt:Rede de Petri ro:Reţea Petri zh:Petri网