AI Chat Paper
Note: Please note that the following content is generated by AMiner AI. SciOpen does not take any responsibility related to this content.
{{lang === 'zh_CN' ? '文章概述' : 'Summary'}}
{{lang === 'en_US' ? '中' : 'Eng'}}
Chat more with AI
Powered by AMiner. Clicking this button will take you away from SciOpen.
Home Journal of Computer Science and Technology Article
Article Link
Cite
EndNote(RIS) BibTeX
Collect
Submit Manuscript
Show Outline
Outline
Show full outline
Hide outline
Outline
Show full outline
Hide outline
Regular Paper

Model Checking for Probabilistic Multiagent Systems

State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing 100190, China
University of Chinese Academy of Sciences, Beijing 100049, China
Institute of Intelligent Software, Guangzhou 511455, China
Department of Computer Science, University of Liverpool, Liverpool L693BX, U.K.
Microsoft Research, Beijing 100190, China
Centre for Quantum Software and Information, University of Technology Sydney, Sydney 2007, Australia
Show Author Information

Abstract

In multiagent systems, agents usually do not have complete information of the whole system, which makes the analysis of such systems hard. The incompleteness of information is normally modelled by means of accessibility relations, and the schedulers consistent with such relations are called uniform. In this paper, we consider probabilistic multiagent systems with accessibility relations and focus on the model checking problem with respect to the probabilistic epistemic temporal logic, which can specify both temporal and epistemic properties. However, the problem is undecidable in general. We show that it becomes decidable when restricted to memoryless uniform schedulers. Then, we present two algorithms for this case: one reduces the model checking problem into a mixed integer non-linear programming (MINLP) problem, which can then be solved by Satisfiability Modulo Theories (SMT) solvers, and the other is an approximate algorithm based on the upper confidence bounds applied to trees (UCT) algorithm, which can return a result whenever queried. These algorithms have been implemented in an existing model checker and then validated on experiments. The experimental results show the efficiency and extendability of these algorithms, and the algorithm based on UCT outperforms the one based on MINLP in most cases.

Keywords

probabilistic multiagent systemmodel checkinguniform schedulerprobabilistic epistemic temporal logic

Electronic Supplementary Material

Download File(s)
JCST-2012-11218-Highlights.pdf (139.1 KB)

References

[1]

Seuken S, Zilberstein S. Formal models and algorithms for decentralized decision making under uncertainty. Autonomous Agents and Multi-Agent Systems, 2008, 17(2): 190–250. DOI: 10.1007/s10458-007-9026-5.
Crossref Google Scholar
[2]
Bernstein D S, Zilberstein S, Washington R, Bresina J L. Planetary rover control as a Markov decision process. In Proc. the 6th Int. Symp. Artificial Intelligence, Robotics, and Automation in Space, Jun. 2001.
[3]
Nair R, Varakantham P, Tambe M, Yokoo M. Networked distributed POMDPs: A synthesis of distributed constraint optimization and POMDPs. In Proc. the 20th National Conf. Artificial Intelligence and the 17th Innovative Applications of Artificial Intelligence Conference, Jul. 2005, pp.133–139. DOI: 10.5555/1619332.1619356.
[4]

