Outline Petri nets Introduction Examples Properties Analysis techniques 1 EE249Fall04 Petri Nets PNs Model introduced by C A Petri in 1962 Ph D Thesis Communication with Automata Applications distributed computing manufacturing control communication networks transportation PNs describe explicitly and graphically sequencing causality conflict non deterministic choice concurrency Basic PN model Asynchronous model partial ordering Main drawback no hierarchy 2 EE249Fall04 Example Synchronization at single track rail segment Preconditions 3 EE249Fall04 Playing the token game 4 EE249Fall04 Conflict for resource track 5 EE249Fall04 Petri Net Graph Bipartite weighted directed graph Places circles Transitions bars or boxes Arcs arrows labeled with weights Tokens black dots p2 t2 p1 2 t1 p4 3 t3 6 p3 EE249Fall04 Petri Net A PN N M0 is a Petri Net Graph N places represent distributed state by holding tokens marking state M is an n vector m1 m2 m3 where mi is the non negative number of tokens in place pi initial marking M0 is initial state transitions represent actions events enabled transition enough tokens in predecessors firing transition modifies marking p2 and an initial marking M0 p1 2 t1 p4 3 Places Transitions conditions events 7 t2 t3 p3 EE249Fall04 Transition firing rule A marking is changed according to the following rules A transition is enabled if there are enough tokens in each input place An enabled transition may or may not fire The firing of a transition modifies marking by consuming tokens from the input places and producing tokens in the output places 2 2 3 2 2 3 8 EE249Fall04 Concurrency causality choice t1 t2 t5 t3 9 t4 t6 EE249Fall04 Concurrency causality choice t1 Concurrency t2 t5 t3 10 t4 t6 EE249Fall04 Concurrency causality choice t1 t2 Causality sequencing t3 11 t5 t4 t6 EE249Fall04 Concurrency causality choice t1 t2 t5 t3 12 Choice conflict t4 t6 EE249Fall04 Concurrency causality choice t1 t2 t5 t3 13 Choice conflict t4 t6 EE249Fall04 Communication Protocol Send msg Receive msg P2 P1 Send Ack Receive Ack 14 EE249Fall04 Communication Protocol Send msg Receive msg P2 P1 Send Ack Receive Ack 15 EE249Fall04 Communication Protocol Send msg Receive msg P2 P1 Send Ack Receive Ack 16 EE249Fall04 Communication Protocol Send msg Receive msg P2 P1 Send Ack Receive Ack 17 EE249Fall04 Communication Protocol Send msg Receive msg P2 P1 Send Ack Receive Ack 18 EE249Fall04 Communication Protocol Send msg Receive msg P2 P1 Send Ack Receive Ack 19 EE249Fall04 Producer Consumer Problem Produce Buffer Consume 20 EE249Fall04 Producer Consumer Problem Produce Buffer Consume 21 EE249Fall04 Producer Consumer Problem Produce Buffer Consume 22 EE249Fall04 Producer Consumer Problem Produce Buffer Consume 23 EE249Fall04 Producer Consumer Problem Produce Buffer Consume 24 EE249Fall04 Producer Consumer Problem Produce Buffer Consume 25 EE249Fall04 Producer Consumer Problem Produce Buffer Consume 26 EE249Fall04 Producer Consumer Problem Produce Buffer Consume 27 EE249Fall04 Producer Consumer Problem Produce Buffer Consume 28 EE249Fall04 Producer Consumer Problem Produce Buffer Consume 29 EE249Fall04 Producer Consumer Problem Produce Buffer Consume 30 EE249Fall04 Producer Consumer Problem Produce Buffer Consume 31 EE249Fall04 Producer Consumer Problem Produce Buffer Consume 32 EE249Fall04 Producer Consumer Problem Produce Buffer Consume 33 EE249Fall04 Producer Consumer with priority A Consumer B can consume only if buffer A is empty Inhibitor arcs B 34 EE249Fall04 PN properties Behavioral depend on the initial marking most interesting Reachability Boundedness Schedulability Liveness Conservation Structural do not depend on the initial marking often too restrictive Consistency Structural boundedness 35 EE249Fall04 Reachability Marking M is reachable from marking M0 if there exists a sequence of firings M0 t1 M1 t2 M2 M that transforms M0 to M The reachability problem is decidable p2 p1 t2 t1 p4 p3 36 0 1 0 1 0 M 1 1 0 0 t3 0 1 0 1 0 t3 M1 1 0 0 1 t2 M 1 1 0 0 EE249Fall04 Liveness Liveness from any marking any transition can become fireable Liveness implies deadlock freedom not viceversa Not live 37 EE249Fall04 Liveness Liveness from any marking any transition can become fireable Liveness implies deadlock freedom not viceversa Not live 38 EE249Fall04 Liveness Liveness from any marking any transition can become fireable Liveness implies deadlock freedom not viceversa Deadlock free 39 EE249Fall04 Liveness Liveness from any marking any transition can become fireable Liveness implies deadlock freedom not viceversa Deadlock free 40 EE249Fall04 Boundedness Boundedness the number of tokens in any place cannot grow indefinitely 1 bounded also called safe Application places represent buffers and registers check there is no overflow Unbounded 41 EE249Fall04 Boundedness Boundedness the number of tokens in any place cannot grow indefinitely 1 bounded also called safe Application places represent buffers and registers check there is no overflow Unbounded 42 EE249Fall04 Boundedness Boundedness the number of tokens in any place cannot grow indefinitely 1 bounded also called safe Application places represent buffers and registers check there is no overflow Unbounded 43 EE249Fall04 Boundedness Boundedness the number of tokens in any place cannot grow indefinitely 1 bounded also called safe Application places represent buffers and registers check there is no overflow Unbounded 44 EE249Fall04 Boundedness Boundedness the number of tokens in any place cannot grow indefinitely 1 bounded also called safe Application places represent buffers and registers check there is no overflow Unbounded 45 EE249Fall04 Conservation Conservation the total number of tokens in the net is constant Not conservative 46 EE249Fall04 Conservation Conservation the total number of tokens in the net is constant Not conservative 47 EE249Fall04 Conservation Conservation the total number of tokens in the net is constant Conservative 2 2 48 EE249Fall04 Analysis techniques Structural analysis techniques Incidence matrix T and S Invariants State Space Analysis techniques Coverability Tree Reachability Graph 49 EE249Fall04 Incidence Matrix t2 p1 t1 p2 p3 t3 t1 t2 t3 1 A 1 0 0 1 1 0 p1 1 p2 1 p3 Necessary condition for marking M to be reachable from initial marking M0 there exists firing vector v s t M M0 A v 50 EE249Fall04 State equations E g reachability of M 0 0 1 T from M0 1 0 0 T p1 t1 p2 t2 p3 1 A 1 0 0 1 1 0 1 1 t3 1 v1 0 1 0 1 1 0 0 1 1 0 0 0 1
View Full Document
Unlocking...