Model Checking for Probabilistic Multiagent Systems

被引:0
|
作者
Chen Fu
Andrea Turrini
Xiaowei Huang
Lei Song
Yuan Feng
Li-Jun Zhang
机构
[1] Chinese Academy of Sciences,State Key Laboratory of Computer Science, Institute of Software
[2] University of Chinese Academy of Sciences,Department of Computer Science
[3] Institute of Intelligent Software,Centre for Quantum Software and Information
[4] University of Liverpool,undefined
[5] Microsoft Research,undefined
[6] University of Technology Sydney,undefined
来源
Journal of Computer Science and Technology | 2023年 / 38卷
关键词
probabilistic multiagent system; model checking; uniform scheduler; probabilistic epistemic temporal logic;
D O I
暂无
中图分类号
学科分类号
摘要
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.
引用
收藏
页码:1162 / 1186
页数:24
相关论文
共 50 条
  • [21] Model checking probabilistic systems against pushdown specifications
    Dubslaff, Clemens
    Baier, Christel
    Berg, Manuela
    INFORMATION PROCESSING LETTERS, 2012, 112 (8-9) : 320 - 328
  • [22] Logic and Model Checking by Imprecise Probabilistic Interpreted Systems
    Termine, Alberto
    Antonucci, Alessandro
    Primiero, Giuseppe
    Facchini, Alessandro
    MULTI-AGENT SYSTEMS, EUMAS 2021, 2021, 12802 : 211 - 227
  • [23] Probabilistic Model Checking for Feature-Oriented Systems
    Dubslaff, Clemens
    Baier, Christel
    Klueppelholz, Sascha
    TRANSACTIONS ON ASPECT-ORIENTED SOFTWARE DEVELOPMENT XII, 2015, 8989 : 180 - 220
  • [24] Quantitative refinement and model checking for the analysis of probabilistic systems
    McIver, A. K.
    FM 2006: FORMAL METHODS, PROCEEDINGS, 2006, 4085 : 131 - 146
  • [25] MODEL CHECKING KNOWLEDGE AND COMMITMENTS IN MULTIAGENT SYSTEMS USING ACTORS AND UPPAAL
    Nigro, Christian
    Nigro, Libero
    Sciammarella, Paolo F.
    32ND EUROPEAN CONFERENCE ON MODELLING AND SIMULATION (ECMS 2018), 2018, : 136 - 142
  • [26] Probabilistic Model Checking
    Baier, Christel
    DEPENDABLE SOFTWARE SYSTEMS ENGINEERING, 2016, 45 : 1 - 23
  • [27] Model checking epistemic-probabilistic logic using probabilistic interpreted systems
    Wan, Wei
    Bentahar, Jamal
    Ben Hamza, Abdessamad
    KNOWLEDGE-BASED SYSTEMS, 2013, 50 : 279 - 295
  • [28] Probabilistic model checking of biological systems with uncertain kinetic rates
    Barbuti, Roberto
    Levi, Francesca
    Milazzo, Paolo
    Scatena, Guido
    THEORETICAL COMPUTER SCIENCE, 2012, 419 : 2 - 16
  • [29] Towards probabilistic model checking on P systems using PRISM
    Romero-Campero, Francisco J.
    Gheorghe, Marian
    Bianco, Luca
    Pescini, Dario
    Perez-Jimenez, Mario J.
    Ceterchi, Rodica
    MEMBRANE COMPUTING, 2006, 4361 : 477 - +
  • [30] MODEL-CHECKING FOR PROBABILISTIC REAL-TIME SYSTEMS
    ALUR, R
    COURCOUBETIS, C
    DILL, D
    LECTURE NOTES IN COMPUTER SCIENCE, 1991, 510 : 115 - 126