Affordable Access

Equivalence checking for infinite systems using parameterized Boolean equation systems

Publication Date
  • Computer Science
  • Mathematics


LNCS 4703 - Equivalence Checking for Infinite Systems Using Parameterized Boolean Equation Systems Equivalence Checking for Infinite Systems Using Parameterized Boolean Equation Systems Taolue Chen1,�, Bas Ploeger2,��, Jaco van de Pol1,2, and Tim A.C. Willemse2,� � � 1 CWI, Department of Software Engineering, P.O. Box 94079, 1090 GB Amsterdam, The Netherlands 2 Eindhoven University of Technology, Design and Analysis of Systems Group, P.O. Box 513, 5600 MB Eindhoven, The Netherlands Abstract. In this paper, we provide a transformation from the branching bisim- ulation problem for infinite, concurrent, data-intensive systems in linear process format, into solving Parameterized Boolean Equation Systems. We prove cor- rectness, and illustrate the approach with an unbounded queue example. We also provide some adaptations to obtain similar transformations for weak bisimulation and simulation equivalence. 1 Introduction A standard approach for verifying the correctness of a computer system or a communi- cation protocol is the equivalence-based methodology. This framework was introduced by Milner [23] and has been intensively explored in process algebra. One proceeds by establishing two descriptions (models) for one system: a specification and an implemen- tation. The former describes the desired high-level behavior, while the latter provides lower-level details indicating how this behavior is to be achieved. Then an implemen- tation is said to be correct, if it behaves “the same as” its specification. Similarly, one could check whether the implementation has “at most” the behavior allowed by the specification. Several behavioral equivalences and preorders have been introduced to relate specifications and implementations, supporting different notions of observability. These include strong, weak [24], and branching bisimulation [11,4]. Equivalence Checking for Finite Systems. Checking strong bisimulation of finite sys- tems can be done very efficiently. The basic algorithm is the we

There are no comments yet on this publication. Be the first to share your thoughts.