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 an unbounded queue example. We also provide some adaptations to obtain similar transformations for weak bisimulation and simulation equivalence.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Alur, R., Dill, D.L.: A theory of timed automata. Theoretical Computer Science 126(2), 183–235 (1994)
Andersen, H.R.: Model checking and boolean graphs. Theoretical Computer Science 126(1), 3–30 (1994)
Andersen, H.R., Vergauwen, B.: Efficient checking of behavioural relations and modal assertions using fixed-point inversion. In: Wolper, P. (ed.) CAV 1995. LNCS, vol. 939, pp. 142–154. Springer, Heidelberg (1995)
Basten, T.: Branching bisimilarity is an equivalence indeed! Information Processing Letters 58, 141–147 (1996)
Bolognesi, T., Brinksma, E.: Introduction to the ISO specification language LOTOS. Computer Networks 14, 25–59 (1987)
Chandy, K.M., Misra, J.: Parallel Program Design: A Foundation. Addison-Wesley, Reading (1988)
Chen, T., Ploeger, B., van de Pol, J., Willemse, T.A.C.: Equivalence checking for infinite systems using parameterized boolean equation systems. CS-Report 07-14, Technische Universiteit Eindhoven (2007)
Cleaveland, R., Steffen, B.: Computing behavioural relations, logically. In: Leach Albert, J., Monien, B., Rodríguez-Artalejo, M. (eds.) Automata, Languages and Programming. LNCS, vol. 510, pp. 127–138. Springer, Heidelberg (1991)
Fokkink, W., Pang, J., van de Pol, J.: Cones and foci: A mechanical framework for protocol verification. Formal Methods in System Design 29(1), 1–31 (2006)
van Glabbeek, R.: The Linear Time - Branching Time Spectrum II. In: Best, E. (ed.) CONCUR 1993. LNCS, vol. 715, pp. 66–81. Springer, Heidelberg (1993)
van Glabbeek, R.J., Weijland, W.P.: Branching time and abstraction in bisimulation semantics. Journal of the ACM 43, 555–600 (1996)
Groote, J.F., Mateescu, R.: Verification of temporal properties of processes in a setting with data. In: Haeberer, A.M. (ed.) AMAST 1998. LNCS, vol. 1548, pp. 74–90. Springer, Heidelberg (1998)
Groote, J.F., van de Pol, J.: A bounded retransmission protocol for large data packets. In: Nivat, M., Wirsing, M. (eds.) AMAST 1996. LNCS, vol. 1101, pp. 536–550. Springer, Heidelberg (1996)
Groote, J.F., Reniers, M.: Algebraic process verification. In: Bergstra, J.A., Ponse, A., Smolka, S.A. (eds.) Handbook of Process Algebra, pp. 1151–1208. Elsevier, Amsterdam (2001)
Groote, J.F., Vaandrager, F.W.: An efficient algorithm for branching bisimulation and stuttering equivalence. In: Paterson, M.S. (ed.) Automata, Languages and Programming. LNCS, vol. 443, pp. 626–638. Springer, Heidelberg (1990)
Groote, J.F., Willemse, T.A.C.: Model-checking processes with data. Science of Computer Programming 56(3), 251–273 (2005)
Groote, J.F., Willemse, T.A.C.: Parameterised boolean equation systems. Theoretical Computer Science 343(3), 332–369 (2005)
Kwak, H., Choi, J., Lee, I., Philippou, A.: Symbolic weak bisimulation for value-passing calculi. Technical Report, MS-CIS-98-22, Department of Computer and Information Science, University of Pennsylvania (1998)
Lin, H.: Symbolic transition graph with assignment. In: Sassone, V., Montanari, U. (eds.) CONCUR 1996. LNCS, vol. 1119, pp. 50–65. Springer, Heidelberg (1996)
Lynch, N., Tuttle, M.: An introduction to input/output automata. CWI Quarterly 2(3), 219–246 (1989)
Mader, A.: Verification of modal properties using boolean equation systems. PhD Thesis, VERSAL 8, Bertz Verlag, Berlin (1997)
Mateescu, R.: A generic on-the-fly solver for alternation-free boolean equation systems. In: Garavel, H., Hatcliff, J. (eds.) ETAPS 2003 and TACAS 2003. LNCS, vol. 2619, pp. 81–96. Springer, Heidelberg (2003)
Milner, R.: A Calculus of Communicating Systems. Springer, Heidelberg (1980)
Milner, R.: Communication and Concurrency. Prentice-Hall, Englewood Cliffs (1989)
Milner, R., Parrow, J., Walker, D.: A calculus of mobile processes (Part I/II). Information and Computation 100(1), 1–77 (1992)
Paige, R., Tarjan, R.: Three partition refinement algorithms. SIAM Journal of Computing 16(6), 973–989 (1987)
Tarski, A.: A lattice-theoretical fixpoint theorem and its applications. Pacific Journal of Mathematics 5(2), 285–309 (1955)
Zhang, D., Cleaveland, R.: Fast generic model-checking for data-based systems. In: Wang, F. (ed.) FORTE 2005. LNCS, vol. 3731, pp. 83–97. Springer, Heidelberg (2005)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Chen, T., Ploeger, B., van de Pol, J., Willemse, T.A.C. (2007). Equivalence Checking for Infinite Systems Using Parameterized Boolean Equation Systems. In: Caires, L., Vasconcelos, V.T. (eds) CONCUR 2007 – Concurrency Theory. CONCUR 2007. Lecture Notes in Computer Science, vol 4703. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-74407-8_9
Download citation
DOI: https://doi.org/10.1007/978-3-540-74407-8_9
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-74406-1
Online ISBN: 978-3-540-74407-8
eBook Packages: Computer ScienceComputer Science (R0)