Alternation Is Strict For Higher-Order Modal Fixpoint Logic

TL;DR

This paper investigates the expressive power of Higher-Order Modal Fixpoint Logic (HFL) through the study of Alternating Parity Krivine Automata (APKA), establishing a hierarchy based on priorities and demonstrating the strictness of alternation levels.

Contribution

It introduces a hierarchy of expressive power for APKA and HFL based on priorities, and proves the strictness of this hierarchy using advanced theoretical methods.

Findings

Priorities determine a hierarchy of expressiveness in APKA.

The hierarchy of APKA priorities induces a strict alternation hierarchy in HFL.

The proof employs encoding runs into trees and the Banach Fixpoint Theorem.

Abstract

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.