On Guarded Transformation In The Modal Mu-Calculus

TL;DR

This paper investigates guarded transformations in the modal mu-calculus, revealing exponential blowup issues and linking polynomial transformations to solving parity games, an open problem in the field.

Contribution

It demonstrates that existing guarded transformations can cause exponential growth and connects polynomial guarded transformations to solving parity games, providing new insights.

Findings

Guarded transformations can cause exponential formula size increase.

Polynomial guarded transformations imply a polynomial solution for parity games.

Transformations between mu-calculus, vectorial form, and hierarchical systems are explored.

Abstract

Guarded normal form requires occurrences of fixpoint variables in a {\mu}-calculus-formula to occur under the scope of a modal operator. The literature contains guarded transformations that effectively bring a {\mu}-calculus-formula into guarded normal form. We show that the known guarded transformations can cause an exponential blowup in formula size, contrary to existing claims of polynomial behaviour. We also show that any polynomial guarded transformation for {\mu}-calculus-formulas in the more relaxed vectorial form gives rise to a polynomial solution algorithm for parity games, the existence of which is an open problem. We also investigate transformations between the {\mu}-calculus, vectorial form and hierarchical equation systems, which are an alternative syntax for alternating parity tree automata.