The Modal -calculus, Model Checking, Equation Systems and Gauß Elimination

Angelika Mader

In TACAS, pages 44--57


The paper presents a novel approach for solving Boolean equation systems. It does not use approximation techniques and backtracking. The method works similar to Gauß elimination for linear equation systems. Homogeneous, hierarchical and alternating fixpoints are treated uniformly. In contrast to other techniques Gauß elimination leads to both a global and a local model checking algorithm within one framework.

Technical University, Munich, Germany.

Available as PostScript, DVI.

[BRICS symbol] BRICS WWW home page