- Date:22 Nov 2020
- Views:0
- Downloads:0
- Size:290.00 KB

Transcription:

COMP290 084Graphical Representation ofAsynchronous SystemsJan 15 2004 Graphical Representation.

Petri Nets Asynchronous State Graphs Burst Mode Representation Timed Automata Petri Nets.

Reference Tadao Murata Petri nets Properties Analysisand Applications Proc of the IEEE 77 4 1989 available on class websiteLecture Notes by .

Gabriel EireaUC Berkeley Petri Nets Properties Analysis and ApplicationsGabriel Eirea.

UC BerkeleyBased on paper by T Murata Introduction History Transition enabling firing Modeling examples.

Behavioral properties Analysis methods Liveness safeness reachability Analysis synthesis of Marked Graphs Structural properties.

Modified Petri Nets Introduction Petri Nets concurrent asynchronous distributed parallel nondeterministic and or stochastic.

graphical tool visual communication aid mathematical tool state equations algebraic equations etc communication between theoreticians and.

practitioners 1962 C A Petri s dissertation U Darmstadt W Germany 1970 Project MAC Conf on Concurrent Systems andParallel Computation MIT USA 1975 Conf on Petri Nets and related Methods MIT USA .

1979 Course on General Net Theory of Processes andSystems Hamburg W Germany 1980 First European Workshop on Applications andTheory of Petri Nets Strasbourg France 1985 First International Workshop on Timed Petri Nets.

Torino Italy Applications performance evaluation communication protocols distributed software systems.

distributed database systems concurrent and parallel programs industrial control systems discrete events systems multiprocessor memory systems.

dataflow computing systems fault tolerant systems etc etc etc Definition Directed weighted bipartite graph.

places transitions arcs places to transitions or transitionsto places weights associated with each arc.

Initial marking assigns a non negative integer to each Transition firing rule A transition t is enabled if each inputplace p has at least w p t tokens.

An enabled transition may or may A firing on an enabled transition tremoves w p t from each inputplace p and adds w t p to eachoutput place p .

Firing example2H2 O2 2H2O Firing example2H2 O2 2H2O Some definitions.

source transition no inputs sink transition no outputs self loop a pair p t s t p is both an input and an output of t pure PN no self loops ordinary PN all arc weights are 1 s.

infinite capacity net places can accommodate an unlimitednumber of tokens finite capacity net each place p has a maximum capacity strict transition rule after firing each output place can thave more than K p tokens.

Theorem every pure finite capacity net can be transformedinto an equivalent infinite capacity net Modeling FSMsvend 15 candyvend 20 candy.

Modeling FSMsvend 15 candy5 state machines each transition5 5 has exactly.

one input and5 one outputvend 20 candy Modeling FSMsconflict 5 5.

or choice 5 Modeling concurrencymarked graph each place hasexactly one.

t3 incoming arc Modeling concurrencyt2 concurrency Modeling dataflowcomputation.

x a b a b copy a b xcopy a b Modeling communicationready ready.

to send to receivesend full receiveproc 1 wait proc 2receive sendreceived sent.

Modeling synchronizationwriting k reading Behavioral properties 1 Properties that depend on the initial marking Reachability.

Mn is reachable from M0 if exists a sequence offirings that transform M0 into Mn reachability is decidable but exponential Boundedness a PN is bounded if the number of tokens in each.

place doesn t exceed a finite number k for anymarking reachable from M0 a PN is safe if it is 1 bounded Behavioral properties 2 Liveness.

a PN is live if no matter what marking has beenreached it is possible to fire any transition with anappropriate firing sequence equivalent to deadlock free strong property different levels of liveness are defined.

L0 dead L1 L2 L3 and L4 live Reversibility a PN is reversible if for each marking M reachable fromM0 M0 is reachable from M relaxed condition a marking M is a home state if for.

each marking M reachable from M0 M is reachable Behavioral properties 3 Coverability a marking is coverable if exists M reachable fromM0 s t M p M p for all places p.

Persistence a PN is persistent if for any two enabled transitions the firing of one of them will not disable the other then once a transition is enabled it remainsenabled until it s fired.

all marked graphs are persistent a safe persistent PN can be transformed into amarked graph Analysis methods 1 Coverability tree.

tree representation of all possible markings root M0 nodes markings reachable from M0 arcs transition firings if net is unbounded then tree is kept finite by.

introducing the symbol Properties a PN is bounded iff doesn t appear in any node a PN is safe iff only 0 s and 1 s appear in nodes a transition is dead iff it doesn t appear in any arc.

if M is reachable form M0 then exists a node M that covers Coverability tree example Coverability tree examplet3 M1 001 dead end .

Coverability tree examplet3 M1 001 M3 1 0 dead end Coverability tree examplet3 M1 001 M3 1 0 .

dead end M4 0 1 Coverability tree examplet3 M1 001 M3 1 0 dead end .

M4 0 1 M3 1 0 t2 old Coverability tree examplet3 M1 001 M3 1 0 dead end .

M4 0 1 M6 1 0 t2 old M5 0 1 Coverability tree exampleM1 001 M3 1 0 .

001 1 0 dead end M4 0 1 M6 1 0 t2 old M5 0 1 coverability graph coverability tree.

Subclasses of Petri Nets 1 Ordinary PNs all arc weights are 1 s same modeling power as general PN moreconvenient for analysis but less efficient.

State machine each transition has exactly one input placeand exactly one output place Marked graph each place has exactly one input transition.

and exactly one output transition Subclasses of Petri Nets 2 Free choice every outgoing arc from a place is either uniqueor is a unique incoming arc to a transition.

Extended free choice if two places have some common outputtransition then they have all their outputtransitions in common Asymmetric choice or simple .

if two places have some common outputtransition then one of them has all the outputtransitions of the other and possibly more Subclasses of Petri Nets 3 AC EFC FC SM MG.

Liveness and SafenessCriteria 1 general PN if a PN is live and safe then there are nosource or sink places and source or sink.

transitions if a connected PN is live and safe then the netis strongly connected a SM is live iff the net is strongly connectedand M0 has at least one token.

a SM is safe iff M0 has at most one token Liveness and SafenessCriteria 2 a MG is equivalent to a marked directed graph arcs places nodes transitions .

a MG is live iff M0 places at least one token oneach directed circuit in the marked directed a live MG is safe iff every place belongs to adirected circuit on which M0 places exactly there exists a live and safe marking in a.

directed graph iff it is strongly connectedProc. of the IEEE, 77(4), 1989. available on class website Credits Lecture Notes by: Gabriel Eirea UC Berkeley Petri Nets: Properties, Analysis and Applications Gabriel Eirea UC Berkeley 10/8/02 Based on paper by T. Murata Outline Introduction/History Transition enabling & firing Modeling examples Behavioral properties Analysis methods Liveness ...

Recent Views:

- Esra spring member meeting
- The twists of avalon thinking in wpf
- Pourquoi apprendre le fran ais
- Enfermedades m s frecuentes y medidas de prevenci n
- Abc poem for number the stars hoboken charter school
- A report on america s bone health why should you care
- The networked education database
- Bagaimana cara memilih topik yunita sari
- Africa in the world today
- It s slippery at the top churn and anxiety amongst elite