The Power of Priority Channel Systems

TL;DR

This paper introduces Priority Channel Systems, a novel class of message-passing models with priorities, demonstrating their computational power and analyzing their verification complexity using a new well-quasi-ordering.

Contribution

It presents Priority Channel Systems, a new model with prioritized messages, and establishes their decidability properties and computational complexity using a novel priority embedding.

Findings

Decidability of safety and inevitability properties

Priority embedding as a new well-quasi-ordering

Verification problems are _{\u03b5_{0}}-complete

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.