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

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

Identifiants

Collections

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〉

Partager

Métriques

Consultations de la notice

50