Journal of Computer Science and Technology


Model Checking for Probabilistic Multiagent Systems

Chen Fu1,2(付辰), Andrea Turrini1,3, Xiaowei Huang4(黄小炜), Lei Song5(宋磊), Yuan Feng6(冯元), and Lijun Zhang1,2,3(张立军), Senior Member, CCF   

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

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 one 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.


1、 研究背景(context):
2、 目的(Objective):
3、 方法(Method):
对于无记忆的一致策略下的模型检验问题,本文提出了两种算法,一种是将模型检验问题转换为非线性整数规划问题(MINLP),然后通过SMT(Satisfiability Modulo Theories)求解器解决。另一种是近似算法,基于UCT(the Upper Confidence bounds applied to Trees)算法,这是一种基于蒙特卡洛树搜索的算法。
4、 结果(Result & Findings):
5、 结论(Conclusions):
本文研究了概率多智能体系统中的概率认知时序逻辑的模型检验问题,并对可判定的子类问题提出了两种算法,包括一个精确算法和一个近似算法。实验结果证明了这两种算法的有效性。本文工作的局限在于未考虑交替时序逻辑(Alternating Temporal Logic)和随机化策略(Randomised Schedulers),在下一步工作中,我们将进行这些方向上的尝试。

Key words: probabilistic multiagent system, model checking, uniform scheduler, probabilistic epistemic temporal logic


No related articles found!
Full text



[1] Wang Jianchao; Wei Daozheng;. An Effective Test Generation Algorithm for Combinational Circuits[J]. , 1986, 1(4): 1 -16 .
[2] HU Zhanyi(胡占义),LEI Cheng(雷成)and TSUI Hung Tat(徐孔达). Robot Self-Location by Line Correspondence[J]. , 2001, 16(2): 0 .
[3] Mohamed El Bachir Menai and Tasniem Nasser Al-Yahya. A Taxonomy of Exact Methods for Partial Max-SAT[J]. , 2013, 28(2): 232 -246 .
[4] Zhi-Guo Wan, Robert H. Deng, David Lee, Ying Li. MicroBTC: Efficient, Flexible and Fair Micropayment for Bitcoin Using Hash Chains[J]. Journal of Computer Science and Technology, 2019, 34(2): 403 -415 .
[5] Wan-Wei Liu, Fu Song, Tang-Hao-Ran Zhang, Ji Wang. Verifying ReLU Neural Networks from a Model Checking Perspective[J]. Journal of Computer Science and Technology, 2020, 35(6): 1365 -1381 .
[6] Ning Bao, Yun-Peng Chai, Xiao Qin, and Chuan-Wen Wang. MacroTrend: A Write-Efficient Cache Algorithm for NVM-Based Read Cache[J]. Journal of Computer Science and Technology, 2022, 37(1): 207 -230 .
[7] Gen Zhang, Peng-Fei Wang, Tai Yue, Xu Zhou, Kai Lu. MEBS: Uncovering Memory Life-Cycle Bugs in Operating System Kernels[J]. Journal of Computer Science and Technology, 2021, 36(6): 1248 -1268 .
[8] Lu-Tan Zhao, Rui Hou, Kai Wang, Yu-Lan Su, Pei-Nan Li, Dan Meng. A Novel Probabilistic Saturating Counter Design for Secure Branch Predictor[J]. Journal of Computer Science and Technology, 2021, 36(5): 1022 -1036 .
[9] Tao Xie, Shengchao Qin, Wenhui Zhang. Preface[J]. Journal of Computer Science and Technology, 2021, 36(6): 1229 -1230 .
[10] Li-Li Xiao, Hui-Biao Zhu, Qi-Wen Xu. Trace Semantics and Algebraic Laws for Total Store Order Memory Model[J]. Journal of Computer Science and Technology, 2021, 36(6): 1269 -1290 .

ISSN 1000-9000(Print)

CN 11-2296/TP

Editorial Board
Author Guidelines
Journal of Computer Science and Technology
Institute of Computing Technology, Chinese Academy of Sciences
P.O. Box 2704, Beijing 100190 P.R. China
  Copyright ©2015 JCST, All Rights Reserved