Skip to Main content Skip to Navigation
Conference papers

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.
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

Identifiers

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. ⟨10.1007/11916277_24⟩. ⟨inria-00424346⟩

Share

Metrics

Record views

105