Pynadath D V, Tambe M. The communicative multiagent team decision problem: Analyzing teamwork theories and models. Journal of Artificial Intelligence Research, 2002, 16: 389–423. DOI: 10.1613/jair.1024.
Crossref Google Scholar
[5]
Kaźmierczak P, Ågotnes T, Jamroga W. Multi-agency is coordination and (limited) communication. In Proc. the 17th Int. Conf. Principles and Practice of Multi-Agent Systems, Dec. 2014, pp.91–106. DOI: 10.1007/978-3-319-13191-7_8.
Crossref
[6]
Delgado C, Benevides M. Verification of epistemic properties in probabilistic multi-agent systems. In Proc. the 7th German Conference on Multiagent System Technologies, Sept. 2009, pp.16–28. DOI: 10.1007/978-3-642-04143-3_3.
Crossref
[7]
Fagin R, Halpern J Y, Moses Y, Vardi M Y. Reasoning About Knowledge. The MIT Press, 2004. DOI: 10.7551/mitpress/5803.001.0001.
Crossref
[8]
Jonsson B, Larsen K G. Specification and refinement of probabilistic processes. In Proc. the 6th Annual IEEE Symposium on Logic in Computer Science, Jul. 1991, pp.266–277. DOI: 10.1109/LICS.1991.151651.
Crossref
[9]
Baier C, Katoen J P. Principles of Model Checking. The MIT Press, 2008.
[10]
De Moura L, Bjørner N. Z3: An efficient SMT solver. In Proc. the 14th Int. Conf. Tools and Algorithms for the Construction and Analysis of Systems, Mar. 2008, pp.337–340. DOI: 10.1007/978-3-540-78800-3_24.
Crossref
[11]
Kocsis L, Szepesvári C. Bandit based Monte-Carlo planning. In Proc. the 17th European Conf. Machine Learning, Sept. 2006, pp.282–293. DOI: 10.1007/11871842_29.
Crossref
[12]
Keller T, Eyerich P. PROST: Probabilistic planning based on UCT. In Proc. the 22nd International Conference on Automated Planning and Scheduling, June 2012, pp.119–127. DOI: 10.1609/icaps.v22i1.13518.
Crossref
[13]

Coles A, Coles A, Olaya A G, Jiménez S, López C L, Sanner S, Yoon S. A survey of the seventh international planning competition. AI Magazine, 2012, 33(1): 83–88. DOI: 10.1609/aimag.v33i1.2392.
Crossref Google Scholar
[14]

Vallati M, Chrpa L, Grześ M, McCluskey T L, Roberts M, Sanner S. The 2014 international planning competition: Progress and trends. AI Magazine, 2015, 36(3): 90–98. DOI: 10.1609/aimag.v36i3.2571.
Crossref Google Scholar
[15]
Hartmanns A, Klauck M, Parker D, Quatmann T, Ruijters E. The quantitative verification benchmark set. In Proc. the 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Apr. 2019, pp.344–350. DOI: 10.1007/978-3-030-17462-0_20.
Crossref
[16]
Fu C, Turrini A, Huang X W, Song L, Feng Y, Zhang L J. Model checking probabilistic epistemic logic for probabilistic multiagent systems. In Proc. the 27th International Joint Conference on Artificial Intelligence, Jul. 2018, pp.4757–4763. DOI: 10.24963/ijcai.2018/661.
Crossref
[17]
Huang X W, Luo C. A logic of probabilistic knowledge and strategy. In Proc. the 12th International Conference on Autonomous Agents and Multi-Agent Systems, May 2013, pp.845–852. DOI: 10.5555/2484920.2485055.
[18]

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.
Crossref Google Scholar
[19]

Jamroga W, Van Der Hoek W. Agents that know how to play. Fundamenta Informaticae, 2004, 63(2/3): 185–219.
Google Scholar
[20]

Rabin M O. Probabilistic automata. Information and Control, 1963, 6(3): 230–245. DOI: 10.1016/S0019-9958(63) 90290-0.
Crossref Google Scholar
[21]
Paz A. Introduction to Probabilistic Automata. Academic Press, 1971. DOI: 10.1016/C2013-0-11297-4.
Crossref
[22]

Madani O, Hanks S, Condon A. On the undecidability of probabilistic planning and related stochastic optimization problems. Artificial Intelligence, 2003, 147(1/2): 5–34. DOI: 10.1016/S0004-3702(02)00378-8.
Crossref Google Scholar
[23]
Madani O, Hanks S, Condon A. On the undecidability of probabilistic planning and infinite-horizon partially observable Markov decision problems. In Proc. the 16th National Conference on Artificial Intelligence and the 11th Innovative Applications of Artificial Intelligence, Jul. 1999, pp.541–548. DOI: 10.5555/315149.315395.
[24]
Mundhenk M. The complexity of planning with partially-observable Markov decision processes. Computer Science Technical Report TR2000-376, Dartmouth College, 2000. https://digitalcommons.dartmouth.edu/cs_tr/176/, Sept. 2023.
[25]
Bellman R E. Dynamic Programming. Princeton University Press, 1957.
[26]
Kolobov A, Mausam, Weld D. LRTDP versus UCT for online probabilistic planning. In Proc. the 26th AAAI Conference on Artificial Intelligence, Jul. 2012, pp.1786–1792. DOI: 10.1609/aaai.v26i1.8362.
Crossref
[27]
Younes H L S, Simmons R G. Probabilistic verification of discrete event systems using acceptance sampling. In Proc. the 14th Int. Conf. Computer Aided Verification, Jul. 2002, pp.223–235. DOI: 10.1007/3-540-45657-0_17.
Crossref
[28]
Hérault T, Lassaigne R, Magniette F, Peyronnet S. Approximate probabilistic model checking. In Proc. the 5th Int. Conf. Verification, Model Checking, and Abstract Interpretation, Jan. 2004, pp.73–84. DOI: 10.1007/978-3-540-24622-0_8.
Crossref
[29]
Henriques D, Martins J G, Zuliani P, Platzer A, Clarke E M. Statistical model checking for Markov decision processes. In Proc. the 9th International Conference on Quantitative Evaluation of Systems, Sept. 2012, pp.84–93. DOI: 10.1109/QEST.2012.19.
Crossref
[30]
D’Argenio P R, Hartmanns A, Sedwards S. Lightweight statistical model checking in nondeterministic continuous time. In Proc. the 8th Int. Symp. Leveraging Applications of Formal Methods, Verification and Validation, Nov. 2018, pp.336–353. DOI: 10.1007/978-3-030-03421-4_22.
Crossref
[31]
Ashok P, Kretínský J, Weininger M. PAC statistical model checking for Markov decision processes and stochastic games. In Proc. the 31st International Conference on Computer Aided Verification, Jul. 2019, pp.497–519. DOI: 10.1007/978-3-030-25540-4_29.
Crossref
[32]
Hahn E M, Li Y, Schewe S, Turrini A, Zhang L J. IscasMC: A Web-based probabilistic model checker. In Proc. the 19th Int. Symp. Formal Methods, May 2014, pp.312–317. DOI: 10.1007/978-3-319-06410-9_22.
Crossref
[33]
Kwiatkowska M, Norman G, Parker D, Santos G. PRISM-games 3.0: Stochastic game verification with concurrency, equilibria and time. In Proc. the 32nd International Conference on Computer Aided Verification, Jul. 2020, pp.475–487. DOI: 10.1007/978-3-030-53291-8_25.
Crossref
[34]
Kwiatkowska M, Parker D, Simaitis A. Strategic analysis of trust models for user-centric networks. In Proc. the 1st International Workshop on Strategic Reasoning, Mar. 2013, pp.53–59. DOI: 10.4204/EPTCS.112.10.
Crossref
[35]

Kwiatkowska M, Norman G, Parker D, Santos G. Automatic verification of concurrent stochastic systems. Formal Methods in System Design, 2021, 58(1/2): 188–250. DOI: 10.1007/s10703-020-00356-y.
Crossref Google Scholar
[36]
Kwiatkowska M, Norman G, Parker D, Santos G. Multi-player equilibria verification for concurrent stochastic games. In Proc. the 17th International Conference on Quantitative Evaluation of Systems, Aug. 2020, pp.74–95. DOI: 10.1007/978-3-030-59854-9_7.
Crossref
[37]
Huang X W, Su K L, Zhang C Y. Probabilistic alternating-time temporal logic of incomplete information and synchronous perfect recall. In Proc. the 26th AAAI Conference on Artificial Intelligence, Jul. 2012, pp.765–771. DOI: 10.1609/aaai.v26i1.8214.
Crossref
[38]

Huang X W, Van Der Meyden R. An epistemic strategy logic. ACM Trans. Computational Logic, 2018, 19(4): Article No. 26. DOI: 10.1145/3233769.
Crossref Google Scholar
[39]

Chatterjee K, Doyen L, Henzinger T A. A survey of partial-observation stochastic parity games. Formal Methods in System Design, 2013, 43(2): 268–284. DOI: 10.1007/ s10703-012-0164-2.
Crossref Google Scholar
[40]

