Additional Winning Strategies in Reachability Games

• Autorzy: Malvone V. , Murano A. , Sorrentino L.

Identyfikatory

DOI

10.3233/FI-2018-1662

• Konferencja: Convegno Italiano di Logica Computazionale : CILC 2015 (30th; 01-03.07.2015; University of Genoa, Italy)
• Języki publikacji: EN

Abstrakty

EN

In game theory, deciding whether a designed player wins a game amounts to check whether he has a winning strategy. However, there are several game settings in which knowing whether he has more than a winning strategy is also important. For example, this is crucial in deciding whether a game admits a unique Nash Equilibrium, or in planning a rescue as this would provide a backup plan. In this paper we study the problem of checking whether, in a two-player reachability game, a designed player has more than a winning strategy. We investigate this question both under perfect and imperfect information about the moves performed by the players. We provide an automata-based solution that results, in the perfect information setting, in a linear-time procedure; in the imperfect information setting, instead, it shows an exponential-time upper bound. In both cases, the results are tight.

Słowa kluczowe

EN

additional strategies; graded modalities; imperfect information; two-player reachability games

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2018
• Tom: Vol. 159, nr 1/2
• Strony: 175--195
• Opis fizyczny: Bibliogr. 56 poz., rys.

Twórcy

autor

Malvone V.

• Università degli Studi di Napoli Federico II, Department DIETI, Via Claudio n.21, 80125, Napoli, Italy

autor

Murano A.

• Università degli Studi di Napoli Federico II, Department DIETI, Via Claudio n.21, 80125, Napoli, Italy

autor

Sorrentino L.

• Università degli Studi di Napoli Federico II, Department DIETI, Via Claudio n.21, 80125, Napoli, Italy

Bibliografia

