2015/09/10 by Martin Lange
Computer Science · #cs.LO
paper · pdf · doi:10.4204/eptcs.191.10
published as EPTCS 191, 2015, pp. 105-116 · In Proceedings FICS 2015, arXiv:1509.02826
arxiv created 2015/09/10 · arxiv updated 2015/09/11
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.