Model Checking for Probabilistic Multiagent Systems  

作　　者：付辰 Andrea Turrini 黄小炜 宋磊 冯元 张立军 Chen Fu;Andrea Turrini;Xiaowei Huang;Lei Song;Yuan Feng;Li-Jun Zhang(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)

机构地区：[1]State Key Laboratory of Computer Science,Institute of Software,Chinese Academy of Sciences,Beijing 100190,China [2]University of Chinese Academy of Sciences,Beijing 100049,China [3]Institute of Intelligent Software,Guangzhou 511455,China [4]Department of Computer Science,University of Liverpool,Liverpool L693BX,U.K [5]Microsoft Research,Beijing 100190,China [6]Centre for Quantum Software and Information,University of Technology Sydney,Sydney 2007,Australia

出　　处：《Journal of Computer Science & Technology》2023年第5期1162-1186,共25页计算机科学技术学报（英文版）

基　　金：supported by the National Natural Science Foundation of China under Grant No.61836005;the Australian Research Council under Grant Nos.DP220102059 and DP180100691。

摘　　要：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.

关 键 词：probabilistic multiagent system model checking uniform scheduler probabilistic epistemic temporal logic 

分 类 号：TP18[自动化与计算机技术—控制理论与控制工程]