Minimization of Large State Spaces using Symbolic Branching Bisimulation

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.

• Type: Conference
• Year: 2006
• Where: DDECS
• Authors: Ralf Wimmer, Marc Herbstritt, Bernd Becker
• Keywords: DDECS 2006, Explicit State Space, Hardware, Strong Bisimulation, Well-defined Observational Behavior