Abstract
This paper presents a technique for the resolution of alternating disjunctive/conjunctive boolean equation systems. The technique can be used to solve various verification problems on finite-state concurrent systems, by encoding the problems as boolean equation systems and determining their local solutions. The main contribution of this paper is that a recent resolution technique from [13] for disjunctive/conjunctive boolean equation systems is extended to the more general disjunctive/conjunctive forms with alternation. Our technique has the time complexity O(m+n 2), where m is the number of alternation free variables occurring in the equation system and n the number of alternating variables. We found that many μ-calculus formulas with alternating fixed points occurring in the literature can be encoded as boolean equation systems of disjunctive/conjunctive forms. Practical experiments show that we can verify alternating formulas on state spaces that are orders of magnitudes larger than reported up till now.
Chapter PDF
Similar content being viewed by others
References
Andersen, H.R.: Model checking and boolean graphs. Theoretical Computer Science 126, 3–30 (1994)
Arnold, A., Crubille, P.: A linear time algorithm to solve fixed-point equations on transition systems. Information Processing Letters 29, 57–66 (1988)
Arnold, A., Niwinski, D.: Rudiments of μ-calculus. Studies in Logic and the foundations of mathematics, vol. 146. Elsevier, Amsterdam (2001)
Bradfield, J., Stirling, C.: Modal Logics and mu-Calculi: An introduction. In: Bergstra, J.A., Ponse, A., Smolka, S.A. (eds.) Handbook of Process Algebra. ch. 4, Elsevier, Amsterdam (2001)
Bhat, G., Cleaveland, R.: Efficient local model-checking for fragments of the modal μ-calculus. In: Margaria, T., Steffen, B. (eds.) TACAS 1996. LNCS, vol. 1055, pp. 107–126. Springer, Heidelberg (1996)
Cleaveland, R., Steffen, B.: Computing Behavioural relations logically. In: Leach Albert, J., Monien, B., Rodríguez-Artalejo, M. (eds.) ICALP 1991. LNCS, vol. 510, pp. 127–138. Springer, Heidelberg (1991)
Emerson, E.A., Jutla, C., Sistla, A.P.: On model checking for fragments of the μ-calculus. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol. 697, pp. 385–396. Springer, Heidelberg (1993)
Emerson, E.A., Jutla, C., Sistla, A.P.: On model checking for the μ-calculus and its fragments. Theoretical Computer Science 258, 491–522 (2001)
Jurdzinski, M.: Deciding the winner in parity games is in UP ∩co−UP. Information Processing Letters 68, 119–124 (1998)
Kozen, D.: Results on the propositional μ-calculus. Theoretical computer Science 27, 333–354 (1983)
Liu, X., Ramakrishnan, C.R., Smolka, S.A.: Fully Local and Efficient Evaluation of Alternating Fixed Points. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol. 1384, p. 5. Springer, Heidelberg (1998)
Mader, A.: Verification of Modal Properties using Boolean Equation Systems. PhD thesis, Technical University of Munich (1997)
Mateescu, R.: A Generic On-the-Fly Solver for Alternation-Free Boolean Equation Systems. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 81–96. Springer, Heidelberg (2003)
Steffen, B., Classen, A., Klein, M., Knoop, J., Margaria, T.: The fixpoint analysis machine. In: Lee, I., Smolka, S.A. (eds.) CONCUR 1995. LNCS, vol. 962, pp. 72–87. Springer, Heidelberg (1995)
Tarjan, R.: Depth-First Search and Linear Graph Algorithms. SIAM J. Computing 1(2) (June 1972)
Vergauwen, B., Lewi, J.: A linear algorithm for solving fixed-point equations on transition systems. In: Raoult, J.-C. (ed.) CAAP 1992. LNCS, vol. 581, pp. 321–341. Springer, Heidelberg (1992)
Vergauwen, B., Lewi, J.: Efficient Local Correctness Checking for Single and Alternating Boolean Equation Systems. In: Shamir, E., Abiteboul, S. (eds.) ICALP 1994. LNCS, vol. 820, Springer, Heidelberg (1994)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Groote, J.F., Keinänen, M. (2004). Solving Disjunctive/Conjunctive Boolean Equation Systems with Alternating Fixed Points. In: Jensen, K., Podelski, A. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2004. Lecture Notes in Computer Science, vol 2988. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-24730-2_33
Download citation
DOI: https://doi.org/10.1007/978-3-540-24730-2_33
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-21299-7
Online ISBN: 978-3-540-24730-2
eBook Packages: Springer Book Archive