Several approaches have been proposed to relax behavioral equivalences for fine-grain models including probabilities and time. All of them face two problems behind the notion of approximation, i.e., the lack of transitivity and the efficiency of the verification algorithm. While the typical equivalence under approximation is bisimulation,wepresent a relaxation of Markovian testing equivalence in a process algebraic framework. In this coarser setting, we show that it is particularly intuitive to manage separately three different dimensions of the approximation – execution time, event probability, and observed behavior – by illustrating in each case, results concerning the two problems mentioned above. Finally, a unified definition combining the three orthogonal aspects is provided in order to favor trade-off analyses.

Approximating Markovian Testing Equivalence

ALDINI, ALESSANDRO
2012

Abstract

Several approaches have been proposed to relax behavioral equivalences for fine-grain models including probabilities and time. All of them face two problems behind the notion of approximation, i.e., the lack of transitivity and the efficiency of the verification algorithm. While the typical equivalence under approximation is bisimulation,wepresent a relaxation of Markovian testing equivalence in a process algebraic framework. In this coarser setting, we show that it is particularly intuitive to manage separately three different dimensions of the approximation – execution time, event probability, and observed behavior – by illustrating in each case, results concerning the two problems mentioned above. Finally, a unified definition combining the three orthogonal aspects is provided in order to favor trade-off analyses.
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: https://hdl.handle.net/11576/2511149
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 1
  • ???jsp.display-item.citation.isi??? 0
social impact