Abstract
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.
H. Michalewski—Author supported by Polands National Science Centre grant no. 2014-13/B/ST6/03595.
M. Mio—Author supported by grant “Projet Émergent PMSO” of the École Normale Supérieure de Lyon.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
References
Baier, C., Bertrand, N., Bouyer, P., Brihaye, T., Größer, M.: Probabilistic and topological semantics for timed automata. In: Arvind, V., Prasad, S. (eds.) FSTTCS 2007. LNCS, vol. 4855, pp. 179–191. Springer, Heidelberg (2007)
Baier, C., Katoen, J.P.: Principles of Model Checking. The MIT Press (2008)
Bárány, V., Kaiser, Ł., Rabinovich, A.: Cardinality quantifiers in MLO over trees. In: Grädel, E., Kahle, R. (eds.) CSL 2009. LNCS, vol. 5771, pp. 117–131. Springer, Heidelberg (2009)
Barua, R.: \(R\)-sets and category. Trans. Amer. Math. Soc. 286(1), 125–158 (1984)
Bertrand, N., Fearnley, J., Schewe, S.: Bounded satisfiability for PCTL. In: Proc. of CSL (2012)
Brázdil, T., Forejt, V., Kretínský, J., Kucera, A.: The satisfiability problem for probabilistic CTL. In: Proc. of LICS, pp. 391–402 (2008)
Carayol, A., Haddad, A., Serre, O.: Randomization in automata on infinite trees. ACM Transactions on Computational Logic 15(3) (2014)
Carayol, A., Serre, O.: How good is a strategy in a game with nature? In: To appear in Proc. LICS (2015)
Gogacz, T., Michalewski, H., Mio, M., Skrzypczak, M.: Measure properties of game tree languages. In: Csuhaj-Varjú, E., Dietzfelbinger, M., Ésik, Z. (eds.) MFCS 2014, Part I. LNCS, vol. 8634, pp. 303–314. Springer, Heidelberg (2014)
Hansson, H., Jonsson, B.: A logic for reasoning about time and reliability. Formal Aspects of Computing 6(5), 512–535 (1994)
Hjorth, G., Khoussainov, B., Montalban, A., Nies, A.: From automatic structures to Borel structures. In: Proc. of LICS, pp. 431–441 (2008)
Kechris, A.S.: Classical Descriptive Set Theory. Springer (1994)
Muller, D.E., Schupp, P.E.: Simulating alternating tree automata by nondeterministic automata: New results and new proofs of the theorems of Rabin. McNaughton and Safra. Theor. Comput. Sci. 141(1&2), 69–107 (1995)
Rabin, M.O.: Decidability of second-order theories and automata on infinite trees. Transactions of American Mathematical Society 141, 1–35 (1969)
Serre, O.: Playing with Trees and Logic. Habilitation Thesis, Université Paris Diderot (Paris 7) (2015)
Staiger, L.: Rich omega-words and monadic second-order arithmetic. In: Proc. of CSL, pp. 478–490 (1997)
Steinhorn, C.I.: Chapter XVI: Borel Structures and Measure and Category Logics. Perspectives in Mathematical Logic, vol. 8. Springer (1985)
Thomas, W.: On chain logic, path logic, and first-order logic over infinite trees. In: Proc. of LICS, pp. 245–256 (1987)
Thomas, W.: Languages, automata, and logic. In: Handbook of Formal Languages, pp. 389–455. Springer (1996)
Vaught, R.: Invariant sets in topology and logic. Fund. Math., 82, 269–294 (1974/1975), Collection of articles dedicated to Andrzej Mostowski on his sixtieth birthday, VII
Völzer, H., Varacca, D.: Defining fairness in reactive and concurrent systems. Journal of the ACM 59(3) (2012)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Michalewski, H., Mio, M. (2015). Baire Category Quantifier in Monadic Second Order Logic. In: Halldórsson, M., Iwama, K., Kobayashi, N., Speckmann, B. (eds) Automata, Languages, and Programming. ICALP 2015. Lecture Notes in Computer Science(), vol 9135. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-47666-6_29
Download citation
DOI: https://doi.org/10.1007/978-3-662-47666-6_29
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-662-47665-9
Online ISBN: 978-3-662-47666-6
eBook Packages: Computer ScienceComputer Science (R0)