2016/09/13 by Florian Bruse
Computer Science · Mathematics · #Alternation (linguistics) #Automaton #Computer science #Discrete mathematics #Expressive power #Fixed point #Formal Methods in Verification #Hierarchy #Logic, Reasoning, and Knowledge #Logic, programming, and type systems #Mathematics #Modal #Modal logic #Modal μ-calculus #Normal modal logic #Operational semantics #Programming language #Semantics (computer science) #Theoretical computer science #cs.FL #cs.LO
paper · pdf · doi:10.4204/eptcs.226.8
published as EPTCS 226, 2016, pp. 105-119 · In Proceedings GandALF 2016, arXiv:1609.03648
openalex publication_date 2016/09/13 · arxiv created 2016/09/14 · arxiv updated 2016/09/15 · openalex created_date 2025/10/10 · openalex updated_date 2026/08/06
We study the expressive power of Alternating Parity Krivine Automata (APKA), which provide operational semantics to Higher-Order Modal Fixpoint Logic (HFL). APKA consist of ordinary parity automata extended by a variation of the Krivine Abstract Machine. We show that the number and parity of priorities available to an APKA form a proper hierarchy of expressive power as in the modal mu-calculus. This also induces a strict alternation hierarchy on HFL. The proof follows Arnold's (1999) encoding of runs into trees and subsequent use of the Banach Fixpoint Theorem.