The Power of Priority Channel Systems

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}}_{{\epsilon }_0}$-complete.

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

References in corpus (3)

• Multiply-Recursive Upper Bounds with Higman's Lemma
• The Power of Well-Structured Systems
• The Power of Priority Channel Systems

Cited by in corpus (9)

• Complexity Hierarchies Beyond Elementary
• The Power of Well-Structured Systems
• The Power of Priority Channel Systems
• On the state complexity of closures and interiors of regular languages with subwords and superwords
• Verifying Unboundedness via Amalgamation
• Decidability in the logic of subsequences and supersequences
• On Functions Weakly Computable by Pushdown Petri Nets and Related Systems
• On Freeze LTL with Ordered Attributes
• On the cartesian product of well-orderings