Skip to Main content Skip to Navigation
New interface
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
Contributor : Sylvain Schmitz Connect in order to contact the contributor
Submitted on : Thursday, December 4, 2014 - 3:55:45 PM
Last modification on : Wednesday, January 26, 2022 - 3:08:04 AM

Links full text



Christoph Haase, Sylvain Schmitz, Philippe Schnoebelen. The Power of Priority Channel Systems. Logical Methods in Computer Science, 2014, 10 (4:4), pp.1--39. ⟨10.2168/LMCS-10(4:4)2014⟩. ⟨hal-01091086⟩



Record views