### From $μ$-Calculus to Alternating Tree Automata using Parity Games

**2016-02-02**

1602.00912 | cs.LO

$\mu$-Calculus and automata on infinite trees are complementary ways of
describing infinite tree languages. The correspondence between $\mu$-Calculus
and alternating tree automaton is used to solve the satisfiability and model
checking problems by compiling the modal $\mu$-Calculus formula into an
alternating tree automata. Thus advocating an automaton model specially
tailored for working with modal $\mu$-Calculus. The advantage of the automaton
model is its ability to deal with arbitrary branching in a much simpler way as
compare to the one proposed by Janin and Walukiewicz. Both problems (i.e.,
model checking and satisfiability) are solved by reduction to the corresponding
problems of alternating tree automata, namely to the acceptance and the
non-emptiness problems, respectively. These problems, in turn, are solved using
parity games where semantics of alternating tree automata is translated to a
winning strategy in an appropriate parity game.

**Login to like/save this paper, take notes and configure your recommendations**

# Related Articles

**2019-02-27**

1902.10654 | cs.FL

The complexity of parity games is a long standing open problem that saw a
major breakthrough in 2017… show more

**2019-01-14**

1901.04349 | cs.LO

We prove that the theory of Monadic Second-Order logic (MSO) of the infinite
binary tree extended wi… show more

**2018-07-02**

1807.00893 | cs.FL

We introduce a new setting where a population of agents, each modelled by a
finite-state system, are… show more

**2018-04-17**

1804.06168 | cs.GT

Quantitative extensions of parity games have recently attracted significant
interest. These extensio… show more

**2018-07-27**

1807.10546 | cs.FL

Several distinct techniques have been proposed to design quasi-polynomial
algorithms for solving par… show more

**2018-11-01**

1811.00483 | cs.FL

We introduce a measure called width, quantifying the amount of nondeterminism
in automata. Width gen… show more

**2017-04-28**

1704.08887 | cs.GT

What is a finite-state strategy in a delay game? We answer this surprisingly
non-trivial question by… show more

**2018-02-21**

1802.07435 | cs.LO

We introduce two-player games which build words over infinite alphabets, and
we study the problem of… show more

**2018-05-31**

1805.12592 | cs.LO

We introduce an extension of Strategy Logic for the imperfect-information
setting, called SLii, and … show more

**2016-11-10**

1611.03524 | cs.LO

Quantified CTL (QCTL) is a well-studied temporal logic that extends CTL with
quantification over ato… show more

**2019-03-29**

1903.12620 | cs.FL

An improved translation from alternating parity automata on infinite words to
alternating weak autom… show more

**2017-04-04**

1704.00904 | cs.GT

We introduce quantitative reductions, a novel technique for structuring the
space of quantitative ga… show more

**2019-03-14**

1903.05878 | cs.LO

This paper presents a complete axiomatization of Monadic Second-Order Logic
(MSO) over infinite tree… show more

**2018-09-16**

1809.05978 | cs.GT

We compare two approaches for modelling imperfect information in infinite
games on finite-state syst… show more

**2018-08-28**

1808.09430 | cs.LO

Reactive synthesis is an automatic way to translate a human intention
expressed in some logic into a… show more

**2017-09-14**

1709.04854 | cs.GT

Recently, Dallal, Neider, and Tabuada studied a generalization of the
classical game-theoretic model… show more