Symbolic Model Checking Epistemic Strategy Logic

AAAI 2014 pp. 1426-1432

doi:10.1609/AAAI.V28I1.8894 /aaai/2014/huang2014aaai-symbolic/

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.

PDF AAAI Semantic Scholar

Cite

Text

Huang and van der Meyden. "Symbolic Model Checking Epistemic Strategy Logic." AAAI Conference on Artificial Intelligence, 2014. doi:10.1609/AAAI.V28I1.8894

Markdown

[Huang and van der Meyden. "Symbolic Model Checking Epistemic Strategy Logic." AAAI Conference on Artificial Intelligence, 2014.](https://mlanthology.org/aaai/2014/huang2014aaai-symbolic/) doi:10.1609/AAAI.V28I1.8894

BibTeX

@inproceedings{huang2014aaai-symbolic,
  title     = {{Symbolic Model Checking Epistemic Strategy Logic}},
  author    = {Huang, Xiaowei and van der Meyden, Ron},
  booktitle = {AAAI Conference on Artificial Intelligence},
  year      = {2014},
  pages     = {1426-1432},
  doi       = {10.1609/AAAI.V28I1.8894},
  url       = {https://mlanthology.org/aaai/2014/huang2014aaai-symbolic/}
}