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 条
  • [1] Model Checking Multi-Agent Systems against LDLK Specifications
    Kong, Jeremy
    Lomuscio, Alessio
    PROCEEDINGS OF THE TWENTY-SIXTH INTERNATIONAL JOINT CONFERENCE ON ARTIFICIAL INTELLIGENCE, 2017, : 1138 - 1144
  • [2] Symbolic Model Checking Multi-Agent Systems against CTL*K Specifications
    Kong, Jeremy
    Lomuscio, Alessio
    AAMAS'17: PROCEEDINGS OF THE 16TH INTERNATIONAL CONFERENCE ON AUTONOMOUS AGENTS AND MULTIAGENT SYSTEMS, 2017, : 114 - 122
  • [3] Decidability of model checking multi-agent systems against a class of EHS specifications
    Lomuscio, Alessio R.
    Michaliszyn, Jakub
    21ST EUROPEAN CONFERENCE ON ARTIFICIAL INTELLIGENCE (ECAI 2014), 2014, 263 : 543 - 548
  • [4] Model Checking Multi-Agent Systems against Epistemic HS Specifications with Regular Expressions
    Lomuscio, Alessio
    Michaliszyn, Jakub
    FIFTEENTH INTERNATIONAL CONFERENCE ON THE PRINCIPLES OF KNOWLEDGE REPRESENTATION AND REASONING, 2016, : 298 - 307
  • [5] Checking Multi-Agent Systems against Temporal-Epistemic Specifications
    Chen, Ran
    Zhang, Wenhui
    2019 24TH INTERNATIONAL CONFERENCE ON ENGINEERING OF COMPLEX COMPUTER SYSTEMS (ICECCS 2019), 2019, : 21 - 30
  • [6] Decidability of Model Checking Multi-Agent Systems with Regular Expressions against Epistemic HS Specifications
    Michaliszyn, Jakub
    Witkowski, Piotr
    PROCEEDINGS OF THE TWENTY-EIGHTH INTERNATIONAL JOINT CONFERENCE ON ARTIFICIAL INTELLIGENCE, 2019, : 4746 - 4752
  • [7] Multi-Agent Automata and Its Application to LDLK Satisfiability Checking
    Gao, Ya
    Zhang, Wenhui
    Zhu, Xue-Yang
    2021 IEEE 21ST INTERNATIONAL CONFERENCE ON SOFTWARE QUALITY, RELIABILITY AND SECURITY (QRS 2021), 2021, : 1024 - 1035
  • [8] Model checking multi-agent systems
    Yuan Mengting
    Yu Chao
    2007 INTERNATIONAL CONFERENCE ON SERVICE SYSTEMS AND SERVICE MANAGEMENT, VOLS 1-3, 2007, : 567 - +
  • [9] Model Checking Multi-Agent Systems
    Bourahla, Mustapha
    Benmohamed, Mohamed
    INFORMATICA-JOURNAL OF COMPUTING AND INFORMATICS, 2005, 29 (02): : 189 - 197
  • [10] Abstraction for model checking multi-agent systems
    Zhou, Conghua
    Sun, Bo
    Liu, Zhifeng
    FRONTIERS OF COMPUTER SCIENCE IN CHINA, 2011, 5 (01): : 14 - 25
12345