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

Highlights - Most important sentences from the article

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
PDF

Highlights - Most important sentences from the article

2019-01-14

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

Highlights - Most important sentences from the article

2018-07-02

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

Highlights - Most important sentences from the article

2018-04-17

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

Highlights - Most important sentences from the article

2018-07-27

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

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
PDF

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
PDF

Highlights - Most important sentences from the article

2018-02-21

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

Highlights - Most important sentences from the article

2018-05-31

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

Highlights - Most important sentences from the article

2016-11-10

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

Highlights - Most important sentences from the article

2019-03-29

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

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
PDF

Highlights - Most important sentences from the article

2019-03-14
1903.05878 | cs.LO

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

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
PDF

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
PDF

Highlights - Most important sentences from the article

2017-09-14

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

Highlights - Most important sentences from the article