@inproceedings{93bff0dd38be4736b07f666b103067c3,

title = "Proof graphs for parameterised Boolean equation systems",

abstract = "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.",

author = "S. Cranen and T.A.C. Willemse and S.P. Luttik",

year = "2013",

doi = "10.1007/978-3-642-40184-8_33",

language = "English",

isbn = "978-3-642-40183-1",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "470--484",

editor = "P.R. D'Argenio and H. Melgratti",

booktitle = "CONCUR 2013 - Concurrency Theory (24th International Conference on Concurrency Theory, Buenos Aires, Argentina, August 27-30, 2013. Proceedings)",

address = "Germany",

}