Abstract
In this paper we present a novel approach for solving Boolean equation systems with nested minimal and maximal fixpoints. The method works by successively eliminating variables and reducing a Boolean equation system similar to Gauß elimination for linear equation systems. It does not require backtracking techniques. Within one framework we suggest a global and a local algorithm. In the context of model checking in the modal μ-calculus the local algorithm is related to the tableau methods, but has a better worst case complexity.
Supported by Siemens AG, Corporate Research and Development, and a grant from the Hochschulsonderprogramm II.
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
H. Andersen. Model Checking and Boolean Graphs. In Proc. of ESOP'92, LNCS 582, 1992.
A. Arnold, P. Crubille. A Linear Algorithm to Solve Fixed-Point Equations on Transition Systems. Information Processing Letters, vol. 29, 57–66, 1988.
J.R. Burch, E.M. Clarke and K.L. McMillan and D.L. Dill and L.J. Hwang. Symbolic Model Checking: 1020 States and Beyond. Information and Computation, Vol. 98, pp. 142–170, 1992.
H. Bekic. Definable operations in general algebras, and the theory of automata and flow charts. In C.B.Jones, editor, Hans Bekic: Programming Languages and Their Definition, LNCS 177, 1984.
J. Bradfield. Verifying Temporal Properties of Systems. Birkhäuser,1992.
J. Bradfield, C. Stirling. Verifying Temporal Properties of Processes. Proc. of CONCUR'90, LNCS 458, 1991.
R.E. Bryant. Symbolic Boolean Manipulation with Ordered Binary-Decision Diagrams. ACM Computing Surveys, Vol. 24, No. 3, September 1992.
E. M. Clarke and E. A. Emerson. Design and synthesis of synchronization skeletons using branching time temporal logics. In LNCS 131, pp. 52–71, 1981.
E. M. Clarke, E. A. Emerson and A. P. Sistla. Automatic verification of finite-state concurrent systems using temporal logic specifications. In ACM Trans. on Programming Languages and Systems 8, pp. 244–263, 1986.
R. Cleaveland. Tableau-based model checking in the prepositional mu-calculus. Acta Informatica, Vol. 27, pp. 725–747, 1990.
R. Cleaveland and B. Steffen. A Linear-Time Model Checking Algorithm for the Alternation-Free Modal Mu-Calculus. In Proc. of CAV'91, LNCS 575, 1992.
R. Cleaveland, M. Dreimüller and B. Steffen. Faster Model Checking for the Modal Mu-Calculus. In Proc. of CAV'92, LNCS 663, 1993.
E.A. Emerson and C.-L. Lei. Efficient model checking in fragments of the prepositional mu-calculus. In Proc. of LICS'86, Computer Society Press, 1986.
D. Kozen. Results on the Prepositional μ-Calculus. TCS, Vol. 27, 1983, pp. 333–354.
K. Larsen. Efficient Local Correctness Checking. In Proc. of CAV'92, LNCS 663, 1993.
D. E. Long, A. Browne, E. M. Clarke, S. Jha, W. R. Marrero. An improved algorithm for the evaluation of fixpoint expressions. In Proc. of CAV'94, LNCS 818, 1994.
A. Mader. Tableau Recycling. In Proc. of CAV'92, LNCS 663, 1993.
S. Rudeanu. Boolean Functions and Equations. North-Holland Publishing Company, 1974.
C. Stirling. Modal and Temporal Logics. In Handbook of Logic in Computer Science, Oxford University Press, 1992.
C. Stirling and D. Walker. Local model checking in the modal mu-calculus. In Proc. of TAPSOFT'89, LNCS 351, 1989.
A. Tarski. A Lattice Theoretical Fixpoint Theorem and its Applications. In Pacific Journal of Mathematics, 5, 1955.
B. Vergauwen and J. Lewi A linear algorithm for solving fixedpoint equations on transition systems. In Proc. of CAAP'92, LNCS 581, 1992.
D. Walker. Automated Analysis of Mutual Exclusion Algorithms using CCS. Technical Report ECS-LFCS-89-91, University of Edinburgh, 1991.
Liu Xinxin. Specification and Decomposition in Concurrency. PhD Thesis, Aalborg University Center, Denmark, 1992.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1995 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Mader, A. (1995). Modal μ-calculus, model checking and Gauß elimination. In: Brinksma, E., Cleaveland, W.R., Larsen, K.G., Margaria, T., Steffen, B. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 1995. Lecture Notes in Computer Science, vol 1019. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-60630-0_4
Download citation
DOI: https://doi.org/10.1007/3-540-60630-0_4
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-60630-7
Online ISBN: 978-3-540-48509-4
eBook Packages: Springer Book Archive