Analysis of Boolean Equation Systems through Structure Graphs

TL;DR

This paper introduces a novel method for analyzing Boolean equation systems using structure graphs derived from deduction rules, demonstrating that bisimilar graphs imply identical solutions and enabling system simplification.

Contribution

It extends previous dependency graph methods to a broader class of Boolean equation systems using structure graphs and bisimulation, providing a new approach for system analysis and minimization.

Findings

Bisimilar structure graphs guarantee identical solutions.

The approach extends earlier dependency graph analysis to more general systems.

Demonstrated system simplification through structure graph minimization.

Abstract

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.