Christoph Haase ; Sylvain Schmitz ; Philippe Schnoebelen - The Power of Priority Channel Systems

lmcs:1049 - Logical Methods in Computer Science, December 3, 2014, Volume 10, Issue 4 - https://doi.org/10.2168/LMCS-10(4:4)2014
The Power of Priority Channel SystemsArticle

Authors: Christoph Haase ORCID; Sylvain Schmitz ORCID; 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.


    Volume: Volume 10, Issue 4
    Published on: December 3, 2014
    Imported on: March 29, 2014
    Keywords: Computer Science - Logic in Computer Science

    14 Documents citing this article

    Consultation statistics

    This page has been seen 1323 times.
    This article's PDF has been downloaded 375 times.