Proof graphs for parameterised Boolean equation systems

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

12 Citations (Scopus)
2 Downloads (Pure)

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.
Original languageEnglish
Title of host publicationCONCUR 2013 - Concurrency Theory (24th International Conference on Concurrency Theory, Buenos Aires, Argentina, August 27-30, 2013. Proceedings)
EditorsP.R. D'Argenio, H. Melgratti
Place of PublicationBerlin
PublisherSpringer
Pages470-484
ISBN (Print)978-3-642-40183-1
DOIs
Publication statusPublished - 2013

Publication series

NameLecture Notes in Computer Science
Volume8052
ISSN (Print)0302-9743

Fingerprint Dive into the research topics of 'Proof graphs for parameterised Boolean equation systems'. Together they form a unique fingerprint.

Cite this