×

Parameterised Boolean equation systems. (English) Zbl 1077.68061

Summary: Boolean equation system are a useful tool for verifying formulas from modal \(\mu\)-calculus on transition systems [see (*) A. Mader, Lect. Notes Comput. Sci. 1019, 72–88 (1995) for an excellent treatment]. We are interested in an extension of Boolean equation systems with data. This allows us to formulate and prove a substantially wider range of properties on much larger and even infinite state systems. In previous works it has been outlined how to transform a modal formula and a process, both containing data, to a so-called parameterised Boolean equation system, or equation system for short. In this article we focus on techniques to solve such equation systems.
We introduce a new equivalence between equation systems, because existing equivalences are not compositional. We present techniques similar to Gauß elimination as outlined in (*) that allow us to solve each equation system provided a single equation can be solved. We give several techniques for solving single equations, such as approximation (known), patterns (new) and invariants (new). Finally, we provide several small but illustrative examples of verifications of modal \(\mu \)-calculus formulas on concrete processes to show the use of the techniques.

MSC:

68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
68Q60 Specification and verification (program logics, model checking, etc.)
PDFBibTeX XMLCite
Full Text: DOI Link

References:

[1] P. Abdulla, A. Bouajjani, B. Jonsson, On-the-fly analysis of systems with unbounded, lossy fifo channels, in: A.J. Hu, M.Y. Vardi (Eds.), 10th Internat. Conf. on Computer Aided Verification, CAV’98, Lecture Notes in Computer Science, Vol. 1427, Springer, 1998, pp. 305-318.; P. Abdulla, A. Bouajjani, B. Jonsson, On-the-fly analysis of systems with unbounded, lossy fifo channels, in: A.J. Hu, M.Y. Vardi (Eds.), 10th Internat. Conf. on Computer Aided Verification, CAV’98, Lecture Notes in Computer Science, Vol. 1427, Springer, 1998, pp. 305-318.
[2] H. Bekič, Definable operations in general algebras, and the theory of automata and flow charts, in: C.B. Jones (Ed.), Programming Languages and Their Definition - Hans Bekič (1936-1982), Lecture Notes in Computer Science, Vol. 177, Springer, 1984, pp. 30-55.; H. Bekič, Definable operations in general algebras, and the theory of automata and flow charts, in: C.B. Jones (Ed.), Programming Languages and Their Definition - Hans Bekič (1936-1982), Lecture Notes in Computer Science, Vol. 177, Springer, 1984, pp. 30-55.
[3] M.A. Bezem, J.F. Groote, Invariants in process algebra with data, in: B. Jonsson, J. Parrow (Eds.), Proc. Concur’94, Uppsala, Sweden, Lecture Notes in Computer Science, Vol. 836, Springer, 1994, pp. 401-416.; M.A. Bezem, J.F. Groote, Invariants in process algebra with data, in: B. Jonsson, J. Parrow (Eds.), Proc. Concur’94, Uppsala, Sweden, Lecture Notes in Computer Science, Vol. 836, Springer, 1994, pp. 401-416.
[4] B. Boigelot, P. Godefroid, B. Willems, P. Wolper, The power of qdds, in: P. van Hentenryck (Ed.), Static Analysis, 4th Internat. Symp. SAS’97, Lecture Notes in Computer Science, Vol. 1302, Springer, 1997, pp. 172-186.; B. Boigelot, P. Godefroid, B. Willems, P. Wolper, The power of qdds, in: P. van Hentenryck (Ed.), Static Analysis, 4th Internat. Symp. SAS’97, Lecture Notes in Computer Science, Vol. 1302, Springer, 1997, pp. 172-186.
[5] Bradfield, J. C., Verifying Temporal Properties of Systems, Progress in Theoretical Computer Science (1992), Birkhäuser
[6] Bradfield, J.; Stirling, C., Modal logics and mu-calculian introduction, (Bergstra, J. A.; Ponse, A.; Smolka, S. A., Handbook of Process Algebra (2001), Elsevier), 293-330 · Zbl 1002.03021
[7] R.E. Bryant, S.K. Lahiri, S.A. Seshia, Modeling and verifying systems using a logic of counter arithmetic with lambda expressions and uninterpreted functions, in: 14th Internat. Conf. on Computer Aided Verification, CAV 2002, Lecture Notes in Computer Science, Vol. 2404, Springer, 2002, pp. 78-92.; R.E. Bryant, S.K. Lahiri, S.A. Seshia, Modeling and verifying systems using a logic of counter arithmetic with lambda expressions and uninterpreted functions, in: 14th Internat. Conf. on Computer Aided Verification, CAV 2002, Lecture Notes in Computer Science, Vol. 2404, Springer, 2002, pp. 78-92. · Zbl 1010.68522
[8] T. Bultan, R. Gerber, W. Pugh, Symbolic model checking of infinite state systems using pressburger arithmetic, in: O. Grumberg (Ed.), Ninth Internat. Conf. on Computer Aided Verification, CAV’97, Lecture Notes in Computer Science, Vol. 1254, Springer, 1997, pp. 400-411.; T. Bultan, R. Gerber, W. Pugh, Symbolic model checking of infinite state systems using pressburger arithmetic, in: O. Grumberg (Ed.), Ninth Internat. Conf. on Computer Aided Verification, CAV’97, Lecture Notes in Computer Science, Vol. 1254, Springer, 1997, pp. 400-411.
[9] P. Cousot, Semantic foundations of program analysis, in: S.S. Muchnick, N.D. Jones (Eds.), Program Flow Analysis: Theory and Applications, Prentice-Hall, Englewood Cliffs, New Jersey, USA, 1981, pp. 303-342 (Chapter 10).; P. Cousot, Semantic foundations of program analysis, in: S.S. Muchnick, N.D. Jones (Eds.), Program Flow Analysis: Theory and Applications, Prentice-Hall, Englewood Cliffs, New Jersey, USA, 1981, pp. 303-342 (Chapter 10).
[10] E.A. Emerson, C.-L. Lei, Efficient model checking in fragments of the propositional mu-calculus, in: First IEEE Symp. Logic in Computer Science, LICS’86, IEEE Computer Society Press, 1986, pp. 267-278.; E.A. Emerson, C.-L. Lei, Efficient model checking in fragments of the propositional mu-calculus, in: First IEEE Symp. Logic in Computer Science, LICS’86, IEEE Computer Society Press, 1986, pp. 267-278.
[11] J.F. Groote, R. Mateescu, Verification of temporal properties of processes in a setting with data, in: A.M. Haeberer (Ed.), AMAST’98, Lecture Notes in Computer Science, Vol. 1548, Springer, 1999, pp. 74-90.; J.F. Groote, R. Mateescu, Verification of temporal properties of processes in a setting with data, in: A.M. Haeberer (Ed.), AMAST’98, Lecture Notes in Computer Science, Vol. 1548, Springer, 1999, pp. 74-90. · Zbl 0926.03036
[12] J.F. Groote, J.C. van de Pol, Equational Binary Decision Diagrams, in: Proc. LPAR 2000, Reunion Island, LNAI 1955, 2000, pp. 161-178.; J.F. Groote, J.C. van de Pol, Equational Binary Decision Diagrams, in: Proc. LPAR 2000, Reunion Island, LNAI 1955, 2000, pp. 161-178. · Zbl 0988.68590
[13] Groote, J. F.; Ponse, A., The syntax and semantics of \(\mu\) CRL, (Ponse, A.; Verhoef, C.; van Vlijmen, S. F.M., Algebra of Communicating Processes ’94, Workshops in Computing Series (1995), Springer), 26-62
[14] Groote, J. F.; Reniers, M. A., Algebraic process verification, (Bergstra, J. A.; Ponse, A.; Smolka, S. A., Handbook of Process Algebra (2001), Elsevier: Elsevier North-Holland), 1151-1208, (Chapter 17) · Zbl 1035.68069
[15] J.F. Groote, T.A.C. Willemse, Model-checking processes with data. Sci. Comput. Program. 56 (2005) 251-273.; J.F. Groote, T.A.C. Willemse, Model-checking processes with data. Sci. Comput. Program. 56 (2005) 251-273. · Zbl 1082.68067
[16] J.F. Groote, T.A.C. Willemse, Parameterised boolean equation systems (Extended Abstract), in: P. Gardner, N. Yoshida (Eds.), Proc. of CONCUR 2004, London, Lecture Notes in Computer Science, Vol. 3170, Springer, 2004, pp. 308-324.; J.F. Groote, T.A.C. Willemse, Parameterised boolean equation systems (Extended Abstract), in: P. Gardner, N. Yoshida (Eds.), Proc. of CONCUR 2004, London, Lecture Notes in Computer Science, Vol. 3170, Springer, 2004, pp. 308-324. · Zbl 1099.68670
[17] J.F. Groote, T.A.C. Willemse, Parameterised boolean equation systems, Technical Report CSR 04-09, Eindhoven University of Technology, Department of Mathematics and Computer Science, 2004.; J.F. Groote, T.A.C. Willemse, Parameterised boolean equation systems, Technical Report CSR 04-09, Eindhoven University of Technology, Department of Mathematics and Computer Science, 2004. · Zbl 1099.68670
[18] Gurov, D.; Berezin, S.; Kapron, B., A modal \(\mu \)-calculus and a proof system for value-passing processes, (Proc. Infinity, Workshop on Verification of Infinite State Systems, Pisa (1996)), 149-163
[19] Kozen, D., Results on the propositional mu-calculus, Theoret. Comput. Sci., 27, 333-354 (1983) · Zbl 0553.03007
[20] A. Mader, Modal \(\operatorname{Μ;} \); A. Mader, Modal \(\operatorname{Μ;} \)
[21] A. Mader, Verification of Modal Properties Using Boolean Equation Systems, PhD Thesis, Technical University of Munich, 1997.; A. Mader, Verification of Modal Properties Using Boolean Equation Systems, PhD Thesis, Technical University of Munich, 1997.
[22] Rathke, J.; Hennessy, M., Local model checking for value-passing processes, (Proc. of TACS’97, the Internat. Symp. on Theoretical Aspects of Computer Software, Sendai, 1997 (1997)) · Zbl 0885.03021
[23] D.S. Scott, J.W. de Bakker, A theory of programs, 1969.; D.S. Scott, J.W. de Bakker, A theory of programs, 1969.
[24] Stirling, C., Modal and Temporal Properties of Processes, Texts in Computer Science (2001), Springer
[25] B. Vergauwen, J. Lewi, Efficient local correctness checking for single and alternating boolean equation systems, in: S. Abiteboul, E. Shamir (Eds.), Proc. ICALP’94, Lecture Notes in Computer Science, Vol. 820, Springer, 1994, pp. 302-315.; B. Vergauwen, J. Lewi, Efficient local correctness checking for single and alternating boolean equation systems, in: S. Abiteboul, E. Shamir (Eds.), Proc. ICALP’94, Lecture Notes in Computer Science, Vol. 820, Springer, 1994, pp. 302-315. · Zbl 1422.68174
[26] T.A.C. Willemse, Semantics and Verification in Process Algebras with Data and Timing, PhD Thesis, Eindhoven University of Technology, February 2003.; T.A.C. Willemse, Semantics and Verification in Process Algebras with Data and Timing, PhD Thesis, Eindhoven University of Technology, February 2003.
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.