Parameterised Boolean equation systems (PBESs) can be used for solving a variety of verification problems such as model checking and equivalence checking problems. The definition of solution for a PBES is notoriously difficult to understand, which makes them hard to work with. Tan and Cleaveland proposed a notion of proof for Boolean equation systems they call support sets. We show that an adapted notion of support sets called proof graphs gives an alternative characterisation of the solution to a PBES, and prove that minimising proof graphs is NP-hard. Finally, we explain how proof graphs may be used in practice and illustrate how they can be used in equivalence checking to generate distinguishing formulas.
|Title of host publication||CONCUR 2013 - Concurrency Theory (24th International Conference on Concurrency Theory, Buenos Aires, Argentina, August 27-30, 2013. Proceedings)|
|Editors||P.R. D'Argenio, H. Melgratti|
|Place of Publication||Berlin|
|Publication status||Published - 2013|
|Name||Lecture Notes in Computer Science|