The power of priority channel systems. (English) Zbl 1448.68341

Haase, Christoph; Schmitz, Sylvain; Schnoebelen, Philippe

Log. Methods Comput. Sci. 10, No. 4, Paper No. 4, 39 p. (2014).

Summary: 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.

MSC:

68Q85

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

Keywords:

well-quasi-order; well-structured transition systems; fast-growing complexity