Markovian testing and trace equivalences have been recently proposed as reasonable alternatives to Markovian bisimilarity, as both of them induce at the Markov chain level an aggregation strictly coarser than ordinary lumping that is still exact. In this paper we provide a modal logic characterization for each of the two non-bisimulation-based Markovian behavioral equivalences, which relies on a quantitative interpretation of a variant of the Hennessy-Milner logic. We also show that, unlike the Markovian bisimilarity case, such modal logic characterizations exist only when probabilistic and temporal aspects are treated in a global way.

Modal Logic Characterization of Markovian Testing and Trace Equivalences

Bernardo, Marco;
2006

Abstract

Markovian testing and trace equivalences have been recently proposed as reasonable alternatives to Markovian bisimilarity, as both of them induce at the Markov chain level an aggregation strictly coarser than ordinary lumping that is still exact. In this paper we provide a modal logic characterization for each of the two non-bisimulation-based Markovian behavioral equivalences, which relies on a quantitative interpretation of a variant of the Hennessy-Milner logic. We also show that, unlike the Markovian bisimilarity case, such modal logic characterizations exist only when probabilistic and temporal aspects are treated in a global way.
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: http://hdl.handle.net/11576/1891887
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 4
  • ???jsp.display-item.citation.isi??? ND
social impact