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 条
  • [41] Symbolic model checking
    McMillan, KL
    VERIFICATION OF DIGITAL AND HYBRID SYSTEM, 2000, 170 : 117 - 137
  • [42] Well-structured program graphs and the issue of local computations
    Klopotek, MA
    INTELLIGENT INFORMATION SYSTEMS 2002, PROCEEDINGS, 2002, 17 : 365 - 368
  • [43] Ordinal theory for expressiveness of well-structured transition systems
    Bonnet, Remi
    Finkel, Alain
    Haddad, Serge
    Rosa-Velardo, Fernando
    INFORMATION AND COMPUTATION, 2013, 224 : 1 - 22
  • [44] A well-structured framework for analysing petri net extensions
    Finkel, A
    McKenzie, P
    Picaronny, C
    INFORMATION AND COMPUTATION, 2004, 195 (1-2) : 1 - 29
  • [45] Decidability Results for Well-structured Graph Transformation Systems
    Koenig, Barbara
    Stueckrath, Jan
    ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2013, (140): : 87 - 88
  • [46] Structural and Behavioral Properties of Well-Structured Workflow Nets
    Gou, Zhaolong
    Yamaguchi, Shingo
    IEICE TRANSACTIONS ON FUNDAMENTALS OF ELECTRONICS COMMUNICATIONS AND COMPUTER SCIENCES, 2017, E100A (02) : 421 - 426
  • [47] Initial and concurrent planning in solutions to well-structured problems
    Davies, SP
    QUARTERLY JOURNAL OF EXPERIMENTAL PSYCHOLOGY SECTION A-HUMAN EXPERIMENTAL PSYCHOLOGY, 2003, 56 (07): : 1147 - 1164
  • [48] Fundamental structures in well-structured infinite transition systems
    Finkel, A
    Schnoebelen, P
    LATIN '98: THEORETICAL INFORMATICS, 1998, 1380 : 102 - 118
  • [49] Parameterized Verification of Coverability in Well-Structured Broadcast Networks
    Balasubramanian, A. R.
    ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2018, (277): : 133 - 146
  • [50] Meta-kernelization using well-structured modulators
    Eiben, Eduard
    Ganian, Robert
    Szeider, Stefan
    DISCRETE APPLIED MATHEMATICS, 2018, 248 : 153 - 167
12345