Сандық жүйелерді сипаттау моделі: Петри торы

Model to describe distributed systems

A Petri net, also known as a place/transition net (PT net), is one of several mathematical modeling languages for the description of distributed systems. It is a class of discrete event dynamic system. A Petri net is a directed bipartite graph that has two types of elements: places and transitions. Place elements are depicted as white circles and transition elements are depicted as rectangles. A place can contain any number of tokens, depicted as black circles. A transition is enabled if all places connected to it as inputs contain at least one token. Some sources state that Petri nets were invented in August 1939 by Carl Adam Petri—at the age of 13—for the purpose of describing chemical processes. Like industry standards such as UML activity diagrams, Business Process Model and Notation, and event driven process chains, Petri nets offer a graphical notation for stepwise processes that include choice, iteration, and concurrent execution. Unlike these standards, Petri nets have an exact mathematical definition of their execution semantics, with a well developed mathematical theory for process analysis.

The German computer scientist Carl Adam Petri, after whom such structures are named, analyzed Petri nets extensively in his 1962 dissertation Kommunikation mit Automaten.

A Petri net consists of places, transitions, and arcs. Arcs run from a place to a transition or vice versa, never between places or between 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. Graphically, places in a Petri net may contain a discrete number of marks called tokens. Any distribution of tokens over the places will represent a configuration of the net called a marking. In an abstract sense relating to a Petri net diagram, a transition of a Petri net may fire if it is enabled, i. e. there are sufficient tokens in all of its input places; when the transition fires, it consumes the required input tokens, and creates tokens in its output places. A firing is atomic, i. e. a single non interruptible step. Unless an execution policy (e. g. a strict ordering of transitions, describing precedence) is defined, the execution of Petri nets is nondeterministic: when multiple transitions are enabled at the same time, they will fire in any order. Since firing is nondeterministic, and multiple tokens may be present anywhere in the net (even in the same place), Petri nets are well suited for modeling the concurrent behavior of distributed systems.

Petri nets are state transition systems that extend a class of nets called elementary nets. Definition 1. A net is a tuple where
and are disjoint finite sets of places and transitions, respectively. is a set of (directed) arcs (or flow relations). Definition 2. Given a net N = (P, T, F), a configuration is a set C so that C ⊆ P.

Definition 3. An elementary net is a net of the form EN = (N, C) where
N = (P, T, F) is a net. C is such that C ⊆ P is a configuration. Definition 4. A Petri net is a net of the form PN = (N, M, W), which extends the elementary net so that
N = (P, T, F) is a net. M : P → Z is a place multiset, where Z is a countable set. M extends the concept of configuration and is commonly described with reference to Petri net diagrams as a marking. W : F → Z is an arc multiset, so that the count (or weight) for each arc is a measure of the arc multiplicity. If a Petri net is equivalent to an elementary net, then Z can be the countable set {0,1} and those elements in P that map to 1 under M form a configuration. Similarly, if a Petri net is not an elementary net, then the multiset M can be interpreted as representing a non singleton set of configurations. In this respect, M extends the concept of configuration for elementary nets to Petri nets. In the diagram of a Petri net (see top figure right), places are conventionally depicted with circles, transitions with long narrow rectangles and arcs as one way arrows that show connections of places to transitions or transitions to places. If the diagram were of an elementary net, then those places in a configuration would be conventionally depicted as circles, where each circle encompasses a single dot called a token. In the given diagram of a Petri net (see right), the place circles may encompass more than one token to show the number of times a place appears in a configuration. The configuration of tokens distributed over an entire Petri net diagram is called a marking. In the top figure (see right), the place p1 is an input place of transition t; whereas, the place p2 is an output place to the same transition. Let PN0 (top figure) be a Petri net with a marking configured M0, and PN1 (bottom figure) be a Petri net with a marking configured M1. The configuration of PN0 enables transition t through the property that all input places have sufficient number of tokens (shown in the figures as dots) "equal to or greater" than the multiplicities on their respective arcs to t. Once and only once a transition is enabled will the transition fire. In this example, the firing of transition t generates a map that has the marking configured M1 in the image of M0 and results in Petri net PN1, seen in the bottom figure. In the diagram, the firing rule for a transition can be characterised by subtracting a number of tokens from its input places equal to the multiplicity of the respective input arcs and accumulating a new number of tokens at the output places equal to the multiplicity of the respective output arcs. Remark 1. The precise meaning of "equal to or greater" will depend on the precise algebraic properties of addition being applied on Z in the firing rule, where subtle variations on the algebraic properties can lead to other classes of Petri nets; for example, algebraic Petri nets. The following formal definition is loosely based on Many alternative definitions exist.

