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 条
12345