The Power of Priority Channel Systems

Christoph Haase 1, 2 Sylvain Schmitz 2, 1 Philippe Schnoebelen 1
2 DAHU - Verification in databases
CNRS - Centre National de la Recherche Scientifique : UMR8643, Inria Saclay - Ile de France, ENS Cachan - École normale supérieure - Cachan, LSV - Laboratoire Spécification et Vérification [Cachan]
Abstract : We introduce Priority Channel Systems, a new class of channel systems where messages carry a numeric priority and where higher-priority messages can supersede lower-priority messages preceding them in the fifo communication buffers. The decidability of safety and inevitability properties is shown via the introduction of a priority embedding, a well-quasi-ordering that has not previously been used in well-structured systems. We then show how Priority Channel Systems can compute Fast-Growing functions and prove that the aforementioned verification problems are $\mathbf{F}_{\varepsilon_0}$-complete.
Document type :
Journal articles
Complete list of metadatas

https://hal.inria.fr/hal-01091086
Contributor : Sylvain Schmitz <>
Submitted on : Thursday, December 4, 2014 - 3:55:45 PM
Last modification on : Thursday, July 4, 2019 - 3:56:24 PM

Links full text

Identifiers

Collections

Citation

Christoph Haase, Sylvain Schmitz, Philippe Schnoebelen. The Power of Priority Channel Systems. Logical Methods in Computer Science, Logical Methods in Computer Science Association, 2014, 10 (4:4), pp.1--39. ⟨http://www.lmcs-online.org/ojs/viewarticle.php?id=1595&layout=abstract⟩. ⟨10.2168/LMCS-10(4:4)2014⟩. ⟨hal-01091086⟩

Share

Metrics

Record views

174