Symbolic Model Checking Epistemic Strategy Logic

Authors

  • Xiaowei Huang The University of New South Wales
  • Ron van der Meyden The University of New South Wales

DOI:

https://doi.org/10.1609/aaai.v28i1.8894

Keywords:

Model checking, strategy, the logic of knowledge

Abstract

This paper presents a symbolic BDD-based model checking algorithm for an epistemic strategy logic with observational semantics. The logic has been shown to be more expressive than several variants of ATELand therefore the algorithm can also be used for ATEL model checking. We implement the algorithm in a model checker and apply it to an application on train control system. The performance of the algorithm is also reported, with a comparison showing improved results over a previous partially symbolic approach for ATEL model checking.

AAAI 2014 Proceedings Cover

Downloads

Published

2014-06-21

How to Cite

Huang, X., & van der Meyden, R. (2014). Symbolic Model Checking Epistemic Strategy Logic. Proceedings of the AAAI Conference on Artificial Intelligence, 28(1). https://doi.org/10.1609/aaai.v28i1.8894

Issue

Vol. 28 No. 1 (2014): Twenty-Eighth AAAI Conference on Artificial Intelligence

Section

AAAI Technical Track: Multiagent Systems