On-the-fly branching bisimulation minimization for compositional analysis

Yung Pin Cheng, Hong Yi Wang, Yu Ru Cheng

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

2 Scopus citations

Abstract

Branching bisimulation minimization is often used to obtain a smaller but equivalent model for a complicated one. It is particularly useful in compositional analysis to replace a subsystem's behaviors with the minimal one so that the growth of states can be controlled in a hierarchical, divide-and-conquer manner. Nonetheless, branching bisimulation minimization is typically invoked after the whole state space is enumerated entirely. In practice, when the parallel composition engine drains too many memory resources during exploring reachable states, it causes operating systems to swap excessively (i.e., thrashing) due to the page replacement of virtual memory. When such a scenario occurs, the system degrades dramatically in performance and becomes unusable, albeit minimization is possible to abstract the whole state space into very small one. In this paper, we present a pragmatic approach to make branching bisimulation minimization on-the-fly. It minimizes the state space during composition and releases memory resources that are no longer used. Our approach allows larger systems to be verified by taking account of operating systems memory management.

Original languageEnglish
Title of host publicationImplementation and Application of Automata - 11th International Conference, CIAA 2006, Proceedings
PublisherSpringer Verlag
Pages219-229
Number of pages11
ISBN (Print)354037213X, 9783540372134
DOIs
StatePublished - 2006
Event11th International Conference on Implementation and Application of Automata, CIAA 2006 - Taipei, Taiwan
Duration: 21 Aug 200623 Aug 2006

Publication series

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

Conference

Conference11th International Conference on Implementation and Application of Automata, CIAA 2006
Country/TerritoryTaiwan
CityTaipei
Period21/08/0623/08/06

Fingerprint

Dive into the research topics of 'On-the-fly branching bisimulation minimization for compositional analysis'. Together they form a unique fingerprint.

Cite this