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):
实验结果表明,基于MINLP的算法能够给出精确的结果,但能处理的模型规模较小,且表现严重依赖SMT求解器。而基于UCT的算法能够处理的模型规模较大,能够在更短时间内给出结果,而且它是一个任意时间算法,即能够在运行过程中给出当前发现的结果。基于UCT算法的局限性在于它是近似算法,表现可能会随着随机数的改变发生变化,本文建议增大时间限制以缓解这个问题。
5、 结论(Conclusions):
本文研究了概率多智能体系统中的概率认知时序逻辑的模型检验问题,并对可判定的子类问题提出了两种算法,包括一个精确算法和一个近似算法。实验结果证明了这两种算法的有效性。本文工作的局限在于未考虑交替时序逻辑(Alternating Temporal Logic)和随机化策略(Randomised Schedulers),在下一步工作中,我们将进行这些方向上的尝试。


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

;

No related articles found!
Viewed
Full text


Abstract

Cited

  Shared   
  Discussed   
[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)

         1860-4749(Online)
CN 11-2296/TP

Home
Editorial Board
Author Guidelines
Subscription
Journal of Computer Science and Technology
Institute of Computing Technology, Chinese Academy of Sciences
P.O. Box 2704, Beijing 100190 P.R. China
Tel.:86-10-62610746
E-mail: jcst@ict.ac.cn
 
  Copyright ©2015 JCST, All Rights Reserved