The Power of Priority Channel Systems

Christoph Haase 1, 2 Sylvain Schmitz 2, 1 Philippe Schnoebelen 1
2 DAHU - Verification in databases
LSV - Laboratoire Spécification et Vérification [Cachan], ENS Cachan - École normale supérieure - Cachan, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR8643
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.
Type de document :
Article dans une revue
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〉
Liste complète des métadonnées

https://hal.inria.fr/hal-01091086
Contributeur : Sylvain Schmitz <>
Soumis le : jeudi 4 décembre 2014 - 15:55:45
Dernière modification le : jeudi 11 janvier 2018 - 06:22:14

Lien texte intégral

Identifiants

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〉

Partager

Métriques

Consultations de la notice

130