Bounded model checking of strategy ability with perfect recall

Huang, Xiaowei (2015) Bounded model checking of strategy ability with perfect recall. Artificial Intelligence, 222. pp. 182-200. ISSN 10.1016/j.artint.2015.01.005

Full text not available from this repository. (Request a copy)

Abstract

The paper works with a logic which has the expressiveness to quantify over strategies of bounded length. The semantics of the logic is based on systems with multiple agents. Agents have incomplete information about the underlying system state and their strategies are based on perfect recall memory over observations and local actions. The computational complexity of model checking is shown to be PSPACE-complete. We give two BDD-based model checking algorithms. The algorithms are implemented in a model checker and experimental results are reported to show their applications.

Item Type: Article
Uncontrolled Keywords: Model checking Strategy logic Incomplete information Perfect recall
Subjects: G400 Computer Science
Divisions: Faculty of Computing, Engineering and the Built Environment
Faculty of Computing, Engineering and the Built Environment > School of Computing and Digital Technology
Faculty of Computing, Engineering and the Built Environment > School of Computing and Digital Technology > Cyber Security
UoA Collections > UoA11: Computer Science and Informatics
Depositing User: $ Ian McDonald
Date Deposited: 11 Jul 2017 11:56
Last Modified: 11 Jul 2017 11:56
URI: http://www.open-access.bcu.ac.uk/id/eprint/4841

Actions (login required)

View Item View Item

Research

In this section...