• [1] Malvone V, Murano A, Sorrentino L. Games with Additional Winning Strategies. In: CILC 2015. 2015 pp. 175-180.
• [2] Harel D, Pnueli A. On the Development of Reactive Systems. NATO ASI Series (Series F: Computer and Systems Sciences) vol. 13. Springer, 1985. URL https://doi.org/10.1007/978-3-642-82453-1_17.
• [3] Myerson R. Game Theory: Analysis of Conflict. Harvard University Press, 1991. ISBN: 0674341155, 9780674341159.
• [4] Smith JM. Evolution and the Theory of Games. Cambridge university press, 1982. ISBN: 0521288843, 9780521288842.
• [5] Alur R, Henzinger T, Kupferman O. Alternating-Time Temporal Logic. Journal of the ACM, 2002. 49(5):672-713. doi:10.1145/585265.585270.
• [6] Wooldridge M. An Introduction to Multi Agent Systems. John Wiley & Sons, 2002. ISBN-10:047149691X, 13: 978-0471496915.
• [7] Kupferman O, Vardi M, Wolper P. Module Checking. Information and Computation, 2001. 164(2):322-344. URL https://doi.org/10.1006/inco.2000.2893.
• [8] Kupferman O, Vardi M. Module Checking Revisited. In: Computer Aided Verification’97, LNCS 1254. Springer, 1997 pp. 36-47. URL https://doi.org/10.1007/3-540-63166-6_7.
• [9] Reif JH. The Complexity of Two-Player Games of Incomplete Information. J. Comput. Syst. Sci., 1984. 29(2):274-301. URL https://doi.org/10.1016/0022-0000(84)90034-5.
• [10] Pnueli A, Rosner R. On the Synthesis of a Reactive Module. In: Principles of Programming Languages’89. Association for Computing Machinery, 1989 pp. 179-190. doi:10.1145/75277.75293.
• [11] Malvone V, Murano A, Sorrentino L. Hiding Actions in Concurrent Games. In: ECAI 2016, volume 285 of FAIA. 2016 pp. 1686-1687. doi:10.3233/978-1-61499-672-9-1686.
• [12] Malvone V, Murano A, Sorrentino L. Hiding Actions in Multi-Player Games. In: AAMAS 2017. 2017 pp. 1205-1213. URL http://dl.acm.org/citation.cfm?id=3091282.3091293.
• [13] Altman E, Kameda H, Hosokawa Y. Nash Equilibria in Load Balancing in Distributed Computer Systems. IGTR, 2002. 4(2):91-100. URL https://doi.org/10.1142/S0219198902000574.
• [14] Papavassilopoulos G, Cruz JB. On the Uniqueness of Nash Strategies for a Class of Analytic Differential Games. Journal of Optimization Theory and Applications, 1979. 27(2):309-314.
• [15] Cornes R, Hartley R, Sandler T. An Elementary Proof via Contraction. Journal of Public Economic Theory, 1999. 1(4):499-509. doi:10.1111/1097-3923.00023.
• [16] Orda A, Rom R, Shimkin N. Competitive Routing in Multiuser Communication Networks. IEEE/ACM Trans. Netw., 1993. 1(5):510-521. doi:10.1109/90.251910.
• [17] Bergstrom TC, Blume LE, Varian HR. On the Private Provision of Public Goods. Journal of Public Economics, 1986. 29(1):25-49.
• [18] Fraser CD. The Uniqueness of Nash Equilibrium in the Private Provision of Public Goods: an Alternative Proof. Journal of Public Economics, 1992. 49(3):389-390. URL https://doi.org/10.1016/0047-2727(92)90076-R.
• [19] Glazer A, Konrad KA. Private Provision of Public Goods, Limited Tax Deducibility, and Crowding Out. FinanzArchiv / Public Finance Analysis, 1993. 50(2):203-216.
• [20] Malvone V, Mogavero F, Murano A, Sorrentino L. On the Counting of Strategies. In: TIME 2015. 2015 pp. 170-179. doi:10.1109/TIME.2015.19.
• [21] Aminof B, Malvone V, Murano A, Rubin S. Graded Strategy Logic: Reasoning about Uniqueness of Nash Equilibria. In: AAMAS 2016. 2016 pp. 698-706. ISBN: 978-1-4503-4239-1.
• [22] D Simchi-Levi JB X Chen. The Logic of Logistics: Theory, Algorithms, and Applications for Logistics Management. Science and Business Media. Springer, 2013. ISBN-10: 1461491487, 13: 978-1461491484.
• [23] Zhang Y, Guizani M. Game Theory for Wireless Communications and Networking. CRC Press, 2011. ISBN: 9781439808894.
• [24] Pavel L. Game Theory for Control of Optical Networks. Science and Business Media. Springer, 2012. doi:10.1007/978-0-8176-8322-1.
• [25] Kitano H, Tadokoro S, Noda I, Matsubara H, Takahashi T, Shinjou A, Shimada S. Robocup rescue: Search and Rescue in Large-Scale Disasters as a Domain for Autonomous Agents Research. In: IEEE, volume 6. 1999 pp. 739-743. doi:10.1109/ICSMC.1999.816643.
• [26] Kitano H, Tadokoro S. Robocup Rescue: A Grand Challenge for Multiagent and Intelligent Systems. AI magazine, 2001. 22(1):39. doi: https://doi.org/10.1609/aimag.v22i1.1542.
• [27] Chang M, Tseng Y, Chen J. A Scenario Planning Approach for the Flood Emergency Logistics Preparation Problem under Uncertainty. Transportation Research Part E: Logistics and Transportation Review, 2007. 43(6):737-754. URL http://www.sciencedirect.com/science/article/pii/S1366554507000178.
• [28] Alur R, Courcoubetis C, Yannakakis M. Distinguishing Tests for Nondeterministic and Probabilistic Machines. In: ACM. 1995 pp. 363-372. doi:10.1145/225058.225161.
• [29] Berthon R, Maubert B, Murano A, S Rubin, Vardi MY. Strategy logic with imperfect information. In: LICS. 2017 pp. 1-12. doi:10.1109/LICS.2017.8005136.
• [30] Belardinelli F, Lomuscio A, Murano A, Rubin S. Verification of Broadcasting Multi-Agent Systems against an Epistemic Strategy Logic. In: IJCAI 2017. 2017 pp. 91-97. URL https://doi.org/10.24963/ijcai.2017/14.
• [31] Bonatti P, Lutz C, Murano A, Vardi M. The Complexity of Enriched muCalculi. Logical Methods in Computer Science, 2008. 4(3):1-27. doi:10.2168/LMCS-4(3:11)2008.
• [32] Ferrante A, Murano A, Parente M. Enriched Mu-Calculi Module Checking. Logical Methods in Computer Science, 2008. 4(3):1-21. doi:10.2168/LMCS-4(3:1)2008.
• [33] Fine K. In So Many Possible Worlds. Notre Dame Journal of Formal Logic, 1972. 13:516-520.
• [34] Grädel E, Otto M, Rosen E. Two-Variable Logic with Counting is Decidable. In: Logic in Computer Science’97. IEEE Computer Society, 1997 pp. 306-317. doi:10.1109/LICS.1997.614957.
• [35] Horrocks I, Sattler U. Decidability of SHIQ with Complex Role Inclusion Axioms. Artif. Intell., 2004. 160(1-2):79-104. URL https://doi.org/10.1016/j.artint.2004.06.002.
• [36] Calvanese D, Giacomo GD, Lenzerini M, Vardi MY. Node Selection Query Languages for Trees. In: AAAI. 2010 pp. 279-284.
• [37] Calvanese D, Eiter T, Ortiz M. Answering Regular Path Queries in Expressive Description Logics via Alternating Tree-Automata. Inf. Comput., 2014. 237:12-55. URL https://doi.org/10.1016/j.ic.2014.04.002.
• [38] Baader F, Borgwardt S, Lippmann M. Temporal Conjunctive Queries in Expressive Description Logics with Transitive Roles. In: AI 2015. 2015 pp. 21-33. doi:10.1007/978-3-319-26350-2_3.
• [39] Feier C, Eiter T. Reasoning with Forest Logic Programs Using Fully Enriched Automata. In: LPNMR 2015. 2015 pp. 346-353. doi:10.1007/978-3-319-23264-5_29.
• [40] Kupferman O, Sattler U, Vardi M. The Complexity of the Graded muCalculus. In: Conference on Automated Deduction’02, LNCS 2392. Springer, 2002 pp. 423-437. URL https://doi.org/10.1007/3-540-45620-1_34.
• [41] Bianco A, Mogavero F, Murano A. Graded Computation Tree Logic. Transactions On Computational Logic, 2012. 13(3):25:1-53. doi:10.1145/2287718.2287725.
• [42] Aminof B, Murano A, Rubin S. On CTL* with Graded Path Modalities. In: LPAR-20. 2015 pp. 281-296. doi:10.1007/978-3-662-48899-7_20.
• [43] J Bernet, D Janin, Walukiewicz I. Permissive strategies: from parity games to safety games. RAIRO-Theoretical Informatics and Applications, 2002. 36(3):261-275. URL http://www.numdam.org/item?id=ITA_2002__36_3_261_0.
• [44] Thomas W. Infinite Trees and Automaton Definable Relations over Omega-Words. In: STACS’90. 1990 pp. 263-277. ISBN: 3-540-52282-4.
• [45] Kupferman O, Vardi MY. Synthesis with incomplete informatio. In: Advances in Temporal Logic, vol. 16, pp. 109-127. Springer, 2000. URL https://doi.org/10.1007/978-94-015-9586-5_6.
• [46] Vardi M, Wolper P. Automata-Theoretic Techniques for Modal Logics of Programs. Journal of Computer and System Science, 1986. 32(2):183-221. URL https://doi.org/10.1016/0022-0000(86)90026-7.
• [47] Kupferman O, Vardi M, Wolper P. An Automata Theoretic Approach to Branching-Time Model Checking. Journal of the ACM, 2000. 47(2):312-360. doi:10.1145/333979.333987.
• [48] Emerson E, Jutla C. Tree Automata, muCalculus, and Determinacy. In: Foundation of Computer Science’91. IEEE Computer Society, 1991 pp. 368-377. doi:10.1109/SFCS.1991.185392.
• [49] Sipser M. Introduction to the Theory of Computation, volume 2. Thomson Course Technology Boston, 2006.
• [50] Chatterjee K, Doyen L, Henzinger TA, Raskin J. Algorithms for omega-regular games with imperfect information. Logical Methods in Computer Science, 2007. 3(4):1-23. doi:10.2168/LMCS-3(3:4)2007.
• [51] Emerson E, Jutla C. The Complexity of Tree Automata and Logics of Programs (Extended Abstract). In: Foundation of Computer Science’88. IEEE Computer Society, 1988 pp. 328-337.
• [52] Jamroga W, Murano A. On Module Checking and Strategies. In: Autonomous Agents and MultiAgent Systems’14. International Foundation for Autonomous Agents and Multiagent Systems, 2014 pp. 701-708. ISBN: 978-1-4503-2738-1.
• [53] Jamroga W, Murano A. Module Checking of Strategic Ability. In: Autonomous Agents and MultiAgent Systems’15. International Foundation for Autonomous Agents and Multiagent Systems, 2015 pp. 227-235. ISBN: 978-1-4503-3413-6.
• [54] Murano A, Sorrentino L. A Game-Based Model for Human-Robots Interaction. In: WOA’15, volume 1382 of CEUR Workshop Proceedings. CEUR-WS.org, 2015 pp. 146-150.
• [55] Bozzelli L, Murano A, Peron A. Pushdown Module Checking. Formal Methods in System Design, 2010. 36(1):65-95. URL https://doi.org/10.1007/s10703-010-0093-x.
• [56] Murano A, Perelli G. Pushdown Multi-Agent System Verification. In: IJCAI 2015. AAAI Press 2015 pp.1090-1097. URL http://dl.acm.org/citation.cfm?id=2832249.2832400.

Uwagi

Opracowanie rekordu w ramach umowy 509/P-DUN/2018 ze środków MNiSW przeznaczonych na działalność upowszechniającą naukę (2018).