Computable fixpoints in well-structured symbolic model checking

被引：0
|
作者：
N. Bertrand
P. Schnoebelen
机构：
[1] Inria Rennes Bretagne Atlantique,
[2] LSV,undefined
[3] CNRS & ENS de Cachan,undefined
来源：
Formal Methods in System Design | 2013年 / 43卷
关键词：
Verification of well-structured systems; Verification of probabilistic systems; mu-Calculus; Infinite-state systems;
D O I：
暂无
中图分类号：
学科分类号：
摘要：
We prove a general finite-time convergence theorem for fixpoint expressions over a well-quasi-ordered set. This has immediate applications for the verification of well-structured systems, where a main issue is the computability of fixpoint expressions, and in particular for game-theoretical properties and probabilistic systems where nesting and alternation of least and greatest fixpoints are common.
引用
收藏
页码：233 / 267
页数：34
相关论文
共 7 条
  • [1] Computable fixpoints in well-structured symbolic model checking
    Bertrand, N.
    Schnoebelen, P.
    FORMAL METHODS IN SYSTEM DESIGN, 2013, 43 (02) : 233 - 267
  • [2] A symbolic semantics for abstract model checking
    Levi, F
    SCIENCE OF COMPUTER PROGRAMMING, 2001, 39 (01) : 93 - 123
  • [3] Distributed Symbolic Model Checking for μ-Calculus
    Orna Grumberg
    Tamir Heyman
    Assaf Schuster
    Formal Methods in System Design, 2005, 26 : 197 - 219
  • [4] Distributed symbolic model checking for μ-calculus
    Grumberg, O
    Heyman, T
    Schuster, A
    FORMAL METHODS IN SYSTEM DESIGN, 2005, 26 (02) : 197 - 219
  • [5] A symbolic semantics for abstract model checking
    Levi, F
    STATIC ANALYSIS, 1998, 1503 : 134 - 151
  • [6] Symbolic model checking for μ-calculus requires exponential time
    Rabinovich, A
    THEORETICAL COMPUTER SCIENCE, 2000, 243 (1-2) : 467 - 475
  • [7] From pre-historic to post-modern symbolic model checking
    Henzinger, TA
    Kupferman, O
    Qadeer, S
    FORMAL METHODS IN SYSTEM DESIGN, 2003, 23 (03) : 303 - 327
1