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.
Type de document :
Communication dans un congrès
13th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR'06), Nov 2006, Phnom Penh, Cambodia. Springer, 4246, 2006, LNAI. 〈10.1007/11916277_24〉
Liste complète des métadonnées
https://hal.inria.fr/inria-00424346
Contributeur : Nathalie Bertrand <>
Soumis le : jeudi 15 octobre 2009 - 11:18:08
Dernière modification le : jeudi 11 janvier 2018 - 06:20:13

Lien texte intégral

openaccess

Identifiants

Collections

ENS-CACHAN

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. Springer, 4246, 2006, LNAI. 〈10.1007/11916277_24〉. 〈inria-00424346〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

59

Contact


archive-ouverte@inria.fr