Skip to Main content Skip to Navigation
Journal articles

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], Inria Saclay - Ile de France
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 metadata

https://hal.inria.fr/hal-01091086
Contributor : Sylvain Schmitz Connect in order to contact the contributor
Submitted on : Thursday, December 4, 2014 - 3:55:45 PM
Last modification on : Monday, February 15, 2021 - 10:41:12 AM

Links full text

Identifiers

`

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. ⟨10.2168/LMCS-10(4:4)2014⟩. ⟨hal-01091086⟩

Share

Metrics

Record views

240