LIPIcs.FSTTCS.2019.31.pdf
- Filesize: 0.58 MB
- 15 pages
Document
Concurrent Parameterized Games
Authors
Nathalie Bertrand 
,
Patricia Bouyer ,
-
Part of:
Volume:
39th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2019)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS) - License:
Creative Commons Attribution 3.0 Unported license
- Publication Date: 2019-12-04
File
Document Identifiers
Author Details
Acknowledgements
We thank Christoph Haase for insightful discussions on semilinear sets.
Cite AsGet BibTex
Nathalie Bertrand, Patricia Bouyer, and Anirban Majumdar. Concurrent Parameterized Games. In 39th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 150, pp. 31:1-31:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
https://doi.org/10.4230/LIPIcs.FSTTCS.2019.31
https://doi.org/10.4230/LIPIcs.FSTTCS.2019.31
Abstract
Traditional concurrent games on graphs involve a fixed number of players, who take decisions simultaneously, determining the next state of the game. In this paper, we introduce a parameterized variant of concurrent games on graphs, where the parameter is precisely the number of players. Parameterized concurrent games are described by finite graphs, in which the transitions bear regular languages to describe the possible move combinations that lead from one vertex to another.
We consider the problem of determining whether the first player, say Eve, has a strategy to ensure a reachability objective against any strategy profile of her opponents as a coalition. In particular Eve’s strategy should be independent of the number of opponents she actually has. Technically, this paper focuses on an a priori simpler setting where the languages labeling transitions only constrain the number of opponents (but not their precise action choices). These constraints are described as semilinear sets, finite unions of intervals, or intervals.
We establish the precise complexities of the parameterized reachability game problem, ranging from PTIME-complete to PSPACE-complete, in a variety of situations depending on the contraints (semilinear predicates, unions of intervals, or intervals) and on the presence or not of non-determinism.
Subject Classification
ACM Subject Classification
- Theory of computation → Verification by model checking
Keywords
- concurrent games
- parameterized verification
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads
References
- Luca de Alfaro, Thomas A. Henzinger, and Orna Kupferman. Concurrent Reachability Games. In Proceedings of the 39th Annual Symposium on Foundations of Computer Science (FOCS'98), pages 564-575. IEEE Computer Society, 1998. URL: https://doi.org/10.1109/SFCS.1998.743507.
- Rajeev Alur, Thomas A. Henzinger, and Orna Kupferman. Alternating-time Temporal Logic. Journal of the ACM, 49:672-713, 2002. URL: https://doi.org/10.1145/585265.585270.
- Nathalie Bertrand, Miheer Dewaskar, Blaise Genest, and Hugo Gimbert. Controlling a Population. In Proceedings of the 28th International Conference on Concurrency Theory (CONCUR'17), volume 85 of LIPIcs, pages 12:1-12:16. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2017. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2017.12.
- Nathalie Bertrand, Paulin Fournier, and Arnaud Sangnier. Playing with Probabilities in Reconfigurable Broadcast Networks. In Proceedings of the 17th International Conference on Foundations of Software Science and Computation Structure (FoSSaCS'14), volume 8412 of Lecture Notes in Computer Science, pages 134-148. Springer, April 2014. URL: https://doi.org/10.1007/978-3-642-54830-7_9.
- Roderick Bloem, Swen Jacobs, Ayrat Khalimov, Igor Konnov, Sasha Rubin, Helmut Veith, and Josef Widder. Decidability of Parameterized Verification. Synthesis Lectures on Distributed Computing Theory. Morgan & Claypool Publishers, 2015. URL: https://doi.org/10.2200/S00658ED1V01Y201508DCT013.
- Patricia Bouyer, Romain Brenguier, Nicolas Markey, and Michael Ummels. Pure Nash Equilibria in Concurrent Games. Logical Methods in Computer Science, 11(2:9), 2015. URL: https://doi.org/10.2168/LMCS-11(2:9)2015.
- Marek Chrobak. Finite Automata and Unary Languages. Theoretical Computer Science, 47(3):149-158, 1986. URL: https://doi.org/10.1016/0304-3975(86)90142-8.
- Stephen A. Cook. The Complexity of Theorem-Proving Procedures. In Proceedings of the 3rd Annual ACM Symposium on Theory of Computing (STOC'71), pages 151-158. ACM, 1971. URL: https://doi.org/10.1145/800157.805047.
- Giorgio Delzanno. Constraint-Based Verification of Parameterized Cache Coherence Protocols. Formal Methods in System Design, 23(3):257-301, 2003. URL: https://doi.org/10.1023/A:1026276129010.
- Javier Esparza. Keeping a Crowd Safe: On the Complexity of Parameterized Verification (Invited Talk). In Proceedings of the 31st International Symposium on Theoretical Aspects of Computer Science (STACS'14), volume 25 of LIPIcs, pages 1-10. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2014. URL: https://doi.org/10.4230/LIPIcs.STACS.2014.1.
- Dana Fisman, Orna Kupferman, and Yoad Lustig. Rational Synthesis. In Proceedings of the 16th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'10), volume 6015 of Lecture Notes in Computer Science, pages 190-201. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-12002-2_16.
- Erich Grädel, Wolfgang Thomas, and Thomas Wilke, editors. Automata, Logics, and Infinite Games: A Guide to Current Research, volume 2500 of Lecture Notes in Computer Science. Springer, 2002. URL: https://doi.org/10.1007/3-540-36387-4.
- Igor Konnov, Helmut Veith, and Josef Widder. What You Always Wanted to Know About Model Checking of Fault-Tolerant Distributed Algorithms. In Proceedings of the 10th International Andrei Ershov Informatics Conference (PSI'15), volume 9609 of Lecture Notes in Computer Science, pages 6-21. Springer, 2015. URL: https://doi.org/10.1007/978-3-319-41579-6_2.
-
Andrew Martinez. Efficient Computation of Regular Expressions from Unary NFAs. In Proceedings of the 5th International Workshop on Descriptional Complexity of Formal Systems (DCFS'02), pages 174-187. Department of Computer Science, The University of Western Ontario, Canada, 2002.
- Rohit Parikh. On Context-Free Languages. Journal of the ACM, 13(4):570-581, 1966. URL: https://doi.org/10.1145/321356.321364.
- Larry J. Stockmeyer and Albert R. Meyer. Word Problems Requiring Exponential Time (Preliminary Report). In Proceedings of the 5th Annual ACM Symposium on Theory of Computing (STOC'73), pages 1-9. ACM, 1973. URL: https://doi.org/10.1145/800125.804029.
- Michael Ummels and Dominik Wojtczak. The Complexity of Nash Equilibria in Limit-Average Games. In Proceedings of the 22nd International Conference on Concurrency Theory (CONCUR'11), volume 6901 of Lecture Notes in Computer Science, pages 482-496. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-23217-6_32.