2013/01/31 by Christoph Haase, Sylvain Schmitz, Philippe Schnoebelen · 2 citations
Computer Science · #Channel (broadcasting) #Class (philosophy) #Computer network #Computer science #Cryptographic Implementations and Security #Decidability #Distributed computing #Dynamic priority scheduling #Embedding #Expressive power #FIFO (computing and electronics) #Formal Methods in Verification #Logic, programming, and type systems #Power (physics) #Priority ceiling protocol #Priority inheritance #Programming language #Quality of service #Theoretical computer science #cs.LO
paper · pdf · doi:10.2168/lmcs-10(4:4)2014
published as Logical Methods in Computer Science, Volume 10, Issue 4 (December 3, 2014) lmcs:1049 · Extended version of an article presented at CONCUR 2013, LNCS 8052, pp. 319--333, Springer, doi:10.1007/978-3-642-40184-8_23
arxiv created 2014/12/02 · openalex publication_date 2014/12/03 · arxiv updated 2016/02/01 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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 F_ε0-complete.