Modelling Complex Software Systems
Lecture PN02 II: Semantics
Artem Polyvyanyy,
Copyright By PowCoder代写 加微信 powcoder
Semester 1, 2022
Interleaving semantics of net systems
Concurrency semantics of net systems
Reachable markings
Foranetsystem= , ,amarkingofisareachablemarkingofif = or there exists a sequence of steps
⋯ ,
where∈N, =,and ∈,∈ 1.. .Afinalmarkingisamarkinginwhich no hot transitions are enabled (i.e., the system can remain in a final marking forever).
Figure: A net system.
Marking Reachable Final
ACC ADD ACDDE
Sequential runs (occurrence sequences)
A sequential run of a net system = , is a possibly infinite sequence of steps that starts at the initial marking of .
Figure: A net system.
ACC→ BCC→ACC→⋯
We are often interested in complete sequential runs:
A finite sequential run is complete if it leads to a final marking of the net system An infinite sequential run is complete if no additional step can be inserted into it
Sequential run Finite Complete
ACC→” BCC
ACC→” BCC→$ ACC
ACC→” BCC→% ACDE “%”
ACC→ BCC→ACDE→ BCDE→% ADDEE→&
&”$ ADDE→ADD→BDD→
ADD→” BDD→$ ⋯ “$”
Marking graphs (reachability graphs)
The reachable markings and steps of a net system define the marking graph of .
Its nodes describe the reachable markings of
Its edges describe the steps between the reachable markings of The initial marking is highlighted with an arrow leading to it
Each final marking is highlighted with a double line border
Figure: A one cookie vending machine . Figure: The marking graph of .
Interleaving semantics of net systems
The collection of all complete sequential runs of a net system defines the interleaving semantics of the system.
A net system can describe an infinite collection of complete sequential runs
Each sequential run of a net system is a directed walk in its marking graph that starts at
the node that corresponds to the initial marking of the net system
The marking graph describes all and only complete sequential runs of the net system
Figure: The marking graph of .
“$”$%&”$” AC→ BC→ AC→ BC→ AC→ ADE→ AD→ BD→ AD→⋯
1. The empty sequence
2. AC→”BC→$AC
3 . A C →” B C →$ A C →” B C →$ A C ⋯
n . A C →” B C →$ A C →% A D E
n+1. AC→” BC→$ AC→” BC→$ AC→% ADE
m . A C →” B C →$ A C →% A D E →& A D
m + 1 . A C →” B C →$ A C →” B C →$ A C →% A D E →& A D ⋯
The state explosion problem
In general, a net system can define a very large, or even infinite, marking graph. This phenomenon is known as the state explosion problem.[1]
Figure: A two cookies vending machine ′.
Figure: The marking graph of ′.
Interleaving semantics of net systems
Concurrency semantics of net systems
A net system can be interpreted as a collection of distributed runs. A distributed run describes the behaviour of the system more accurately but requires more effort to understand. The building block of a distributed run is an action, which describes a step.
Figure: An action that describes the step on the left.
The transition refers to the occurred transition
The places without incoming arcs represent
the marking before the transition occurrence The places without outgoing arcs represent the marking after the transition occurrence
Distributed runs (processes)
A distributed run of a net system is a possibly infinite acyclic net structure, also called a causal net, that starts at the initial marking and is defined by an uninterrupted sequence of actions executed by the system.
Figure: An uninterrupted sequence of actions of the two cookies vending machine.
Concurrency semantics of net systems
Each transition of a distributed run represents an action. The collection of all complete distributed runs of a net system defines the concurrency semantics of the system.
A finite distributed run is complete if its places without outgoing arcs represent a final marking of the net system
An infinite distributed run is complete if no additional action can be inserted into it
Figure: A complete distributed run from marking ACC to marking ADD.
Sequential vs distributed runs
Both systems shown below have the same complete sequential runs[2], namely:
ACE →” BCE →$ BDE and ACE →$ ADE →” BDE.
System 45: Independent a and b. System 48: Arbitrary order of a and b. However, complete distributed runs of these two net systems are distinct.
Figure: The only complete distributed Figure: One of the two complete distributed
runof . runsof .
Causality and concurrency relations
Distributed runs encode causality and concurrency relations between actions. A chain of arcs from element 9 to element : in a causal net specifies that
9 causally precedes :, denoted by 9 ↣ :.
If two elements 9 and : of a distributed run are not causal (i.e., neither 9 ↣ : nor 9 ↢ :
holds), then they are concurrent, denoted by 9 || :.
The causality, inverse causality, and concurrency relations partition the Cartesian product
of elements of a distributed run.
Figure: A distributed run.
A↣↣ II↣ II↣ II↣↣ B ↢ II ↢ II II II ↢ II II C II ↣ II II II ↣ II II ↣ D↢↢↢ II↢ II↢↢ II E↣↣ II↣ II↣ II↣↣ E′↢↣↢ II II↣↢ II↣
a b A B C D E E′ E′′ a II ↣ ↢ ↣ II ↣ ↢ ↣ ↣ b ↢ II ↢ II ↢ ↣ ↢ ↢ ↣
E′′↢↢↢ II↢ II↢↢ II
A Petri net can describe a system with infinitely many reachable states and runs
A Petri net can be interpreted according to different semantics (e.g., sequential
and distributed runs)
Sequential runs suit well for the analysis of many practical problems and are well- studied in the literature
Distributed runs capture the causality and concurrency relations between actions of the system explicitly
Hence, distributed runs can be used to distinguish the occurrence of actions in sequence by chance from a situation when the occurrence of an action is a prerequisite for the occurrence of the next action
Moreover, actions that may occur in any order but never simultaneously can be distinguished from actions that can occur truly simultaneously
The fact that a net system can describe infinitely many states and runs complicates its analysis, as a condition of interest (e.g., a defect in the design of the system) can manifest after a very long run of the system composed of a non- anticipated but feasible according to the rules of the system sequence of steps
Further Reading
1. : The State Explosion Problem. 1996: 429-528
https://doi.org/10.1007/3-540-65306-6_21
2. : Understanding – Modeling Techniques, Analysis Methods, Case Studies. Springer 2013, ISBN 978-3-642-33277-7 https://doi.org/10.1007/978-3-642-33278-4
3. : – Properties, Analysis and Applications. Proceedings of the IEEE, 77 (4), pp. 541-580 (1989) http://dx.doi.org/10.1109/5.24143
4. , : The Non-sequential Behavior of . Inf. Control. 57(2/3): 125-147 (1983) https://doi.org/10.1016/S0019-9958(83)80040-0
5. Jörg Desel: Validation of Process Models by Construction of Process Nets. Business Process Management 2000: 110-128 https://doi.org/10.1007/3-540-45594-9_8
6. , César Fernández: Nonsequential Processes – A Petri Net View. EATCS Monographs on Theoretical Computer Science 13, Springer 1988, ISBN 978-3-642-73485-4, pp. i-ix, 1-112 https://doi.org/10.1007/978-3-642-73483-0
7. , : Unfoldings – A Partial-Order Approach to Model Checking. Monographs in Theoretical Computer Science. An EATCS Series, Springer 2008, ISBN 978-3- 540-77425-9, pp. I-XII, 1-156 https://doi.org/10.1007/978-3-540-77426-6
8. The World community: https://www2.informatik.uni-hamburg.de/TGI/PetriNets/
程序代写 CS代考 加微信: powcoder QQ: 1823890830 Email: powcoder@163.com