Citizendia
Your Ad Here

A Petri net (also known as a place/transition net or P/T net) is one of several mathematical representations of discrete distributed systems. Mathematics is the body of Knowledge and Academic discipline that studies such concepts as Quantity, Structure, Space and Knowledge representation is an area in Artificial intelligence that is concerned with how to formally "think" that is how to use a symbol system to represent Distributed computing deals with Hardware and Software Systems containing more than one processing element or Storage element concurrent As a modeling language, it graphically depicts the structure of a distributed system as a directed bipartite graph with annotations. A modeling language is any Artificial language that can be used to express Information or Knowledge or Systems in a Structure that In the mathematical field of Graph theory, a bipartite graph (or bigraph) is a graph whose vertices can be divided into two 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. Carl Adam Petri (born July 12 1926) is a German mathematician and computer scientist

(a) Petri net trajectory example
(a) Petri net trajectory example

Contents

Basic Petri nets

A Petri net consists of places, transitions, and directed arcs. In Mathematics and Computer science, graph theory is the study of graphs: mathematical structures used to model pairwise relations between objects Arcs run between places and transitions—not between places and places or transitions and transitions. The places from which an arc runs 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 non-interruptible step.

Execution of Petri nets is nondeterministic. This means two things:

  1. multiple transitions can be enabled at the same time, any one of which can fire
  2. 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 nondeterministic, Petri nets are well suited for modeling the concurrent behavior of distributed systems. In Computer science, concurrency is a properties of system in which several Computational processes are executing at the same time and potentially interacting

A formal definition

A Petri net is a 5-tuple (S,T,F,M_0,W)\!, where (see Desel and Juhás[1])

A variety of other formal definitions exist. Some definitions do not have arc weights, but they allow multiple arcs between the same place and transition, which is conceptually equal to one arc with a weight of more than one.

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 number of tokens in the 1st place of the net, the 2nd is the number of tokens in the 2nd place, and so on. Such a representation fully describes the state of a Petri net.

