The Arity Hierarchy in the Polyadic μ-Calculus

Martin Lange
(University of Kassel)

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.

In Ralph Matthes and Matteo Mio: Proceedings Tenth International Workshop on Fixed Points in Computer Science (FICS 2015), Berlin, Germany, September 11-12, 2015, Electronic Proceedings in Theoretical Computer Science 191, pp. 105–116.
Published: 9th September 2015.

ArXived at: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: