A semantics for every GSPN

ISCAS OpenIR

	A semantics for every GSPN
	Eisentraut, Christian (1); Hermanns, Holger (1); Katoen, Joost-Pieter (2); Zhang, Lijun (3)
	2013
会议名称	34th International Conference on Application and Theory of Petri Nets and Concurrency, PETRI NETS 2013
页码	90-109
会议日期	June 24, 2013 - June 28, 2013
会议地点	Milan, Italy
收录类别	EI
出版地	Springer Verlag, Tiergartenstrasse 17, Heidelberg, D-69121, Germany
ISSN	3029743
ISBN	9783642386961
部门归属	(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
摘要	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.
语种	英语
内容类型	会议论文
URI标识	http://ir.iscas.ac.cn/handle/311060/16672
专题	中国科学院软件研究所
推荐引用方式 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.