We analyse the problem of solving Boolean equation systems through the use
of structure graphs. The latter are obtained through an elegant
set of Plotkin-style deduction rules. Our main contribution is that
we show that equation systems with bisimilar structure graphs have the
same solution. We show that our work conservatively extends earlier work,
conducted by Keiren and Willemse, in which dependency graphs were
used to analyse a subclass of Boolean equation systems, viz., equation
systems in standard recursive form. We illustrate our approach by
a small example, demonstrating the effect of simplifying an equation system
through minimisation of its structure graph. |