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
相关论文
共 50 条
  • [1] Computable fixpoints in well-structured symbolic model checking
    Bertrand, N.
    Schnoebelen, P.
    FORMAL METHODS IN SYSTEM DESIGN, 2013, 43 (02) : 233 - 267
  • [2] On computing fixpoints in well-structured regular model checking, with applications to lossy channel systems
    Baier, Christel
    Bertrand, Nathalie
    Schnoebelen, Philippe
    Logic for Programming, Artificial Intelligence, and Reasoning, Proceedings, 2006, 4246 : 347 - 361
  • [3] Well-structured model checking of multiagent systems
    Shilov, N. V.
    Garanina, N. O.
    PERSPECTIVES OF SYSTEMS INFORMATICS, 2007, 4378 : 363 - +
  • [4] Model checking μ-Calculus in well-structured transition systems
    Kouzmin, EV
    Shilov, NV
    Sokolov, VA
    11TH INTERNATIONAL SYMPOSIUM ON TEMPORAL REPRESENTATION AND REASONING, PROCEEDINGS, 2004, : 152 - 155
  • [5] The well-structured collaborators
    Kerdellant, Christine
    HISTORIA, 2023, (923): : 28 - 30
  • [6] Well-Structured Committees
    Gupta, Sushmita
    Jain, Pallavi
    Saurabh, Saket
    PROCEEDINGS OF THE TWENTY-NINTH INTERNATIONAL JOINT CONFERENCE ON ARTIFICIAL INTELLIGENCE, 2020, : 189 - 195
  • [7] Well-structured languages
    Geeraerts, Gilles
    Raskin, Jean-Francois
    Van Begin, Laurent
    ACTA INFORMATICA, 2007, 44 (3-4) : 249 - 288
  • [8] Well-structured languages
    Gilles Geeraerts
    Jean-François Raskin
    Laurent Van Begin
    Acta Informatica, 2007, 44 : 249 - 288
  • [9] A fast and well-structured multiplier
    Kang, JY
    Gaudiot, JL
    PROCEEDINGS OF THE EUROMICRO SYSTEMS ON DIGITAL SYSTEM DESIGN, 2004, : 508 - 515
  • [10] Well-structured futures and cache locality
    Herlihy M.
    Liu Z.
    1600, Association for Computing Machinery, 2 Penn Plaza, Suite 701, New York, NY 10121-0701, United States (02):
12345