The Arity Hierarchy in the Polyadic $\mu$-Calculus

TL;DR

This paper establishes a hierarchy within the polyadic mu-calculus, showing that increasing relation arity enhances expressive power, with the proof based on a diagonalisation argument.

Contribution

It introduces a hierarchy result demonstrating that higher arity relations in the polyadic mu-calculus increase expressive power, using a novel diagonalisation proof technique.

Findings

Higher arity relations have greater expressive power.

The hierarchy is strict for each level of fixpoint alternation.

The proof employs a diagonalisation argument.

Abstract

The polyadic mu-calculus is a modal fixpoint logic whose formulas define relations of nodes rather than just sets in labelled transition systems. It can express exactly the polynomial-time computable and bisimulation-invariant queries on finite graphs. In this paper we show a hierarchy result with respect to expressive power inside the polyadic mu-calculus: for every level of fixpoint alternation, greater arity of relations gives rise to higher expressive power. The proof uses a diagonalisation argument.