Multi-valued Verification of Strategic Ability

• Autorzy: Jamroga Wojciech , Konikowska Beata , Kurpiewski Damian , Penczek Wojciech

Identyfikatory

DOI

10.3233/FI-2020-1955

• Języki publikacji: EN

Abstrakty

EN

Some multi-agent scenarios call for the possibility of evaluating specifications in a richer domain of truth values. Examples include runtime monitoring of a temporal property over a growing prefix of an infinite path, inconsistency analysis in distributed databases, and verification methods that use incomplete anytime algorithms, such as bounded model checking. In this paper, we present multi-valued alternating-time temporal logic (mv-ATL_→^∗ ), an expressive logic to specify strategic abilities in multi-agent systems. It is well known that, for branching-time logics, a general method for model-independent translation from multi-valued to two-valued model checking exists. We show that the method cannot be directly extended to mv-ATL _→^∗. We also propose two ways of overcoming the problem. Firstly, we identify constraints on formulas for which the model-independent translation can be suitably adapted. Secondly, we present a model-dependent reduction that can be applied to all formulas of mv-ATL_→^∗ . We show that, in all cases, the complexity of verification increases only linearly when new truth values are added to the evaluation domain. We also consider several examples that show possible applications of mv-ATL_→^∗ and motivate its use for model checking multi-agent systems.

Słowa kluczowe

EN

multiagent systems; logic; distributed databases

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2020
• Tom: Vol. 175, nr 1-4
• Strony: 207--251
• Opis fizyczny: Bibliogr. 70 poz., rys., tab.

Twórcy

autor

Jamroga Wojciech

• Institute of Computer Science, Polish Academy of Sciences, Jana Kazimierza 5, 01-248 Warsaw, Poland

autor

Konikowska Beata

• Institute of Computer Science, Polish Academy of Sciences, Jana Kazimierza 5, 01-248 Warsaw, Poland

autor

Kurpiewski Damian

• Institute of Computer Science, Polish Academy of Sciences, Jana Kazimierza 5, 01-248 Warsaw, Poland

autor

Penczek Wojciech

• Institute of Computer Science, Polish Academy of Sciences, Jana Kazimierza 5, 01-248 Warsaw, Poland

Bibliografia

