The Power Of Priority Channel Systems

We introduce Priority Channel Systems, a new natural 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 veri fi cation problems are F-epsilon 0-complete.