Bisimulation minimisations for Boolean equation systems

Onderzoeksoutput: Hoofdstuk in Boek/Rapport/CongresprocedureConferentiebijdrageAcademicpeer review

6 Citaten (Scopus)

Samenvatting

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 idempotence-identifying 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 mostly 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.
Originele taal-2Engels
TitelHardware and Software: Verification and Testing (5th International Haifa Verification Conference, HVC 2009, Haifa, Israel, October 19-22, 2009. Revised selected papers)
RedacteurenK. Namjoshi, A. Zeller, A. Ziv
Plaats van productieBerlin
UitgeverijSpringer
Pagina's102-116
ISBN van geprinte versie978-3-642-19236-4
DOI's
StatusGepubliceerd - 2011

Publicatie series

NaamLecture Notes in Computer Science
Volume6405
ISSN van geprinte versie0302-9743

Vingerafdruk Duik in de onderzoeksthema's van 'Bisimulation minimisations for Boolean equation systems'. Samen vormen ze een unieke vingerafdruk.

Citeer dit