Authors: Christoph Haase ; Sylvain Schmitz ; Philippe Schnoebelen

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.

Comment: Extended version of an article presented at CONCUR 2013, LNCS 8052, pp. 319--333, Springer, doi:10.1007/978-3-642-40184-8_23

• 68Q85 - Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)