Institutional Repository
| A semantics for every GSPN | |
| Eisentraut, Christian (1); Hermanns, Holger (1); Katoen, Joost-Pieter (2); Zhang, Lijun (3) | |
| 2013 | |
| Conference Name | 34th International Conference on Application and Theory of Petri Nets and Concurrency, PETRI NETS 2013 |
| Pages | 90-109 |
| Conference Date | June 24, 2013 - June 28, 2013 |
| Conference Place | Milan, Italy |
| Indexed Type | EI |
| Publish Place | Springer Verlag, Tiergartenstrasse 17, Heidelberg, D-69121, Germany |
| ISSN | 3029743 |
| ISBN | 9783642386961 |
| Department | (1) Saarland University, Computer Science, Germany; (2) Department of Computer Science, RWTH Aachen University, Germany; (3) State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, China |
| English Abstract | Generalised Stochastic Petri Nets (GSPNs) are a popular modelling formalism for performance and dependability analysis. Their semantics is traditionally associated to continuous-time Markov chains (CTMCs), enabling the use of standard CTMC analysis algorithms and software tools. Due to ambiguities in the semantic interpretation of confused GSPNs, this analysis strand is however restricted to nets that do not exhibit non-determinism, the so-called well-defined nets. This paper defines a simple semantics for every GSPN. No restrictions are imposed on the presence of confusions. Immediate transitions may be weighted but are not required to be. Cycles of immediate transitions are admitted too. The semantics is defined using a non-deterministic variant of CTMCs, referred to as Markov automata. We prove that for well-defined bounded nets, our semantics is weak bisimulation equivalent to the existing CTMC semantics. Finally, we briefly indicate how every bounded GSPN can be quantitatively assessed. © 2013 Springer-Verlag.; Generalised Stochastic Petri Nets (GSPNs) are a popular modelling formalism for performance and dependability analysis. Their semantics is traditionally associated to continuous-time Markov chains (CTMCs), enabling the use of standard CTMC analysis algorithms and software tools. Due to ambiguities in the semantic interpretation of confused GSPNs, this analysis strand is however restricted to nets that do not exhibit non-determinism, the so-called well-defined nets. This paper defines a simple semantics for every GSPN. No restrictions are imposed on the presence of confusions. Immediate transitions may be weighted but are not required to be. Cycles of immediate transitions are admitted too. The semantics is defined using a non-deterministic variant of CTMCs, referred to as Markov automata. We prove that for well-defined bounded nets, our semantics is weak bisimulation equivalent to the existing CTMC semantics. Finally, we briefly indicate how every bounded GSPN can be quantitatively assessed. © 2013 Springer-Verlag. |
| Language | 英语 |
| Content Type | 会议论文 |
| URI | http://ir.iscas.ac.cn/handle/311060/16672 |
| Collection | 中国科学院软件研究所 |
| Recommended Citation GB/T 7714 | Eisentraut, Christian ,Hermanns, Holger ,Katoen, Joost-Pieter ,et al. A semantics for every GSPN[C]. Springer Verlag, Tiergartenstrasse 17, Heidelberg, D-69121, Germany,2013:90-109. |
| Files in This Item: | There are no files associated with this item. | |||||
Items in the repository are protected by copyright, with all rights reserved, unless otherwise indicated.
Edit Comment