Bisimulation Minimization and Symbolic Model Checking

被引:0
|
作者
Kathi Fisler
Moshe Y. Vardi
机构
[1] Worcester Polytechnic Institute,Department of Computer Science
[2] Rice University,Department of Computer Science
来源
关键词
bisimulation minimization; symbolic model checking; invariant properties; on-the-fly model checking;
D O I
暂无
中图分类号
学科分类号
摘要
State space minimization techniques are crucial for combating state explosion. A variety of explicit-state verification tools use bisimulation minimization to check equivalence between systems, to minimize components before composition, or to reduce a state space prior to model checking. Experimental results on bisimulation minimization in symbolic model checking contexts, however, are mixed. This paper explores bisimulation minimization as an optimization in symbolic model checking of invariance properties. We consider three bisimulation minimization algorithms. From each, we produce a BDD-based model checker for invariant properties and compare this model checker to a conventional one based on backwards reachability. Our comparisons, both theoretical and experimental, suggest that bisimulation minimization is not viable in the context of invariance verification, because performing the minimization requires as many, if not more, computational resources as model checking the unminimized system through backwards reachability.
引用
收藏
页码:39 / 78
页数:39
相关论文
共 50 条
  • [1] Bisimulation minimization and symbolic model checking
    Fisler, K
    Vardi, MY
    [J]. FORMAL METHODS IN SYSTEM DESIGN, 2002, 21 (01) : 39 - 78
  • [2] Bisimulation and model checking
    Fisler, K
    Vardi, MY
    [J]. CORRECT HARDWARE DESIGN AND VERIFICATION METHODS, 1999, 1703 : 338 - 341
  • [3] Checking weak bisimulation and observation congruence for symbolic transition graphs
    Li, ZJ
    Chen, HW
    [J]. COMPUTER SCIENCE AND TECHNOLOGY IN NEW CENTURY, 2001, : 34 - 40
  • [4] Minimization of large state spaces using symbolic branching bisimulation
    Wimmer, Ralf
    Herbstritt, Marc
    Becker, Bernd
    [J]. PROCEEDINGS OF THE 2006 IEEE WORKSHOP ON DESIGN AND DIAGNOSTICS OF ELECTRONIC CIRCUITS AND SYSTEMS, 2006, : 8 - +
  • [5] A Parallel Relation-Based Algorithm for Symbolic Bisimulation Minimization
    Huybers, Richard
    Laarman, Alfons
    [J]. VERIFICATION, MODEL CHECKING, AND ABSTRACT INTERPRETATION, VMCAI 2019, 2019, 11388 : 535 - 554
  • [6] Symbolic transition graph and its early bisimulation checking algorithms for the π-calculus
    Zhoujun Li
    Huowang Chen
    Bingshan Wang
    [J]. Science in China Series E: Technological Sciences, 1999, 42 : 342 - 353
  • [7] Symbolic transition graph and its early bisimulation checking algorithms for the π-calculus
    李舟军
    陈火旺
    王兵山
    [J]. Science China Technological Sciences, 1999, (04) : 342 - 353
  • [8] Symbolic transition graph and its early bisimulation checking algorithms for the π-calculus
    Li, ZJ
    Chen, HW
    Wang, BS
    [J]. SCIENCE IN CHINA SERIES E-TECHNOLOGICAL SCIENCES, 1999, 42 (04): : 342 - 353
  • [9] Symbolic model checking
    McMillan, KL
    [J]. VERIFICATION OF DIGITAL AND HYBRID SYSTEM, 2000, 170 : 117 - 137
  • [10] Backward stochastic bisimulation in CSL model checking
    Sproston, J
    Donatelli, S
    [J]. QEST 2004: FIRST INTERNATIONAL CONFERENCE ON THE QUANTITATIVE EVALUATION OF SYSTEMS, PROCEEDINGS, 2004, : 220 - 229