Efficient checking of behavioural relations and modal assertions using fixed-point inversion

This paper presents an algorithm for solving Boolean fixed-point equations containing one level of nesting of minimum and maximum fixed points. The algorithm assumes that the equations of the inner fixed point is of a certain restricted kind and has a worst-case time- and space-complexity that is linear in the size of the equation system. By observing that a range of behavioral relations — in particular weak bisimulation — and modal assertions can be checked using equation systems of this restricted form, the algorithm improves on existing ad hoc constructed algorithms.Finally, we show how the key idea of inverting a fixed point can be used in decreasing the number of fixed-point iterations needed in BDD-based methods for solving the same class of problems.