On Computing Fixpoints in Well-Structured Regular Model Checking, with Applications to Lossy Channel Systems

Christel BaierChristel Baier, Nathalie BertrandNathalie Bertrand, Philippe SchnoebelenPhilippe Schnoebelen

DOI Link

Christel Baier, Nathalie Bertrand, Philippe Schnoebelen
On Computing Fixpoints in Well-Structured Regular Model Checking, with Applications to Lossy Channel Systems
Proc. of the 13th International Conference on Logic for Programming and Artificial Intelligence (LPAR), volume 4246 of Lecture Notes in Computer Science, 347--361, 2006. Springer

Details
Bibtex

KurzfassungAbstract
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.
Forschungsgruppe:Research Group: Algebraische und logische Grundlagen der InformatikAlgebraic and Logical Foundations of Computer Science

The final publication is available at Springer via http://dx.doi.org/10.1007/11916277_24.

@inproceedings{BBS2006,
  author    = {Christel Baier and Nathalie Bertrand and Philippe Schnoebelen},
  title     = {On Computing Fixpoints in Well-Structured Regular Model Checking,
               with Applications to Lossy Channel Systems},
  booktitle = {Proc. of the 13th International Conference on Logic for
               Programming and Artificial Intelligence (LPAR)},
  series    = {Lecture Notes in Computer Science},
  volume    = {4246},
  publisher = {Springer},
  year      = {2006},
  pages     = {347--361},
  doi       = {10.1007/11916277_24}
}