Equivalence Checking for Infinite Systems Using Parameterized Boolean Equation Systems

In this paper, the authors provide a transformation from the branching bisimulation problem for infinite, concurrent, data-intensive systems in linear process format, into solving Parameterized Boolean Equation Systems. They prove correctness and illustrate the approach with two examples. They also provide small adaptations to obtain similar transformations for strong and weak bisimulations and simulation equivalences. A standard approach for verifying the correctness of a computer system or a communication protocol is the equivalence-based methodology. This framework was introduced by Milner and has been intensively explored in process algebra. One proceeds by establishing two descriptions (models) for one system: a specification and an implementation. The former describes the desired high-level behavior, while the latter provides lower-level details indicating how this behavior is to be achieved.