We show how bisimulation equivalence and simulation preorder on probabilistic LTSs (PLTSs), namely the main behavioural relations on probabilistic nondeterministic processes, can be characterized by abstract interpretation. Both bisimulation and simulation can be obtained as completions of partitions and preorders, viewed as abstract domains, w.r.t. a pair of concrete functions that encode a PLTS. This approach provides a general framework for designing algorithms that compute bisimulation and simulation on PLTSs. Notably, (i) we show that the standard bisimulation algorithm by Baier et al. (2000) can be viewed as an instance of such a framework and (ii) we design a new efficient simulation algorithm that improves the state of the art.

Bisimulation and simulation algorithms on probabilistic transition systems by abstract interpretation

CRAFA, SILVIA;RANZATO, FRANCESCO
2012

Abstract

We show how bisimulation equivalence and simulation preorder on probabilistic LTSs (PLTSs), namely the main behavioural relations on probabilistic nondeterministic processes, can be characterized by abstract interpretation. Both bisimulation and simulation can be obtained as completions of partitions and preorders, viewed as abstract domains, w.r.t. a pair of concrete functions that encode a PLTS. This approach provides a general framework for designing algorithms that compute bisimulation and simulation on PLTSs. Notably, (i) we show that the standard bisimulation algorithm by Baier et al. (2000) can be viewed as an instance of such a framework and (ii) we design a new efficient simulation algorithm that improves the state of the art.
File in questo prodotto:
File Dimensione Formato  
CrafaRanzato.pdf

accesso aperto

Tipologia: Preprint (submitted version)
Licenza: Accesso libero
Dimensione 247.09 kB
Formato Adobe PDF
247.09 kB Adobe PDF Visualizza/Apri
Pubblicazioni consigliate

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/11577/2493919
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 7
  • ???jsp.display-item.citation.isi??? 6
  • OpenAlex ND
social impact