Compositional model checking is lively

S.M.J. de Putter, A.J. Wijs

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

4 Citations (Scopus)

Abstract

Compositional model checking approaches attempt to limit state space explosion by iteratively combining behaviour of some of the components in the system and reducing the result modulo an appropriate equivalence relation. For an equivalence relation to be applicable, it should be a congruence for parallel composition where synchronisations between the components may be introduced. An equivalence relation preserving both safety and liveness properties is divergence-preserving branching bisimulation (DPBB). It is generally assumed that DPBB is a congruence for parallel composition, even in the context of synchronisations between components. However, so far, no such results have been published. This work finally proves that this is the case. Furthermore, we discuss how to safely decompose an existing LTS network in components such that the re-composition is equivalent to the original LTS network. All proofs have been mechanically verified using the Coq proof assistant. Finally, to demonstrate the effectiveness of compositional model checking with intermediate DPBB reductions, we discuss the results we obtained after having conducted a number of experiments.

Original languageEnglish
Title of host publicationFormal Aspects of Component Software
Subtitle of host publication14th International Conference, FACS 2017, Braga, Portugal, October 10-13, 2017, Proceedings
EditorsJ. Proença , M. Lumpe
Place of PublicationDordrecht
PublisherSpringer
Pages117-136
Number of pages20
ISBN (Electronic)978-3-319-68034-7
ISBN (Print)978-3-319-68033-0
DOIs
Publication statusPublished - 2017
Event14th International Conference on Formal Aspects of Component Software (FACS 2017), 10-13 October 2017, Braga, Portugal - Braga, Portugal
Duration: 10 Oct 201713 Oct 2017
http://facs2017.di.uminho.pt/

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume10487 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference14th International Conference on Formal Aspects of Component Software (FACS 2017), 10-13 October 2017, Braga, Portugal
Abbreviated titleFACS 2017
CountryPortugal
CityBraga
Period10/10/1713/10/17
Internet address

Fingerprint Dive into the research topics of 'Compositional model checking is lively'. Together they form a unique fingerprint.

Cite this