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
来源
关键词
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 条
  • [21] A Small yet Well-Structured Step
    Jiang, Jovia
    Liu, Tianyu
    Osterland, Anke
    Squillaci, Marco Antonio
    Wen, Xi
    SMALL STRUCTURES, 2022, 3 (01):
  • [22] The importance of a well-structured strategy of transitions
    Verplaetze, A
    FIFTY YEARS AFTER BRETTON WOODS: THE NEW CHALLENGE OF EAST-WEST PARTNERSHIP FOR ECONOMIC PROGRESS, 1996, : 232 - 234
  • [23] The Structure of Ill-Structured (and Well-Structured) Problems Revisited
    Stephen K. Reed
    Educational Psychology Review, 2016, 28 : 691 - 716
  • [24] Synthesis and Assembly of Well-structured Hybrid Microgels
    Suzuki, Daisuke
    Kawaguchi, Haruma
    TRANSACTIONS OF THE MATERIALS RESEARCH SOCIETY OF JAPAN, VOL 33, NO 2, 2008, 33 (02): : 365 - 368
  • [25] Termination and Boundedness for Well-Structured Pushdown Systems
    Lei, Suhua
    Cai, Xiaojuan
    Ogawa, Mizuhito
    2016 10TH INTERNATIONAL SYMPOSIUM ON THEORETICAL ASPECTS OF SOFTWARE ENGINEERING (TASE), 2016, : 22 - 29
  • [26] WELL-STRUCTURED FHMA CODEBOOKS - A GEOMETRIC APPROACH
    JEVTIC, DB
    IEEE TRANSACTIONS ON COMMUNICATIONS, 1991, 39 (10) : 1427 - 1432
  • [27] The Structure of Ill-Structured (and Well-Structured) Problems Revisited
    Reed, Stephen K.
    EDUCATIONAL PSYCHOLOGY REVIEW, 2016, 28 (04) : 691 - 716
  • [28] Resilience of Well-structured Graph Transformation Systems
    Oezkan, Okan
    Wuerdemann, Nick
    ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2021, (350): : 69 - 88
  • [29] Parallel Degree of Well-Structured Workflow Nets
    Qu, Nan
    Yamaguchi, Shingo
    Ge, Qi-Wei
    IEICE TRANSACTIONS ON FUNDAMENTALS OF ELECTRONICS COMMUNICATIONS AND COMPUTER SCIENCES, 2010, E93A (12) : 2730 - 2739
  • [30] Well-Structured Program Equivalence Is Highly Undecidable
    Goldblatt, Robert
    Jackson, Marcel
    ACM TRANSACTIONS ON COMPUTATIONAL LOGIC, 2012, 13 (03)