Model Checking Multi-Agent Systems against LDLK Specifications on Finite Traces

被引：0
|
作者：
Kong, Jeremy [1 ]
Lomuscio, Alessio [1 ]
机构：
[1] Imperial Coll London, Dept Comp, London, England
来源：
PROCEEDINGS OF THE 17TH INTERNATIONAL CONFERENCE ON AUTONOMOUS AGENTS AND MULTIAGENT SYSTEMS (AAMAS' 18) | 2018年
关键词：
Verification; model checking; epistemic logic; LDL;
D O I：
暂无
中图分类号：
TP [自动化技术、计算机技术];
学科分类号：
0812 ;
摘要：
We introduce the logic LDLfK, a variant of the epistemic logic LDLK, interpreted on finite traces of multi-agent systems. We explore the verification problem of multi-agent systems against LDLfK specifications and give algorithms for the reduction of LDLfK model checking to LDLK verification on a different model and different specification. We analyse the resulting complexity and show it to be PSPACE-complete. We report on a full implementation of the algorithm and assess its performance on a number of examples.
引用
收藏
页码：166 / 174
页数：9
相关论文
共 50 条
  • [41] Reduction Model Checking for Multi-Agent Systems of Group Social Commitments
    AlFawwaz, Bader M.
    Al-Saqqar, Faisal
    AL-Shatnawi, Atallah
    COMPUTATION, 2022, 10 (06)
  • [42] Model checking algorithm for temporal logics of knowledge in multi-agent systems
    Wu, Li-Jun
    Su, Kai-Le
    Ruan Jian Xue Bao/Journal of Software, 2004, 15 (07): : 1012 - 1020
  • [43] Verifying Multi-agent Programs by Model Checking
    Rafael H. Bordini
    Michael Fisher
    Willem Visser
    Michael Wooldridge
    Autonomous Agents and Multi-Agent Systems, 2006, 12 : 239 - 256
  • [44] Model checking multi-agent programs with CASP
    Bordini, RH
    Fisher, M
    Pardavila, C
    Visser, W
    Wooldridge, M
    COMPUTER AIDED VERIFICATION, 2003, 2725 : 110 - 113
  • [45] Verifying multi-agent programs by model checking
    Bordini, RH
    Fisher, M
    Visser, W
    Wooldridge, M
    AUTONOMOUS AGENTS AND MULTI-AGENT SYSTEMS, 2006, 12 (02) : 239 - 256
  • [46] Model checking probabilistic systems against pushdown specifications
    Dubslaff, Clemens
    Baier, Christel
    Berg, Manuela
    INFORMATION PROCESSING LETTERS, 2012, 112 (8-9) : 320 - 328
  • [47] Decomposition of Finite LTL Specifications for Efficient Multi-agent Planning
    Schillinger, Philipp
    Buerger, Mathias
    Dimarogonas, Dimos V.
    DISTRIBUTED AUTONOMOUS ROBOTIC SYSTEMS, 2019, 6 : 253 - 267
  • [48] Runnable specifications of interactions for open multi-agent systems
    Mathieu, P
    Routier, JC
    Secq, Y
    IKE'03: PROCEEDINGS OF THE INTERNATIONAL CONFERENCE ON INFORMATION AND KNOWLEDGE ENGINEERING, VOLS 1 AND 2, 2003, : 431 - 437
  • [49] On vector trajectory specifications for multi-agent product systems
    Romanovski, I
    Caines, PE
    PROCEEDINGS OF THE 40TH IEEE CONFERENCE ON DECISION AND CONTROL, VOLS 1-5, 2001, : 2333 - 2334
  • [50] Bounded model checking algorithm to reduce the state space in multi-agent systems
    Zhou, Cong-Hua
    Ye, Meng
    Wang, Chang-Da
    Liu, Zhi-Feng
    Ruan Jian Xue Bao/Journal of Software, 2012, 23 (11): : 2835 - 2861
12345