Skip to Main content Skip to Navigation
Conference papers

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

Christel Baier 1 Nathalie Bertrand 2 Philippe Schnoebelen 2
1 Department of Computer Science [Dresden]
2 LSV - Laboratoire Spécification et Vérification [Cachan]
Abstract : 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.
Document type :
Conference papers
Complete list of metadata
https://hal.inria.fr/inria-00424346
Contributor : Nathalie Bertrand <>
Submitted on : Thursday, October 15, 2009 - 11:18:08 AM
Last modification on : Monday, February 15, 2021 - 10:39:41 AM

Links full text

arxiv

Identifiers

Collections

CNRS | ENS-CACHAN | ENS-PARIS-SACLAY

Citation

Christel Baier, Nathalie Bertrand, Philippe Schnoebelen. On Computing Fixpoints in Well-Structured Regular Model Checking, with Applications to Lossy Channel Systems.. 13th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR'06), Nov 2006, Phnom Penh, Cambodia. ⟨10.1007/11916277_24⟩. ⟨inria-00424346⟩

Export

BibTeX TEI DC DCterms EndNote

Share

Metrics

Record views

105

 

Contact                    Legal Notice                    Personal Data