Model Checking for Probabilistic Multiagent Systems
作者机构：State Key Laboratory of Computer ScienceInstitute of SoftwareChinese Academy of SciencesBeijing 100190China University of Chinese Academy of SciencesBeijing 100049China Institute of Intelligent SoftwareGuangzhou 511455China Department of Computer ScienceUniversity of LiverpoolLiverpool L693BXU.K Microsoft ResearchBeijing 100190China Centre for Quantum Software and InformationUniversity of Technology SydneySydney 2007Australia
出 版 物：《Journal of Computer Science & Technology》 (计算机科学技术学报（英文版）)
年 卷 期：2023年第38卷第5期
页 面：1162-1186页
核心收录：
学科分类：12[管理学] 1201[管理学-管理科学与工程(可授管理学、工学学位)] 081104[工学-模式识别与智能系统] 08[工学] 0835[工学-软件工程] 0811[工学-控制科学与工程] 0812[工学-计算机科学与技术（可授工学、理学学位）]
基 金：supported by the National Natural Science Foundation of China under Grant No.61836005 the Australian Research Council under Grant Nos.DP220102059 and DP180100691
主 题：probabilistic multiagent system model checking uniform scheduler probabilistic epistemic temporal logic
摘 要：In multiagent systems,agents usually do not have complete information of the whole system,which makes the analysis of such systems *** incompleteness of information is normally modelled by means of accessibility relations,and the schedulers consistent with such relations are called *** 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 ***,the problem is undecidable in *** show that it becomes decidable when restricted to memoryless uniform ***,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 *** algorithms have been implemented in an existing model checker and then validated on *** 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.
维普期刊数据库