The Modal -calculus, Model Checking, Equation Systems and
In TACAS, pages
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,
BRICS WWW home page