Equivalence Checking for Infinite Systems Using Parameterized Boolean Equation Systems

Abstract. In this paper, we provide a transformation from the branching bisimulation problem for infinite, concurrent, data-intensive systems in linear process format, into solving Parameterized Boolean Equation Systems. We prove correctness and illustrate the approach with two examples. We also provide small adaptations to obtain similar transformations for strong and weak bisimulations and simulation equivalences.

• Type: Conference
• Year: 2007
• Where: CONCUR
• Authors: Taolue Chen, Bas Ploeger, Jaco van de Pol, Tim A. C. Willemse
• Keywords: Branching Bisimulation Problem, CONCUR 2007, Distributed And Parallel Computing, Linear Process Format, Parameterized Boolean Equation