• [1] Alur R, Henzinger T. A, Kupferman O. Alternating-Time Temporal Logic. In: Proceedings of FOCS. IEEE Computer Society Press, 1997 pp. 100-109.
• [2] Alur R, Henzinger T. A, Kupferman O. Alternating-Time Temporal Logic. Journal of the ACM, 2002. 49:672-713. doi:10.1145/585265.585270.
• [3] Konikowska B, Penczek W. Model Checking for Multi-valued Computation Tree Logics. In: Fitting M, Orłowska E (eds.), Beyond Two: Theory and Applications of Multiple Valued Logic, pp. 193-210. Physica-Verlag, 2003. doi:10.1007/978-3-7908-1769-0_8.
• [4] Konikowska B, Penczek W. Model Checking of Multivalued Logic of Knowledge and Time. In: Proceedings of AAMAS. ACM Press, 2006 pp. 169-176. doi:10.1145/1160633.1160661.
• [5] Bauer A, Leucker M, Schallhart C. Monitoring of Real-Time Properties. In: Proceedings of FSTTCS, volume 4337 of Lecture Notes in Computer Science. Springer, 2006 pp. 260-272. doi:10.1007/11944836_25.
• [6] Bauer A, Leucker M, Schallhart C. The Good, the Bad, and the Ugly, But How Ugly Is Ugly? In: Proceedings of RV, volume 4839 of Lecture Notes in Computer Science. Springer, 2007 pp. 126-138. doi:10.1007/978-3-540-77395-5_11.
• [7] Biere A, Cimatti A, Clarke E, Zhu Y. Symbolic Model Checking Without BDDs. In: Proceedings of TACAS, volume 1579 of Lecture Notes in Computer Science. Springer, 1999 pp. 193-207. doi:10.1007/3-540-49059-0_14.
• [8] Penczek W, Lomuscio A. Verifying Epistemic Properties of Multi-Agent Systems via Bounded Model Checking. In: Proceedings of AAMAS. ACM Press, 2003 pp. 209-216.
• [9] Lomuscio A, Qu H, Raimondi F. MCMAS: An Open-Source Model Checker for the Verification of Multi-Agent Systems. International Journal on Software Tools for Technology Transfer, 2015. Availabe online. doi:10.1007/s10009-015-0378-x.
• [10] Jamroga W, Konikowska B, Penczek W. Multi-valued Verification of Strategic Ability. In: Proceedings of AAMAS. ACM Press, 2016 pp. 1180-1189.
• [11] Fitting M. Many-valued Modal Logics. Fundamenta Informaticae, 1991. 15(3-4):335-350.
• [12] Fitting M. Many-valued Modal Logics II. Fundamenta Informaticae, 1992. 17:55-73.
• [13] Vijzelaar S, Fokkink W. Multi-valued Abstraction Using Lattice Operations. In: Proceedings of ACSD. 2015 pp. 70-79. doi:10.1109/ACSD.2015.18.
• [14] Gurfinkel A, Chechik M. Multi-valued Model Checking via Classical Model Checking. In: Proceedings of CONCUR, volume 2761 of LNCS. Springer-Verlag, 2003 pp. 266-280. doi:10.1007/978-3-540-45187-7_18.
• [15] Bruns G, Godefroid P. Model Checking with Multi-valued Logics. In: ICALP. 2004 pp. 281-293. doi:10.1007/978-3-540-27836-8_26.
• [16] Shoham S, Grumberg O. Multi-valued Model Checking Games. J. Comput. Syst. Sci., 2012. 78(2):414-429. doi:10.1016/j.jcss.2011.05.003.
• [17] Pan H, Li Y, Cao Y, Ma Z. Model Checking Computation Tree Logic over Finite Lattices. Theoretical Computer Science, 2016. 612:45-62. doi:10.1016/j.tcs.2015.10.014.
• [18] Aminof B, Kupferman O, Murano A. Improved Model Checking of Hierarchical Systems. Information Computation, 2012. 210:68-86. doi:10.1016/j.ic.2011.10.008.
• [19] Kwiatkowska M, Norman G, Parker D. PRISM: Probabilistic Symbolic Model Checker. In: Proceedings of TOOLS, volume 2324 of Lecture Notes in Computer Science. Springer, 2002 pp. 200-204. doi:10.1007/3-540-46029-2_13.
• [20] Godefroid P, Jagadeesan R. On the Expressiveness of 3-Valued Models. In: Proceedings of VMCAI, volume 2575 of LNCS. Springer-Verlag, 2003 pp. 206-222. doi:10.1007/3-540-36384-X_18.
• [21] Huth M, Jagadeesan R, Schmidt D. A. A Domain Equation for Refinement of Partial Systems. Mathematical Structures in Computer Science, 2004. 14:469-505. doi:10.1017/S0960129504004268.
• [22] Huth M, Pradhan S. Consistent Partial Model Checking. In: Proc. of the Workshop on Domains VI, volume 73 of ENTCS. Elsevier, 2004 pp. 45-85. doi:10.1016/j.entcs.2004.08.003.
• [23] Kouvaros P, Lomuscio A. Parameterised Verification of Infinite State Multi-Agent Systems via Predicate Abstraction. In: Proceedings of AAAI. 2017 pp. 3013-3020.
• [24] Belardinelli F, Lomuscio A, Malvone V. Approximating Perfect Recall When Model Checking Strategic Abilities. In: Principles of Knowledge Representation and Reasoning: Proceedings of KR. 2018 pp. 435-444. ID:52969829.
• [25] Belardinelli F, Lomuscio A, Malvone V. An Abstraction-Based Method for Verifying Strategic Properties in Multi-Agent Systems with Imperfect Information. In: The Thirty-Third AAAI Conference on Artificial Intelligence, AAAI 2019, The Thirty-First Innovative Applications of Artificial Intelligence Conference, IAAI 2019, The Ninth AAAI Symposium on Educational Advances in Artificial Intelligence, EAAI 2019. 2019 pp. 6030-6037. doi:10.1609/aaai.v33i01.33016030.
• [26] Maluszynski J, Szalas A. Logical Foundations and Complexity of 4QL, a Query Language with Unrestricted Negation. Journal of Applied Non-Classical Logics, 2011. 21(2):211-232. doi:10.3166/jancl.21.211-232.
• [27] Maluszynski J, Szalas A. Partiality and Inconsistency in Agents’ Belief Bases. In: Proceedings of KESAMSTA, volume 252 of Frontiers in Artificial Intelligence and Applications. IOS Press, 2013 pp. 3-17. doi:10.3233/978-1-61499-254-7-3.
• [28] Ball T, Kupferman O. An Abstraction-Refinement Framework for Multi-Agent Systems. In: Proceedings of LICS. IEEE Computer Society, 2006 pp. 379-388. doi:10.1109/LICS.2006.10.
• [29] Lomuscio A, Michaliszyn J. Verifying Multi-Agent Systems by Model Checking Three-valued Abstractions. In: Proceedings of AAMAS. 2015 pp. 189-198.
• [30] Belardinelli F, Lomuscio A. Agent-based Abstractions for Verifying Alternating-time Temporal Logic with Imperfect Information. In: Proceedings of AAMAS. 2017 pp. 1259-1267.
• [31] de Alfaro L, Faella M, Henzinger T, Majumdar R, Stoelinga M. Model Checking Discounted Temporal properties. Theoretical Computer Science, 2005. 345:139-170. doi:10.1016/j.tcs.2005.07.033.
• [32] Lluch-Lafuente A, Montanari U. Quantitative μ-Calculus and CTL Based on Constraint Semirings. Electr. Notes Theor. Comput. Sci., 2005. 112:37-59. doi:10.1016/j.entcs.2004.02.063.
• [33] Jamroga W. A Temporal Logic for Markov Chains. In: Proceedings of AAMAS. 2008 pp. 697-704.
• [34] Jamroga W. A Temporal Logic for Stochastic Multi-Agent Systems. In: Proceedings of PRIMA, volume 5357 of Lecture Notes in Computer Science. 2008 pp. 239-250. doi:10.1007/978-3-540-89674-6_27.
• [35] Huth M, Kwiatkowska M. Quantitative Analysis and Model Checking. In: Logic in Computer Science. 1997 pp. 111-122. doi:10.1109/LICS.1997.614940.
• [36] Baier C, Kwiatkowska M, Norman G. Computing Probability Bounds for Linear Time Formulas over Concurrent Probabilistic Systems. Electronic Notes in Theoretical Computer Science, 1999. 21(19). doi:10.1016/S1571-0661(05)80595-X.
• [37] Bulling N, Jamroga W. What Agents Can Probably Enforce. Fundamenta Informaticae, 2009. 93(1-3):81-96. doi:10.3233/FI-2009-0089.
• [38] Huang X, Su K, Zhang C. Probabilistic Alternating-Time Temporal Logic of Incomplete Information and Synchronous Perfect Recall. In: Proceedings of AAAI. 2012.
• [39] Chen T, Forejt V, Kwiatkowska M, Parker D, Simaitis A. PRISM-games: A Model Checker for Stochastic Multi-Player Games. In: Proceedings of TACAS, volume 7795 of Lecture Notes in Computer Science. Springer, 2013 pp. 185-191. doi:10.1007/978-3-642-36742-7_13.
• [40] Birkhoff G. Lattice Theory (2nd edition). American Mathematical Society, 1948.
• [41] Davey B. A, Priestley H. A. Introduction to Lattices and Order. Cambridge University Press, 1990. ISBN:10:0521367662, 13:978-0521367660.
• [42] Cousot P, Cousot R. Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints. In: Conference Record of the Fourth ACM Symposium on Principles of Programming Languages. 1977 pp. 238-252. doi:10.1145/512950.512973.
• [43] Clarke E, Grumberg O, Long D. Model Checking and Abstraction. ACM Transactions on Programming Languages and Systems, 1994. 16(5):1512-1542. doi:10.1145/186025.186051.
• [44] Schobbens P. Y. Alternating-Time Logic with Imperfect Recall. Electronic Notes in Theoretical Computer Science, 2004. 85(2):82-93. doi:10.1016/S1571-0661(05)82604-0.
• [45] Hansson H, Jonsson B. A Logic for Reasoning about Time and Reliability. Formal Asp. Comput., 1994. 6(5):512-535. doi:10.1007/BF01211866.
• [46] Godefroid P, Jagadeesan R. Automatic Abstraction Using Generalized Model Checking. In: Proceedings of CAV, volume 2404 of Lecture Notes in Computer Science. Springer, 2002 pp. 137-150. doi:10.1007/3-540-45657-0_11.
• [47] Jamroga W. Some Remarks on Alternating Temporal Epistemic Logic. In: Dunin-Keplicz B, Verbrugge R (eds.), Proceedings of FAMAS. 2003 pp. 133-140.
• [48] Ågotnes T. A Note on Syntactic Characterization of Incomplete Information in ATEL. In: Proceedings of Workshop on Knowledge and Games. 2004 pp. 34-42. ID:17497178.
• [49] Jamroga W, van der Hoek W. Agents that Know how to Play. Fundamenta Informaticae, 2004. 63(2-3):185-219.
• [50] Ågotnes T. Action and Knowledge in Alternating-time Temporal Logic. Synthese, 2006. 149(2):377-409. doi:10.1007/s11229-005-3875-8.
• [51] Jamroga W, Ågotnes T. Constructive Knowledge: What Agents Can Achieve under Incomplete Information. Journal of Applied Non-Classical Logics, 2007. 17(4):423-475. doi:10.3166/jancl.17.423-475.
• [52] Schnoor H. Strategic Planning for Probabilistic Games with Incomplete Information. In: Proceedings of AAMAS. 2010 pp. 1057-1064. doi:10.1145/1838206.1838349.
• [53] Jamroga W, Dix J. Model Checking Abilities of Agents: A Closer Look. Theory of Computing Systems, 2008. 42(3):366-410. doi:10.1007/s00224-007-9080-z.
• [54] Bulling N, Dix J, Jamroga W. Model Checking Logics of Strategic Ability: Complexity. In: Dastani M, Hindriks K, Meyer JJ (eds.), Specification and Verification of Multi-Agent Systems, pp. 125-159. Springer, 2010. doi:10.1007/978-1-4419-6984-2_5.
• [55] Dima C, Tiplea F. Model-Checking ATL under Imperfect Information and Perfect Recall Semantics is Undecidable. CoRR, 2011. abs/1102.4225.
• [56] Bulling N, Jamroga W. Comparing Variants of Strategic Ability: How Uncertainty and Memory Influence General Properties of Games. Journal of Autonomous Agents and Multi-Agent Systems, 2014. 28(3):474-518. doi:10.1007/s10458-013-9231-3.
• [57] Pilecki J, Bednarczyk M, Jamroga W. Synthesis and Verification of Uniform Strategies for Multi-Agent Systems. In: Proceedings of CLIMA XV, volume 8624 of Lecture Notes in Computer Science. Springer, 2014 pp. 166-182. doi:10.1007/978-3-319-09764-0_11.
• [58] Busard S, Pecheur C, Qu H, Raimondi F. Improving the Model Checking of Strategies under Partial Observability and Fairness Constraints. In: Formal Methods and Software Engineering, volume 8829 of Lecture Notes in Computer Science, pp. 27-42. Springer. ISBN 978-3-319-11736-2, 2014. doi:10.1007/978-3-319-11737-9_3.
• [59] Huang X, van der Meyden R. Symbolic Model Checking Epistemic Strategy Logic. In: Proceedings of AAAI Conference on Artificial Intelligence. AAAI Press, 2014 pp. 1426-1432.
• [60] Cermak P, Lomuscio A, Mogavero F, Murano A. MCMAS-SLK: A Model Checker for the Verification of Strategy Logic Specifications. In: Proc. of CAV’14, volume 8559 of LNCS. Springer-Verlag, 2014 pp. 525-532. doi:10.1007/978-3-319-08867-9_34.
• [61] Jamroga W, Knapik M, Kurpiewski D, Mikulski L. Approximate Verification of Strategic Abilities under Imperfect Information. Artif. Intell., 2019. 277. doi:10.1016/j.artint.2019.103172.
• [62] Kurpiewski D, Knapik M, Jamroga W. On Domination and Control in Strategic Ability. In: Proceedings of AAMAS. 2019 pp. 197-205. ID:169031456.
• [63] Jamroga W, Knapik M, Kurpiewski D. Fixpoint Approximation of Strategic Abilities under Imperfect Information. In: Proceedings of AAMAS. IFAAMAS, 2017 pp. 1241-1249.
• [64] Ågotnes T, Goranko V, Jamroga W, Wooldridge M. Knowledge and Ability. In: van Ditmarsch H, Halpern J, van der Hoek W, Kooi B (eds.), Handbook of Epistemic Logic, pp. 543-589. College Publications, 2015.
• [65] Jamroga W. Logical Methods for Specification and Verification of Multi-Agent Systems. ICS PAS Publishing House, 2015. ISBN:978-83-63159-25-2.
• [66] Jamroga W, Dix J. Model Checking ATLir is Indeed ΔP2 -complete. In: Proceedings of EUMAS, volume 223 of CEUR Workshop Proceedings. 2006.
• [67] Busard S. Symbolic Model Checking of Multi-Modal Logics: Uniform Strategies and Rich Explanations. Ph.D. thesis, Universite Catholique de Louvain, 2017. URL http://hdl.handle.net/2078.1/186372.
• [68] Mogavero F, Murano A, Vardi M. Reasoning About Strategies. In: Proceedings of FSTTCS. 2010 pp. 133-144. doi:10.4230/LIPIcs.FSTTCS.2010.133.
• [69] Mogavero F, Murano A, Perelli G, Vardi M. Reasoning About Strategies: On the Model-Checking Problem. ACM Transactions on Computational Logic, 2014. 15(4):1-42. doi:10.1145/2631917.
• [70] Berthon R, Maubert B, Murano A, Rubin S, Vardi MY. Strategy Logic with Imperfect Information. In: Proceedings of LICS. 2017 pp. 1-12. doi:10.1109/LICS.2017.8005136.

Uwagi

Opracowanie rekordu ze środków MNiSW, umowa Nr 461252 w ramach programu "Społeczna odpowiedzialność nauki" - moduł: Popularyzacja nauki i promocja sportu (2020).