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. As a consequence, this approach provides a general framework for designing algorithms for computing bisimulation and simulation on PLTSs. Notably, (i) we show that the standard bisimulation algorithm by Baier et al. 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. © 2011 Springer-Verlag.
CITATION STYLE
Crafa, S., & Ranzato, F. (2011). Probabilistic bisimulation and simulation algorithms by abstract interpretation. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 6756 LNCS, pp. 295–306). https://doi.org/10.1007/978-3-642-22012-8_23
Mendeley helps you to discover research relevant for your work.