A state-transition list, \vec \sigma = \langle M_{i_0} t_{i_1} M_{i_1} \ldots t_{i_n} M_{i_n} \rangle, which can be shortened to simply \vec \sigma = \langle t_{i_1} \ldots t_{i_n} \rangle 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 \langle M_{i_0} M_{i_1} \ldots M_{i_n} \rangle is called a trajectory, and M_{i_n} is called reachable from M_{i_0} through the firing sequence of \vec \sigma. Mathematically written: M_{i_0} [ \vec \sigma > M_{i_n}. The set of all firing sequences that can be reached from a net N and an initial marking M0 are noted as L(N,M0).

The state-transition matrix W is | S | by | T | large, and represents the number of tokens taken by each transition from each place. Similarly, W + represents the number of tokens given by each transition to each place. The sum of the two, W = W +W can be used for calculating the above mentioned equation of M_{i_0} [ \vec \sigma > M_{i_n} which can now be simply written as M_0 - M_n = W^T \cdot \sigma, 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 Mn can be reached from state M0.

(b) Petri net Example
(b) Petri net Example

W^{+}=\begin{bmatrix} * & t1 & t2 \\ p1 & 0  & 1 \\ p2 & 1 & 0 \\ p3 & 1& 0 \\ p4 & 0 & 1 \end{bmatrix}

 W^{-}=\begin{bmatrix} * & t1 & t2 \\ p1 & 1  & 0 \\ p2 & 0 & 1 \\ p3 & 0 & 1 \\ p4 & 0 & 0 \end{bmatrix}

W=\begin{bmatrix} * & t1 & t2 \\ p1 & -1  & 1 \\ p2 & 1 & -1 \\ p3 & 1 & -1 \\ p4 & 0 & 1 \end{bmatrix}

M_{0}=\begin{bmatrix} 1 & 0 & 2 & 1 \end{bmatrix}

Reachability

All states that can be reached from a net N with an initial marking M0 are denoted as R(N,M0). The reachability problem is then the following: is it true that M_{w} \in  R(N,M_{0}) where Mw is, for example, an erroneous state. In Graph theory, reachability is the notion of being able to get from one vertex in a Directed graph to some other vertex

The reachability of a petri net's states can be represented with a reachability graph, a directed graph whose points represent states (i. e. M) and arcs represent transitions between two such states. The graph is constructed through breadth-first search as follows: the starting state (M0) is taken, and all possible transitions are explored from this state, then the transitions from these states, and so on. In Graph theory, breadth-first search ( BFS) is a Graph search algorithm that begins at the root node and explores all the neighboring nodes As the reachability graph may be infinitely large, breadth-first search is preferred because depth-first search would not find all possible states even if given infinite time. Depth-first search ( DFS) is an Algorithm for traversing or searching a tree, Tree structure, or graph.

While reachability seems to a be a good tool to find erroneous states, for practical problems the constructed graph usually has far too many states to calculate. To alleviate this problem, linear temporal logic is usually used in conjunction with the tableau method to prove that such states cannot be reached. Linear temporal logic (LTL is a modal Temporal logic with modalities referring to time In Proof theory, the semantic tableau is a Decision procedure for sentential and related logics and a Proof procedure for formulas of First-order 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.

Reachability is known to be decidable, in at least exponential time. All known general algorithms so far, however, employ non-primitive recursive space [2]. The primitive recursive functions are defined using primitive recursion and composition as central operations and are a strict Subset of the recursive

Liveness

Petri nets can be described as having different levels of liveness L0L4. While the levels of liveness are defined on transitions within the Petri net, the Petri net itself is considered Lk live if and only if every transition within it is Lk live.

A Petri net (N,M0)'s transition t is

Note that these are increasingly stringent requirements such that if a transition is L3 live for example, it is automatically L1 and L2 live as well. As an example, (b) Example Petri net is live with the given initial state, but with a different (e. g. totally empty) initial state, all of its transitions are dead.

In computer programming and other applications, the property of liveness of a Petri net is used to model that the system can never lock up.

Boundedness

Reachability graph of (a) Petri net Example if the net is 2-bounded. In this case, it can only have a maximum of 9 (or 32) states.
Reachability graph of (a) Petri net Example if the net is 2-bounded. In this case, it can only have a maximum of 9 (or 32) states.

A Petri net is inherently 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, the initial M0 marking is also restricted by the boundedness. Note that a Petri net is inherently bounded if and only if all its reachability graphs (i. e reachability graphs with all possible starting states) all have a finite number of states.

Formally, K : S \to \mathbb{N^+} is a set of capacity restrictions, which assigns to each place s \in S some positive number n \in \mathbb{N^+} denoting the maximum number of tokens that can occupy that place. A net in which each of its places has some capacity k, is known as an 'inherently k-bounded' Petri net.

Boundedness is decidable by looking at covering, by constructing the Karp-Miller Tree. In Combinatorics and Computer science, the covering problem is a type of general question if a certain structure covers another or how many structures are required Richard Manning Karp (born 1935 is a Computer scientist and Computational theorist, notable for research in In computer programming and other applications, the property of boundedness of a Petri net is used to model limits on available system resources such as CPUs and I/O buses.

Example place-transformation. The grey place that was originally inherently 2-bounded has been transformed into two places: a grey original, and a counter place
Example place-transformation. The grey place that was originally inherently 2-bounded has been transformed into two places: a grey original, and a counter place

Boundedness of a certain place in an inherently bounded net can be mimicked in a non-inherently bounded net by doing a place-transformation, where a new place (called counter-place) is created, 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 M0 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 M0 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).

Extensions

There are many extensions to Petri nets. Some of them are completely backwards-compatible (e. g. coloured 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, they 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 full range of mathematical tools available to analyse normal Petri nets.

The term high-level Petri net is used for many Petri net formalisms that extend the basic P/T net formalism. This includes coloured 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.

Main Petri net types

Petri net types graphically
Petri net types graphically

There are six main types of petri net:

  1. 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: \forall t\in T: |t\bullet|=|\bullet t|=1
  2. Marked Graph (MG) - here, every place has one incoming arc, and one outgoing arc. A marked graph is a Petri net in which every place has exactly one incoming arc and exactly one outgoing arc This means, that there can not be conflict, but there can be concurrency. Mathematically: \forall s\in S: |s\bullet|=|\bullet s|=1
  3. 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: \forall s\in S: (|s\bullet|\leq 1) \vee (\bullet (s\bullet)=\{s\})
  4. Extended free choice (EFC) - a Petri net that can be transformed into an FC.
  5. Asymmetric choice (AC) - concurrency and conflict (in sum, confusion), but not asymmetrically. Mathematically: \forall s_1,s_2\in S: (s_1\bullet \cap s_2\bullet\neq 0) \to [(s_1\bullet\subseteq s_2\bullet) \vee (s_2\bullet\subseteq s_1\bullet)]
  6. Multiple Asymmetric choice (MAC) - multiple concurrency and conflict (in sum, multiple confusion). Mathematically: for a set |P|=k, \forall t\in T exist a subset  \bullet t, and  \bullet T contains all subset and is the Power Set 2k without the empty subset
  7. Petri Net (PN) - confusion is allowed (i. e. everything is allowed)

Other models of concurrency

Other ways of modelling concurrent computation have been proposed, including process algebra, the actor model, and the theory of traces[2]. In Computer science, the process calculi (or process algebras) are a diverse family of related approaches to formally modelling Concurrent systems Process In Computer science, the Actor model is a mathematical model of Concurrent computation that treats "actors" as the universal primitives of concurrent In Mathematics and Computer science, trace theory aims to provide a concrete mathematical underpinning for the study of Concurrent computation and Different models provide tradeoffs of concepts such as compositionality, modularity, and locality. In Mathematics, Semantics, and Philosophy of language, the Principle of Compositionality is the principle that the meaning of a complex expression is determined Modular programming is a software design technique that increases the extent to which software is composed from separate parts called modules

An approach to relating some of these models of concurrency is proposed in the chapter by Winskel and Nielsen[3].

Application areas

Programming tools

See also

References

Footnotes

  1. ^ 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. [1]
  2. ^ Antoni Mazurkiewicz, "Introduction to Trace Theory", in The Book of Traces V. Diekert, G. Rozenberg, eds. World Scientific, Singapore (1995) pp 3-67.
  3. ^ G. Winskel, M. Nielsen. "Models for Concurrency". Handbook of Logic and the Foundations of Computer Science, vol. 4, pages 1-148, OUP.

External links

Dictionary

Petri net

-noun

  1. One of several mathematical representations of discrete distributed systems, a 5-tuple <math>(S,T,F,M_0,W)\!</math>, where
  2. # <math>S</math> is a set of places.
  3. # <math>T</math> is a set of transitions.
  4. # <math>S</math> and <math>T</math> are disjoint, i.e. no object can be both a place and a transition
  5. # <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>.
  6. # <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_s \in \mathbb{N}</math> tokens.
  7. # <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.
© 2009 citizendia.org; parts available under the terms of GNU Free Documentation License, from http://en.wikipedia.org
Dapyx Software network: MP3 Explorer | Ebook Manager | Zenithic