On computing fixpoints in well-structured regular model checking, with applications to lossy channel systems
符号计算
2012-03-19 v1 计算机科学与博弈论
摘要
We prove a general finite convergence theorem for "upward-guarded" fixpoint expressions over a well-quasi-ordered set. This has immediate applications in regular model checking of well-structured systems, where a main issue is the eventual convergence of fixpoint computations. In particular, we are able to directly obtain several new decidability results on lossy channel systems.
引用
@article{arxiv.cs/0606091,
title = {On computing fixpoints in well-structured regular model checking, with applications to lossy channel systems},
author = {C. Baier and N. Bertrand and Ph. Schnoebelen},
journal= {arXiv preprint arXiv:cs/0606091},
year = {2012}
}
备注
16 pages