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 条

[31] Model checking cooperative multi-agent systems in BDI logic
Chen, Q. (tpchen@jnu.edu.cn), 1600, Binary Information Press, Flat F 8th Floor, Block 3, Tanner Garden, 18 Tanner Road, Hong Kong (09):
[32] Model Checking Systems Against Epistemic Specifications
Lomuscio, Alessio R.
ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2014, (146):
[33] Declarative specifications for the development of multi-agent systems
Challenger, Moharram
Mernik, Marjan
Kardas, Geylani
Kosar, Tomaz
COMPUTER STANDARDS & INTERFACES, 2016, 43 : 91 - 115
[34] Prioritizing quality specifications of Multi-agent systems
Bedi, Punam
Gaur, Vibha
WORLD CONGRESS ON ENGINEERING 2007, VOLS 1 AND 2, 2007, : 541 - +
[35] Verification of Multi-Agent Systems via Predicate Abstraction against ATLK Specifications
Lomuscio, Alessio
Michliszyn, Jakub
AAMAS'16: PROCEEDINGS OF THE 2016 INTERNATIONAL CONFERENCE ON AUTONOMOUS AGENTS & MULTIAGENT SYSTEMS, 2016, : 662 - 670
[36] Module Checking of Pushdown Multi-agent Systems
Bozzelli, Laura
Murano, Aniello
Peron, Adriano
KR2020: PROCEEDINGS OF THE 17TH INTERNATIONAL CONFERENCE ON PRINCIPLES OF KNOWLEDGE REPRESENTATION AND REASONING, 2020, : 162 - 171
[37] Checking multi-agent systems behavior properties
Dekhtyar, M
Dikovsky, A
Valiev, M
2002 IEEE INTERNATIONAL CONFERENCE ON ARTIFICIAL INTELLIGENCE SYSTEMS, PROCEEDINGS, 2002, : 308 - 313
[38] Model checking multi-agent systems with logic based Petri nets
Behrens, Tristan M.
Dix, Juergen
ANNALS OF MATHEMATICS AND ARTIFICIAL INTELLIGENCE, 2007, 51 (2-4) : 81 - 121
[39] Model Checking and Strategy Synthesis for Multi-agent Systems for Resource Allocation
Timm, Nils
Botha, Josua
FORMAL METHODS: FOUNDATIONS AND APPLICATIONS, SBMF 2021, 2021, 13130 : 53 - 69
[40] Model checking multi-agent systems with logic based Petri nets
Tristan M. Behrens
Jürgen Dix
Annals of Mathematics and Artificial Intelligence, 2007, 51 : 81 - 121

← 1 2 3 4 5 →