Parameterised boolean equation systems

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. 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. 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. 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. Bradfield, 1992 Bradfield, 2001, Modal logics and mu-calculi, 293 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. 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. 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). 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. 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, J.C. van de Pol, Equational Binary Decision Diagrams, in: Proc. LPAR 2000, Reunion Island, LNAI 1955, 2000, pp. 161–178. Groote, 1995, The syntax and semantics of μCRL, 26 Groote, 2001, Algebraic process verification, 1151 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, 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, Technical Report CSR 04-09, Eindhoven University of Technology, Department of Mathematics and Computer Science, 2004. Gurov, 1996, A modal μ-calculus and a proof system for value-passing processes, 149 Kozen, 1983, Results on the propositional mu-calculus, Theoret. Comput. Sci., 27, 333, 10.1016/0304-3975(82)90125-6 A. Mader, Modal μ-calculus, model checking and gaußelimination, in: E. Brinksma, R.W. Cleaveland, K.G. Larsen, T. Margaria, B. Steffen (Eds.), Tools and Algorithms for Construction and Analysis of Systems, First International Workshop, TACAS ’95, Aarhus, Denmark, Lecture Notes in Computer Science, Vol. 1019, Springer, 1995, pp. 72–88. A. Mader, Verification of Modal Properties Using Boolean Equation Systems, PhD Thesis, Technical University of Munich, 1997. Rathke, 1997, Local model checking for value-passing processes D.S. Scott, J.W. de Bakker, A theory of programs, 1969. Stirling, 2001 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. T.A.C. Willemse, Semantics and Verification in Process Algebras with Data and Timing, PhD Thesis, Eindhoven University of Technology, February 2003.