Modal µ-Calculus, Model Checking and Gauß Elimination

Mader, Angelika (1995) Modal µ-Calculus, Model Checking and Gauß Elimination. In: First International Workshop on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 1995, May 19-20, 1995, Aarhus, Denmark.

Preview

PDF
818Kb

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.
Item Type:	Conference or Workshop Item
Copyright:	© 1995 Springer-Verlag
Faculty:	Electrical Engineering, Mathematics and Computer Science (EEMCS)
Research Group:	Robotics and Mechatronics (CE)
Link to this item:	http://purl.utwente.nl/publications/56275
Official URL:	http://dx.doi.org/10.1007/3-540-60630-0_4
Export this item as:	BibTeX EndNote HTML Citation Reference Manager

Show download statistics for this publication

Repository Staff Only: item control page