Probabilistic Bisimulation and Simulation Algorithms by Abstract Interpretation

act Interpretation SILVIA CRAFA FRANCESCO RANZATO University of Padova, Italy We show how bisimulation equivalence and simulation preorder on probabilistic LTSs (PLTSs), namely the main behavioural relations on probabiliseterministic processes, can be characterized by abstract interpretation. Both bisimulation and simulation can be obtained as completions of partitions rders, 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.

• Type: Journal
• Year: 2011
• Where: ICALP
• Authors: Silvia Crafa, Francesco Ranzato
• Keywords: ICALP 2011, Programming Languages, Silvia Crafa, Simulation Algorithm, University Of Padova Italy