A common variation is to disallow arc multiplicities and replace the bag of arcs W with a simple set, called the flow relation, This does not limit expressive power as both can represent each other. Another common variation, e. g. in Desel and Juhás (2001), is to allow capacities to be defined on places. This is discussed under extensions below.

Meseguer and Montanari considered a kind of symmetric monoidal categories known as Petri categories.

One thing that makes Petri nets interesting is that they provide a balance between modeling power and analyzability: many things one would like to know about concurrent systems can be automatically determined for Petri nets, although some of those things are very expensive to determine in the general case. Several subclasses of Petri nets have been studied that can still model interesting classes of concurrent systems, while these determinations become easier. An overview of such decision problems, with decidability and complexity results for Petri nets and some subclasses, can be found in Esparza and Nielsen (1995).

The reachability problem for Petri nets is to decide, given a Petri net N and a marking M, whether
It is a matter of walking the reachability graph defined above, until either the requested marking is reached or it can no longer be found. This is harder than it may seem at first: the reachability graph is generally infinite, and it isn't easy to determine when it is safe to stop. In fact, this problem was shown to be EXPSPACE hard years before it was shown to be decidable at all (Mayr, 1981). Papers continue to be published on how to do it efficiently. In 2018, Czerwiński et al. improved the lower bound and showed that the problem is not ELEMENTARY. In 2021, this problem was shown to be non primitive recursive, independently by Jerome Leroux
and by Wojciech Czerwiński and Łukasz Orlikowski. These results thus close the long standing complexity gap. While reachability seems to 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 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.

Petri nets can be described as having different degrees of liveness A Petri net is called live if and only if all of its transitions are live, where a transition is
dead, if it can never fire, i. e. it is not in any firing sequence in
live (potentially fireable), if and only if it may fire, i. e. it is in some firing sequence in
live if it can fire arbitrarily often, i. e. if for every positive integer k, it occurs at least k times in some firing sequence in
live if it can fire infinitely often, i. e. if there is some fixed (necessarily infinite) firing sequence in which for every positive integer k, the transition occurs at least k times,
live (live) if it may always fire, i. e. it is live in every reachable marking in

Note that these are increasingly stringent requirements: liveness implies liveness, for
These definitions are in accordance with Murata's overview, which additionally uses live as a term for dead.

A place in a Petri net is called k bound if it does not contain more than k tokens in all reachable markings, including the initial marking; it is said to be safe if it is 1 bounded; it is bounded if it is k bounded for some k.

A (marked) Petri net is called k bounded, safe, or bounded when all of its places are. A Petri net (graph) is called (structurally) bounded if it is bounded for every possible initial marking. A Petri net is bounded if and only if its reachability graph is finite. Boundedness is decidable by looking at covering, by constructing the Karp–Miller Tree. It can be useful to explicitly impose a bound on places in a given net. This can be used to model limited system resources. Some definitions of Petri nets explicitly allow this as a syntactic feature. Formally, Petri nets with place capacities can be defined as tuples , where is a Petri net, an assignment of capacities to (some or all) places, and the transition relation is the usual one restricted to the markings in which each place with a capacity has at most that many tokens. For example, if in the net N, both places are assigned capacity 2, we obtain a Petri net with place capacities, say N2; its reachability graph is displayed on the right. Alternatively, places can be made bounded by extending the net. To be exact,
a place can be made k bounded by adding a "counter place" with flow opposite to that of the place, and adding tokens to make the total in both places k.

As well as for discrete events, there are Petri nets for continuous and hybrid discrete continuous processes and related to discrete, continuous and hybrid automata.