2015 | OriginalPaper | Buchkapitel
Baire Category Quantifier in Monadic Second Order Logic
verfasst von : Henryk Michalewski, Matteo Mio
Erschienen in: Automata, Languages, and Programming
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
We consider Rabin’s
Monadic Second Order
logic (MSO) of the full binary tree extended with Harvey Friedman’s “for almost all” second-order quantifier (
$$\forall ^*$$
) with semantics given in terms of Baire Category. In Theorem 1 we prove that the new quantifier can be eliminated (
$$\text {MSO}\!+\!\forall ^* \!=\! \text {MSO}$$
). We then apply this result to prove in Theorem 2 that the
finite–SAT
problem for the qualitative fragment of the probabilistic temporal logic pCTL* is decidable. This extends a previous result of Brázdil, Forejt, Křetínský and Kučera valid for qualitative pCTL.