We gratefully acknowledge support from
the Simons Foundation and member institutions.
Full-text links:

Download:

Current browse context:

cs.LO

Change to browse by:

cs

References & Citations

DBLP - CS Bibliography

Bookmark

(what is this?)
CiteULike logo BibSonomy logo Mendeley logo del.icio.us logo Digg logo Reddit logo ScienceWISE logo

Computer Science > Logic in Computer Science

Title: A Survey on Satisfiability Checking for the $μ$-Calculus through Tree Automata

Abstract: Algorithms for model checking and satisfiability of the modal $\mu$-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 $\mu$-calculus.
Comments: 28 pages
Subjects: Logic in Computer Science (cs.LO)
Cite as: arXiv:2207.00517 [cs.LO]
  (or arXiv:2207.00517v2 [cs.LO] for this version)

Submission history

From: Daniel Hausmann [view email]
[v1] Fri, 1 Jul 2022 16:01:43 GMT (35kb)
[v2] Tue, 23 Aug 2022 12:23:11 GMT (35kb)

Link back to: arXiv, form interface, contact.