Bisimulation minimisations for Boolean equation systems

Research output: Book/ReportReportAcademic

81 Downloads (Pure)

Abstract

Boolean equation systems (BESs) have been used to encode several complex verification problems, including model checking and equivalence checking. We introduce the concepts of strong bisimulation and oblivious bisimulation for BESs, and we prove that these can be used for minimising BESs prior to solving these. Our results show that large reductions of the BESs may be obtained efficiently. Minimisation is rewarding for BESs with non-trivial alternations: the time required for solving the original BES exceeds the time required for quotienting plus the time for solving the quotient. Furthermore, we provide a verification example that demonstrates that bisimulation minimisation of a process prior to encoding the verification problem on that process as a BES can be arbitrarily less effective than minimising the BES that encodes the verification problem.
Original languageEnglish
Place of PublicationEindhoven
PublisherTechnische Universiteit Eindhoven
Number of pages22
Publication statusPublished - 2009

Publication series

NameComputer science reports
Volume0917
ISSN (Print)0926-4515

Fingerprint Dive into the research topics of 'Bisimulation minimisations for Boolean equation systems'. Together they form a unique fingerprint.

Cite this