Minimization of large state spaces using symbolic branching bisimulation

Author

Wimmer, Ralf ; Herbstritt, Marc ; Becker, Bernd

Author_Institution

Inst. of Comput. Sci., Albert Ludwigs Univ.

fYear

2006

fDate

18-21 April 2006

Firstpage

7

Lastpage

12

Abstract

Bisimulations in general are a powerful concept to minimize large finite state systems regarding some well-defined observational behavior. In contrast to strong bisimulation, for branching bisimulation there are only tools available that work on an explicit state space representation. In this work, we present for the first time a symbolic approach for branching bisimulation that uses BDDs as basic data structure and that is based on the concept of signature refinement. First experimental results for problem instances derived from process algebraic system descriptions show the feasibility and the robustness of our approach

Keywords

binary decision diagrams; bisimulation equivalence; data structures; finite state machines; minimisation; process algebra; BDD; data structure; finite state systems; large state spaces; process algebraic system; signature refinement; state space minimization; state space representation; symbolic branching bisimulation; Algebra; Boolean functions; Computer science; Concrete; Context modeling; Data structures; Iterative algorithms; Robustness; State-space methods; Vehicles;

fLanguage

English

Publisher

ieee

Conference_Titel

Design and Diagnostics of Electronic Circuits and systems, 2006 IEEE

Conference_Location

Prague

Print_ISBN

1-4244-0185-2

Type

conf

DOI

10.1109/DDECS.2006.1649562

Filename

1649562