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