Chatterjee K, Doyen L. Partial-observation stochastic games: How to win when belief fails. ACM Trans. Computational Logic, 2014, 15(2): Article No. 16. DOI: 10.1145/2579 821.
Crossref Google Scholar
[41]
Schnoor H. Strategic planning for probabilistic games with incomplete information. In Proc. the 9th Int. Conf. Autonomous Agents and Multiagent Systems, May 2010, pp.1057–1064. DOI: 10.5555/1838206.1838349.
[42]
Huang X W, Luo C, Van Der Meyden R. Symbolic model checking of probabilistic knowledge. In Proc. the 13th Conference on Theoretical Aspects of Rationality and Knowledge, Jul. 2011, pp.177–186. DOI: 10.1145/2000378.2000399.
Crossref
[43]

Wan W, Bentahar J, Hamza A B. Model checking epistemic-probabilistic logic using probabilistic interpreted systems. Knowledge-Based Systems, 2013, 50: 279–295. DOI: 10.1016/j.knosys.2013.06.017.
Crossref Google Scholar
[44]

Sultan K, Bentahar J, Wan W, Al-Saqqar F. Modeling and verifying probabilistic multi-agent systems using knowledge and social commitments. Expert Systems with Applications, 2014, 41(14): 6291–6304. DOI: 10.1016/j.eswa.2014.04.008.
Crossref Google Scholar
[45]
Kwiatkowska M Z, Norman G, Parker D. PRISM 4.0: Verification of probabilistic real-time systems. In Proc. the 23rd Int. Conf. Computer Aided Verification, Jul. 2011, pp.585–591. DOI: 10.1007/978-3-642-22110-1_47.
Crossref
[46]

Lomuscio A, Qu H Y, Raimondi F. MCMAS: An open-source model checker for the verification of multi-agent systems. International Journal on Software Tools for Tech nology Transfer, 2017, 19(1): 9–30. DOI: 10.1007/s10009-015-0378-x.
Crossref Google Scholar
[47]
Gammie P, Van Der Meyden R. MCK: Model checking the logic of knowledge. In Proc. the 16th International Conference on Computer Aided Verification, Jul. 2004, pp.479–483. DOI: 10.1007/978-3-540-27813-9_41.
Crossref
[48]
Kumar A, Zilberstein S. Dynamic programming approximations for partially observable stochastic games. In Proc. the 22nd International FLAIRS Conference, May 2009, pp.547–552.
[49]
Winterer L, Wimmer R, Jansen N, Becker B. Strengthening deterministic policies for POMDPs. In Proc. the 12th International Symposium on NASA Formal Methods, May 2020, pp.115–132. DOI: 10.1007/978-3-030-55754-6_7.
Crossref
[50]
Oliehoek F A, Amato C. A Concise Introduction to Decentralized POMDPs. Springer, 2016. DOI: 10.1007/978-3-319-28929-8.
Crossref
[51]

Norman G, Parker D, Zou X Y. Verification and control of partially observable probabilistic systems. Real-Time Systems, 2017, 53(3): 354–402. DOI: 10.1007/s11241-017-9269-4.
Crossref Google Scholar
[52]
Pnueli A. The temporal logic of programs. In Proc. the 18th Annual Symp. Foundations of Computer Science, Oct. 31–Nov. 2, 1977, pp.46–57. DOI: 10.1109/SFCS.1977.32.
Crossref
[53]

Huang X W, Kwiatkowska M, Olejnik M. Reasoning about cognitive trust in stochastic multiagent systems. ACM Trans. Computational Logic, 2019, 20(4): Article No. 21. DOI: 10.1145/3329123.
Crossref Google Scholar
Journal of Computer Science and Technology
Volume 38 Issue 5,
September 2023
Pages 1162-1186
DOI: 10.1007/s11390-022-1218-6
Cite this article:
Fu C, Turrini A, Huang X, et al. Model Checking for Probabilistic Multiagent Systems. Journal of Computer Science and Technology, 2023, 38(5): 1162-1186. https://doi.org/10.1007/s11390-022-1218-6

336

Views

0

Crossref

0

Web of Science

0

Scopus

0

CSCD

Altmetrics
Received: 13 December 2020
Accepted: 27 March 2022
Published: 30 September 2023
© Institute of Computing Technology, Chinese Academy of Sciences 2023
Return