stochastic Petri net
{{Refimprove|date=January 2014}}
Stochastic Petri nets are a form of Petri net where the transitions fire after a probabilistic delay determined by a random variable.
Definition
A stochastic Petri net is a five-tuple SPN = (P, T, F, M0, Λ) where:
- P is a set of states, called places.
- T is a set of transitions.
- F where F ⊂ (P × T) ∪ (T × P) is a set of flow relations called "arcs" between places and transitions (and between transitions and places).
- M0 is the initial marking.
- Λ = is the array of firing rates λ associated with the transitions. The firing rate, a random variable, can also be a function λ(M) of the current marking.
Correspondence to Markov process
The reachability graph of stochastic Petri nets can be mapped directly to a Markov process. It satisfies the Markov property, since its states depend only on the current marking.
Each state in the reachability graph is mapped to a state in the Markov process, and the firing of a transition with firing rate λ corresponds to a Markov state transition with probability λ.
Software tools
- [http://pipe2.sourceforge.net/ Platform Independent Petri net Editor]{{Cite journal | last1 = Dingle | first1 = N. J. | last2 = Knottenbelt | first2 = W. J. | last3 = Suto | first3 = T. | doi = 10.1145/1530873.1530881 | title = PIPE2 | journal = ACM SIGMETRICS Performance Evaluation Review | volume = 36 | issue = 4 | pages = 34 | year = 2009 | s2cid = 3265173 }}
- [http://www.oris-tool.org/ ORIS Tool]{{Cite journal | doi = 10.1109/TSE.2012.42| title = A Quantitative Approach to Input Generation in Real-Time Testing of Stochastic Systems| journal = IEEE Transactions on Software Engineering| volume = 39| issue = 3| pages = 292| year = 2013| last1 = Carnevali | first1 = L. | last2 = Ridi | first2 = L. | last3 = Vicario | first3 = E. | s2cid = 8064028| hdl = 2158/656220| hdl-access = free}}
- [http://www.di.unito.it/~greatspn/index.html GreatSPN]{{Cite book | doi = 10.1007/978-3-319-10696-0_13| chapter = A New GreatSPN GUI for GSPN Editing and CSLTA Model Checking| title = Quantitative Evaluation of Systems| volume = 8657| pages = 170–173| series = Lecture Notes in Computer Science| year = 2014| last1 = Amparore | first1 = E. G. | isbn = 978-3-319-10695-3}}
References
{{Reflist}}
External links
- [http://www.fd.cvut.cz/department/k611/pedagog/tho_a/a_soubory/spn_introduction.pdf Stochastic Petri Nets: an Introduction]
- [http://www.inf.ed.ac.uk/teaching/courses/pm/handouts/stochasticpetrinets.pdf Stochastic Petri Nets]
Category:Formal specification languages