Show simple item record

dc.contributor.authorHausmann, Daniel
dc.contributor.authorPiterman, Nir
dc.date.accessioned2023-01-20T13:21:55Z
dc.date.available2023-01-20T13:21:55Z
dc.date.issued2022
dc.identifier.urihttps://hdl.handle.net/2077/74606
dc.description.abstractAlgorithms for model checking and satisfiability of the modal μ -calculus start by converting formulas to alternating parity tree automata. Thus, model checking is reduced to checking acceptance by tree automata and satisfiability to checking their emptiness. The first reduces directly to the solution of parity games but the second is more complicated. We review the non-emptiness checking of alternating tree automata by a reduction to solving parity games of a certain structure, so-called emptiness games. Since the emptiness problem for alternating tree automata is EXPTIME -complete, the size of these games is exponential in the number of states of the input automaton. We show how the construction of the emptiness games combines a (fixed) structural part with (history-)determinization of parity word automata. For tree automata with certain syntactic structures, simpler methods may be used to handle the treatment of the word automata, which then may be asymptotically smaller than in the general case. These results have direct consequences in satisfiability and validity checking for (various fragments of) the modal μ -calculus.en
dc.language.isoengen
dc.titleA Survey on Satisfiability Checking for the μ -Calculus Through Tree Automataen
dc.typeTexten
dc.type.svepbook chapteren


Files in this item

Thumbnail

This item appears in the following Collection(s)

Show simple item record