Deciding the First Level of the μ-calculus Alternation Hierarchy

We show that the following problem is decidable and complete for deterministic exponential time. Given a formula of modal my-calculus, determine if the formula is equivalent to a formula without greatest fixed point operators. In other words, we show that the first level of the my-calculus fixed point alternation hierarchy is decidable in deterministic exponential time.

Vorschau

Logo BII

BII

Zitieren

Zitierform:
Zitierform konnte nicht geladen werden.

Rechte

Nutzung und Vervielfältigung:Keine Creative-Commons-Lizenz - Es gelten die Bestimmungen des dt. Urheberrechts (UrhG)Bitte beachten Sie, dass einzelne Bestandteile der Publikation anderweitigen Lizenz- bzw. urheberrechtlichen Bedingungen unterliegen können.