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

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

106