×

A survey of Markovian behavioral equivalences. (English) Zbl 1323.68402

Bernardo, Marco (ed.) et al., Formal methods for performance evaluation. 7th international school on formal methods for the design of computer, communication, and software systems, SFM 2007, Bertinoro, Italy, May 28 – June 2, 2007. Advanced lectures. Berlin: Springer (ISBN 978-3-540-72482-7/pbk). Lecture Notes in Computer Science 4486, 180-219 (2007).
Summary: Markovian behavioral equivalences are a means to relate and manipulate the formal descriptions of systems with an underlying CTMC semantics. There are three fundamental approaches to their definition: bisimilarity, testing, and trace. In this paper we survey the major results appeared in the literature about Markovian bisimilarity, Markovian testing equivalence, and Markovian trace equivalence. The objective is to compare these equivalences with respect to a number of criteria such as their discriminating power, the exactness of the CTMC-level aggregations they induce, the achievement of the congruence property, the existence of sound and complete axiomatizations, the existence of logical characterizations, and the existence of efficient verification algorithms.
For the entire collection see [Zbl 1118.68001].

MSC:

68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
68Q60 Specification and verification (program logics, model checking, etc.)
68Q87 Probability in computer science (algorithm analysis, random structures, phase transitions, etc.)

Software:

MoDeST
PDFBibTeX XMLCite
Full Text: DOI