We show that the following problem is decidable and complete for deterministic exponential time. Given a formula of modal μ-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 μ-calculus fixed point alternation hierarchy is decidable in deterministic exponential time. © Springer-Verlag Berlin Heidelberg 2002.
CITATION STYLE
Küsters, R., & Wilke, T. (2002). Deciding the first level of the μ-calculus alternation hierarchy. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 2556 LNCS, pp. 241–252). Springer Verlag. https://doi.org/10.1007/3-540-36206-1_22
Mendeley helps you to discover research relevant for your work.