Level: M1 - M2
Contact: Patricia Bouyer (bouyer@lsv.fr)
Location: Laboratoire Méthodes Formelles, ENS Paris-Saclay
Keywords: Parameterized verification, concurrent games, distributed computing, formal languages
Description
Parameterized verification
The generalisation and everyday usage of modern distributed systems call both for the verification and synthesis of algorithms or strategies running on distributed systems. Concrete examples are cloud computing, blockchain technologies, servers with multiple clients, wireless sensor networks, bio-chemical systems, or fleets of drones cooperating to achieve a common goal [7]. In their general form, these systems are not only distributed, but they may also involve an arbitrary number of agents. This explains the interest of the model-checking community both for the verification of parameterized systems [8, 5], and for the synthesis of distributed strategies [10].
Parameterized verification refers here to the verification of systems formed of an arbitrary number of agents. Often, the precise number of agents is unknown, yet, algorithms and protocols running on such distributed systems are designed to operate correctly independently of the number of agents. The automated verification and control of such systems is challenging.
Concurrent games on graphs
By allowing complex interactions between agents, concurrent games on graphs [1, 2] are a model of choice in several contexts, for instance for multi-agents systems, or for coordination or planning problems. An arena for n agents is a directed graph where the transitions are labeled by n-tuples of actions (or simply words of length n). At each vertex of the graph, all n agents select simultaneously and independently an action, and the next vertex is determined by the combined move consisting of all the actions (or word formed of all the actions). Most often, one considers infinite duration plays, i.e., plays generated by iterating this process forever. Concepts studied on multiagent concurrent games include many borrowed from game theory, such as winning strategies (see e.g., [1]), rationality of the agents (see e.g., [9]), Nash equilibria (see e.g., [11, 6]).
Parameterized concurrent games on graphs
Concurrent games in which the number of agents is arbitrary have been defined in [3]. These games generalize concurrent games with a fixed number of agents, and can be seen as a succinct representation of infinitely many games, one for each fixed number of agents. This is done by replacing, on edges of the arena, words representing the choice of each of the agents by languages of finite yet a priori unbounded words. Such a parameterized arena can represent infinitely many interaction situations, one for each possible number of agents. In parameterized concurrent games, the agents do not know a priori the number of agents participating to the interaction. Each agent observes the action it plays and the vertices the play goes through. These pieces of information may refine the knowledge each agent has on the number of involved agents.
Such a game model raises new interesting questions, since the agents do not know beforehand how many they are. In [3] and [4], we investigated two questions of interest regarding synthesis of strategies for agents in the mentioned context. In particular, [4] investigated the question of synthesizing a coalition strategy profile to achieve a safety objective, using an automata-based approach. Remains open the question of synthesizing a coalition strategy profile for more general properties.
For an overview of the setting or of the existing results, you can listen to my invited talk at CONCUR'21 or to references [3] and [4]
Internship goal
In this internship we will consider the synthesis problem for a coalition strategy profile to achieve a reachability objective. Examples show that the approach used for safety properties cannot transpose to reachability objectives. We will start by examining the simpler case of a three-state game arena, where one of the state is "win", another is "lose", and the last one is "wait". We will also restrict to simpler languages, for instance generated by flat automata.
This M2 internship proposal can be extended to a PhD proposal.
References
[1] 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 Press, 1998. doi:10.1109/SFCS.1998.743507
[2] Rajeev Alur, Thomas A. Henzinger, and Orna Kupferman. Alternating-time temporal logic. Journal of the ACM, 49:672–713, 2002. doi:10.1145/585265.585270
[3] Nathalie Bertrand, Patricia Bouyer, and Anirban Majumdar. Concurrent parameterized games. In Proceedings of the 39th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS’19), volume 150 of LIPIcs, pages 31:1–31:15. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019. doi:10.4230/LIPIcs.FSTTCS.2019.31
[4] Nathalie Bertrand, Patricia Bouyer, Anirban Majumdar. Synthesizing Safe Coalition Strategies. In Proceedings of the 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS’20), volume 182 of LIPIcs, pages 39:1–31:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019. doi:10.4230/LIPIcs.FSTTCS.2020.39
[5] 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. doi:10.2200/ S00658ED1V01Y201508DCT013
[6] Patricia Bouyer, Romain Brenguier, Nicolas Markey, and Michael Ummels. Pure Nash equilibria in concurrent games. Logical Methods in Computer Science, 11(2:9), 2015. doi: 10.2168/LMCS-11(2:9)2015
[7] Tristan Charrier, Arthur Queffelec, Ocan Sankur, and François Schwarzentruber. Reachability and coverage planning for connected agents. In Proceedings of the 28th International Joint Conference on Artificial Intelligence (IJCAI’19), pages 144–150. ijcai.org, 2019. doi:10.24963/ ijcai.2019/21
[8] 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. doi:10.4230/LIPIcs.STACS.2014.1
[9] 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. doi:10.1007/978-3-642-12002-2_16
[10] Amir Pnueli and Roni Rosner. Distributed reactive systems are hard to synthesize. In Proceedings of the 31st Annual Symposium on Foundations of Computer Science (FOCS’90), volume 2, pages 746–757. IEEE Computer Society Press, 1990. doi:10.1109/FSCS.1990. 89597
[11] 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. doi:10.1007/978-3-642-23217-6_32
