Parameterised boolean equation systems

We introduce a new equivalence between equation systems, because existing equivalences are not compositional. We present techniques similar to Gauß elimination as outlined in [Mader, Lecture Notes in Computer Science, Vol. 1019, 1995, pp. 72-88] that allow to solve each equation system provided a single equation can be solved. We give several techniques for solving single equations, such as approximation (known), patterns (new) and invariants (new). Finally, we provide several small but illustrative examples of verifications of modal μ-calculus formulas on concrete processes to show the use of the techniques.