ML p(r)ior | From $μ$-Calculus to Alternating Tree Automata using Parity Games

### 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.

Highlights - Most important sentences from the article

# 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

Highlights - Most important sentences from the article

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

Highlights - Most important sentences from the article

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

Highlights - Most important sentences from the article

2018-04-17
1804.06168 | cs.GT

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

Highlights - Most important sentences from the article

2018-07-27
1807.10546 | cs.FL

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

Highlights - Most important sentences from the article

2018-11-01
1811.00483 | cs.FL

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

Highlights - Most important sentences from the article

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

Highlights - Most important sentences from the article

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

Highlights - Most important sentences from the article

2018-05-31
1805.12592 | cs.LO

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

Highlights - Most important sentences from the article

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

Highlights - Most important sentences from the article

2019-03-29
1903.12620 | cs.FL

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

Highlights - Most important sentences from the article

2017-04-04
1704.00904 | cs.GT

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

Highlights - Most important sentences from the article

2019-03-14
1903.05878 | cs.LO

Highlights - Most important sentences from the article

2018-09-16
1809.05978 | cs.GT

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

Highlights - Most important sentences from the article

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

Highlights - Most important sentences from the article

2017-09-14
1709.04854 | cs.GT