A Survey of Markovian Behavioral Equivalences

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.

• Type: Conference
• Year: 2007
• Where: SFM
• Authors: Marco Bernardo
• Keywords: Markovian, Markovian Behavioral Equivalences, Markovian Trace Equivalence, SFM 2007