Discrete-event models part 5: Reachability Graphs
Dr. Bystrov
School of Engineering Newcastle University
Discrete-event modelspart 5: Reachability Graph
Copyright By PowCoder代写 加微信 powcoder
Reachability Graphs (PN traversal)
Petri net RG
Concurrency – “diamonds” in RGs – interleaving semantics (one ti fires at a time)
The diamonds are semi-modular, distributive lattices
read Foundations of Maths→Set Theory→Lattice
Discrete-event modelspart 5: Reachability Graph
Reachability Graphs and hazards
“Green” states are the instances of previously encountered states
The diamond net is “split” Non-semimodular, distributive lattice
Non-determinism/persistence, unfairness properties
Discrete-event modelspart 5: Reachability Graph
d1 r1 r2 d2
Reachability Graph
Properties – discussion
Reachability of some particular marking/state
Safety (at most one token in a place)
Deadlock freedom
Liveness (any marking can be reached from the given reachable marking)
Persistence (choice, arbitration) (non-)determinism, (un-)fairness
Early evaluation and others, which are not covered here …
Discrete-event modelspart 5: Reachability Graph
Petri nets Reachability graphs verification
Reactivity in models (open/closed models) FSM models (read the book by ) Concurrency modelling
We need more examples and exercise. . .
Discrete-event modelspart 5: Reachability Graph
程序代写 CS代考 加微信: powcoder QQ: 1823890830 Email: powcoder@163.com