AAAI Publications, Twenty-Eighth AAAI Conference on Artificial Intelligence

Font Size: 
Symbolic Model Checking Epistemic Strategy Logic
Xiaowei Huang, Ron van der Meyden

Last modified: 2014-06-21


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.


Model checking; strategy; the logic of knowledge

Full Text: PDF