The Power of Priority Channel Systems - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Article Dans Une Revue Logical Methods in Computer Science Année : 2014

The Power of Priority Channel Systems

Résumé

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.

Dates et versions

hal-01091086 , version 1 (04-12-2014)

Identifiants

Citer

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⟩
72 Consultations
0 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More