More Web Proxy on the site http://driver.im/

research-article

Alternating Tree Automata with Qualitative Semantics

Authors:

Raphaël Berthon,

Nathanaël Fijalkow,

Emmanuel Filiot,

Shibashis Guha,

Bastien Maubert,

Aniello Murano,

Laureline Pinault,

Sophie Pinchinat,

Olivier SerreAuthors Info & Claims

ACM Transactions on Computational Logic (TOCL), Volume 22, Issue 1

Article No.: 7, Pages 1 - 24

https://doi.org/10.1145/3431860

Published: 17 December 2020 Publication History

Abstract

We study alternating automata with qualitative semantics over infinite binary trees: Alternation means that two opposing players construct a decoration of the input tree called a run, and the qualitative semantics says that a run of the automaton is accepting if almost all branches of the run are accepting. In this article, we prove a positive and a negative result for the emptiness problem of alternating automata with qualitative semantics.

The positive result is the decidability of the emptiness problem for the case of Büchi acceptance condition. An interesting aspect of our approach is that we do not extend the classical solution for solving the emptiness problem of alternating automata, which first constructs an equivalent non-deterministic automaton. Instead, we directly construct an emptiness game making use of imperfect information.

The negative result is the undecidability of the emptiness problem for the case of co-Büchi acceptance condition. This result has two direct consequences: the undecidability of monadic second-order logic extended with the qualitative path-measure quantifier and the undecidability of the emptiness problem for alternating tree automata with non-zero semantics, a recently introduced probabilistic model of alternating tree automata.

References

[1]

Christel Baier, Marcus Größer, and Nathalie Bertrand. 2012. Probabilistic ω-automata. J. ACM 59, 1 (2012), 1.

Digital Library

[2]

Vince Bárány, Łukasz Kaiser, and Alex Rabinovich. 2010. Expressing cardinality quantifiers in monadic second-order logic over trees. Fundam. Inf. 100, 1--4 (2010), 1--17.

Digital Library

[3]

Raphaël Berthon, Emmanuel Filiot, Shibashis Guha, Bastien Maubert, Nello Murano, Laureline Pinault, Jean-François Raskin, and Sasha Rubin. 2019. Monadic second-order logic with path-measure quantifier is undecidable. CoRR abs/1901.04349.

[4]

Nathalie Bertrand, Blaise Genest, and Hugo Gimbert. 2009. Qualitative determinacy and decidability of stochastic games with signals. In Proceedings of the 24th Annual IEEE Symposium on Logic in Computer Science. IEEE, 319--328.

Digital Library

[5]

Mikołaj Bojańczyk. 2016. Thin MSO with a probabilistic path quantifier. In Proceedings of the 43rd International Colloquium on Automata, Languages, and Programming (LIPIcs), Vol. 55. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 96:1--96:13.

[6]

Mikołaj Bojańczyk, Hugo Gimbert, and Edon Kelmendi. 2017. Emptiness of zero automata is decidable. In Proceedings of the 44th International Colloquium on Automata, Languages, and Programming (LIPIcs), Vol. 80. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 106:1--106:13.

[7]

Mikołaj Bojańczyk, Edon Kelmendi, and Michal Skrzypczak. 2019. MSO+∇ is undecidable. In Proceedings of the 34th Annual ACM/IEEE Symposium on Logic in Computer Science. IEEE, 1--13.

Digital Library

[8]

Arnaud Carayol, Axel Haddad, and Olivier Serre. 2014. Randomization in automata on infinite trees. ACM Trans. Comput. Logic 15, 3 (2014), 24:1--24:33.

Digital Library

[9]

Arnaud Carayol, Christof Löding, and Olivier Serre. 2018. Pure strategies in imperfect information stochastic games. Fundam. Inf. 160, 4 (2018), 361--384.

Digital Library

[10]

Krishnendu Chatterjee and Laurent Doyen. 2014. Partial-observation stochastic games: How to win when belief fails. ACM Trans. Comput. Logic 15, 2 (2014), 16:1--16:44.

Digital Library

[11]

Krishnendu Chatterjee, Laurent Doyen, Thomas A. Henzinger, and Jean-François Raskin. 2007. Algorithms for omega-regular games with imperfect information. Logic. Methods Comput. Sci. 3, 3 (2007).

[12]

