Automatic Verification of FSA Strategies via Counterexample-Guided Local Search for Invariants
Abstract
Strategy representation and reasoning has received much attention over the past years. In this paper, we consider the representation of general strategies that solve a class of (possibly infinitely many) games with similar structures, and their automatic verification, which is an undecidable problem. We propose to represent a general strategy by an FSA (Finite State Automaton) with edges labelled by restricted Golog programs. We formalize the semantics of FSA strategies in the situation calculus. Then we propose an incomplete method for verifying whether an FSA strategy is a winning strategy by counterexample-guided local search for appropriate invariants. We implemented our method and did experiments on combinatorial game and also single-agent domains. Experimental results showed that our system can successfully verify most of them within a reasonable amount of time.
Cite
Text
Luo and Liu. "Automatic Verification of FSA Strategies via Counterexample-Guided Local Search for Invariants." International Joint Conference on Artificial Intelligence, 2019. doi:10.24963/IJCAI.2019/251Markdown
[Luo and Liu. "Automatic Verification of FSA Strategies via Counterexample-Guided Local Search for Invariants." International Joint Conference on Artificial Intelligence, 2019.](https://mlanthology.org/ijcai/2019/luo2019ijcai-automatic/) doi:10.24963/IJCAI.2019/251BibTeX
@inproceedings{luo2019ijcai-automatic,
title = {{Automatic Verification of FSA Strategies via Counterexample-Guided Local Search for Invariants}},
author = {Luo, Kailun and Liu, Yongmei},
booktitle = {International Joint Conference on Artificial Intelligence},
year = {2019},
pages = {1814-1821},
doi = {10.24963/IJCAI.2019/251},
url = {https://mlanthology.org/ijcai/2019/luo2019ijcai-automatic/}
}