Model checking temporal epistemic logic under bounded recall
File(s)
Accepted version
Author(s)
Belardinelli, Francesco
Lomuscio, Alessio
Yu, Emily
Type
Conference Paper
Abstract
We study the problem of verifying multi-agent systems under the assumption of bounded recall. We introduce the logic CTLKBR, a bounded-recall variant of the temporal-epistemic logic CTLK. We define and study the model checking problem against CTLK specifications under incomplete information and bounded recall and present complexity upper bounds. We present an extension of the BDD-based model checker MCMAS implementing model checking under bounded recall semantics and discuss the experimental results obtained.
Date Issued
2020-06-02
Date Acceptance
2020-02-01
Citation
Proceedings of the AAAI Conference on Artificial Intelligence, 34, 2020, 34 (5), pp.7071-7078
ISSN
2159-5399
Publisher
AAAI Press
Start Page
7071
End Page
7078
Journal / Book Title
Proceedings of the AAAI Conference on Artificial Intelligence, 34
Volume
34
Issue
5
Copyright Statement
© 2020, Association for the Advancement of Artificial Intelligence All Rights Reserved.
Identifier
https://www.webofscience.com/api/gateway?GWVersion=2&SrcApp=PARTNER_APP&SrcAuth=LinksAMR&KeyUT=WOS:000667722807019&DestLinkType=FullRecord&DestApp=ALL_WOS&UsrCustomerID=a2bf6146997ec60c407a63945d4e92bb
Source
34th AAAI Conference on Artificial Intelligence / 32nd Innovative Applications of Artificial Intelligence Conference / 10th AAAI Symposium on Educational Advances in Artificial Intelligence
Subjects
ALGORITHMS
Computer Science
Computer Science, Artificial Intelligence
Computer Science, Interdisciplinary Applications
Education & Educational Research
Education, Scientific Disciplines
KNOWLEDGE
Science & Technology
Social Sciences
Technology
Publication Status
Published
Start Date
2020-02-07
Finish Date
2020-02-12
Coverage Spatial
New York, NY, USA