Costas Courcoubetis and Mihalis Yannakakis. 1990. Markov decision processes and regular events (extended abstract). In Proceedings of the 17th International Colloquium on Automata, Languages, and Programming (ICALP'90), Lecture Notes in Computer Science, Vol. 443. Springer, 336--349.

[13]

Luca de Alfaro. 1999. The verification of probabilistic systems under memoryless partial-information policies is hard. In Proceedings of the 2nd International Workshop on Probabilistic Methods in Verification. 19--32.

[14]

Ronald Fagin, Joseph Y. Halpern, Yoram. Moses, and Moshe Y. Vardi. 1995. Reasoning about Knowledge. MIT Press.

[15]

Nathanaël Fijalkow. 2017. Undecidability results for probabilistic automata. SIGLOG News 4, 4 (2017), 10--17.

Digital Library

[16]

Nathanaël Fijalkow, Hugo Gimbert, Edon Kelmendi, and Youssouf Oualhadj. 2015. Deciding the value 1 problem for probabilistic leaktight automata. Logic. Methods Comput. Sci. 11, 2 (2015), 1--42.

[17]

Nathanaël Fijalkow, Sophie Pinchinat, and Olivier Serre. 2013. Emptiness of alternating tree automata using games with imperfect information. In Proceedings of IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (LIPIcs), Vol. 24. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 299--311.

[18]

Nathanaël Fijalkow, Sophie Pinchinat, and Olivier Serre. 2013. Emptiness of Alternating Tree Automata Using Games with Imperfect Information. Retrieved from https://hal.inria.fr/hal-01260682.

[19]

Paulin Fournier and Hugo Gimbert. 2018. Alternating nonzero automata. In Proceedings of the 29th International Conference on Concurrency Theory (LIPIcs), Vol. 118. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 13:1--13:16.

[20]

Hugo Gimbert and Youssouf Oualhadj. 2010. Probabilistic automata on finite words: Decidable and undecidable problems. In Proceedings of the 37th International Colloquium on Automata, Languages and Programming, Lecture Notes in Computer Science, Vol. 6199. Springer, 527--538.

[21]

Hugo Gimbert and Wiesław Zielonka. 2007. Perfect information stochastic priority games. In Proceedings of the 34th International Colloquium on Automata, Languages, and Programming, Lecture Notes in Computer Science, Vol. 4596. Springer, 850--861.

[22]

Vincent Gripon and Olivier Serre. 2009. Qualitative concurrent stochastic games with imperfect information. In Proceedings of the 36th International Colloquium on Automata, Languages, and Programming, Lecture Notes in Computer Science, Vol. 5556. Springer, 200--211.

[23]

Antonín Kučera. 2011. Turn-based stochastic games. In Lectures in Game Theory for Computer Scientists, Krzysztof R. Apt and Erich Grdel (Eds.). Cambridge University Press, New York, NY, Chapter 5, 146--184.

[24]

Henryk Michalewski and Matteo Mio. 2016. Measure quantifier in monadic second order logic. In Proceedings of the International Symposium on Logical Foundations of Computer Science, Lecture Notes in Computer Science, Vol. 9537. Springer, 267--282.

[25]

Matteo Mio, Michał Skrzypczak, and Henryk Michalewski. 2018. Monadic second order logic with measure and category quantifiers. Logic. Methods Comput. Sci. 14, 2 (2018).

[26]

Azaria Paz. 1971. Introduction to Probabilistic Automata. Academic Press.

Digital Library

[27]

Martin L. Puterman. 1994. Markov Decision Processes: Discrete Stochastic Dynamic Programming. John Wiley 8 Sons, Inc., New York, NY.

[28]

Michael O. Rabin. 1963. Probabilistic automata. Inf. Contr. 6, 3 (1963), 230--245.

[29]

Michael O. Rabin. 1969. Decidability of second-order theories and automata on infinite trees. Trans. AMS 141 (1969), 1--35. https://www.ams.org/journals/tran/1969-141-00/S0002-9947-1969-0246760-1/.

[30]

J. H. Reif. 1979. Universal games of incomplete information. In Proceedings of the Annual ACM Symposium on Theory of Computing (STOC’79). ACM, 288--308.

Digital Library

[31]

J. H. Reif. 1984. The complexity of two-player games of incomplete information. J. Comput. Syst. Sci. 29, 2 (1984), 274--301.

[32]

Wolfgang Thomas. 1997. Languages, automata, and logic. In Handbook of Formal Language Theory, G. Rozenberg and A. Salomaa (Eds.). Vol. III. 389--455.

[33]

Wiesław Zielonka. 1998. Infinite games on finitely coloured graphs with applications to automata on infinite trees. Theor. Comput. Sci. 200, 1--2 (1998), 135--183.

Digital Library

Cited By

Belardinelli FJamroga WMittelmann MMurano ADastani MSichman JAlechina NDignum V(2024)Verification of Stochastic Multi-Agent Systems with Forgetful StrategiesProceedings of the 23rd International Conference on Autonomous Agents and Multiagent Systems10.5555/3635637.3662863(160-169)Online publication date: 6-May-2024
https://dl.acm.org/doi/10.5555/3635637.3662863
He YMittelmann MMurano ASaffidine AThielscher MMarquis POrtiz MPagnucco M(2024)Verification of general games with imperfect information using strategy logicProceedings of the 21st International Conference on Principles of Knowledge Representation and Reasoning10.24963/kr.2024/40(420-430)Online publication date: 2-Nov-2024
https://dl.acm.org/doi/10.24963/kr.2024/40
Lespérance YDe Giacomo GRostamigiv MKhan SWooldridge MDy JNatarajan S(2024)Abstraction of situation calculus concurrent game structuresProceedings of the Thirty-Eighth AAAI Conference on Artificial Intelligence and Thirty-Sixth Conference on Innovative Applications of Artificial Intelligence and Fourteenth Symposium on Educational Advances in Artificial Intelligence10.1609/aaai.v38i9.28933(10624-10634)Online publication date: 20-Feb-2024
https://dl.acm.org/doi/10.1609/aaai.v38i9.28933
Show More Cited By

Index Terms

Alternating Tree Automata with Qualitative Semantics
1. Theory of computation

Recommendations

Relating word and tree automata
LICS '96: Proceedings of the 11th Annual IEEE Symposium on Logic in Computer Science

In the automata-theoretic approach to verification, we translate specifications to automata. Complexity considerations motivate the distinction between different types of automata. Already in the 60's, it was known that deterministic Buchi word automata ...
Alternating two-way AC-tree automata

We explore the notion of alternating two-way tree automata modulo the theory of finitely many associative-commutative (AC) symbols. This was prompted by questions arising in cryptographic protocol verification, in particular in modeling group key ...
Pebble alternating tree-walking automata and their recognizing power

Pebble tree-walking automata with alternation were first investigated by Milo, Suciu and Vianu (2003), who showed that tree languages recognized by these devices are exactly the regular tree languages. We strengthen this by proving the same result for ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Transactions on Computational Logic

ACM Transactions on Computational Logic Volume 22, Issue 1

January 2021

262 pages

ISSN:1529-3785

EISSN:1557-945X

DOI:10.1145/3436816

Editor:
Orna Kupferman
School of Computer Science and Engineering, Hebrew University, Israel

Issue’s Table of Contents

Copyright © 2020 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 17 December 2020

Accepted: 01 October 2020

Revised: 01 October 2020

Received: 01 February 2020

Published in TOCL Volume 22, Issue 1

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article
Research
Refereed

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

4
Total Citations
View Citations
121
Total Downloads

Downloads (Last 12 months)12
Downloads (Last 6 weeks)1

Reflects downloads up to 27 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Belardinelli FJamroga WMittelmann MMurano ADastani MSichman JAlechina NDignum V(2024)Verification of Stochastic Multi-Agent Systems with Forgetful StrategiesProceedings of the 23rd International Conference on Autonomous Agents and Multiagent Systems10.5555/3635637.3662863(160-169)Online publication date: 6-May-2024
https://dl.acm.org/doi/10.5555/3635637.3662863
He YMittelmann MMurano ASaffidine AThielscher MMarquis POrtiz MPagnucco M(2024)Verification of general games with imperfect information using strategy logicProceedings of the 21st International Conference on Principles of Knowledge Representation and Reasoning10.24963/kr.2024/40(420-430)Online publication date: 2-Nov-2024
https://dl.acm.org/doi/10.24963/kr.2024/40
Lespérance YDe Giacomo GRostamigiv MKhan SWooldridge MDy JNatarajan S(2024)Abstraction of situation calculus concurrent game structuresProceedings of the Thirty-Eighth AAAI Conference on Artificial Intelligence and Thirty-Sixth Conference on Innovative Applications of Artificial Intelligence and Fourteenth Symposium on Educational Advances in Artificial Intelligence10.1609/aaai.v38i9.28933(10624-10634)Online publication date: 20-Feb-2024
https://dl.acm.org/doi/10.1609/aaai.v38i9.28933
Belardinelli FFerrando AJamroga WMalvone VMurano AElkind E(2023)Scalable verification of strategy logic through three-valued abstractionProceedings of the Thirty-Second International Joint Conference on Artificial Intelligence10.24963/ijcai.2023/6(46-54)Online publication date: 19-Aug-2023
https://dl.acm.org/doi/10.24963/ijcai.2023/6

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

HTML Format

View this article in HTML Format.

Figures

Tables

Media

View Issue’s Table of Contents