An Automaton Learning Approach to Solving Safety Games over Infinite Graphs

Abstract

We propose a method to construct finite-state reactive controllers for systems whose interactions with their adversarial environment are modeled by infinite-duration two-player games over possibly infinite graphs. The method targets safety games with infinitely many states or with such a large number of states that it would be impractical--if not impossible--for conventional synthesis techniques that work on the entire state space. We resort to constructing finite-state controllers for such systems through an automata learning approach, utilizing a symbolic representation of the underlying game that is based on finite automata. Throughout the learning process, the learner maintains an approximation of the winning region represented as a finite automaton and refines it using different types of counterexamples provided by the teacher until a satisfactory controller can be derived if one exists. We present a symbolic representation of safety games inspired by regular model checking, propose implementations of the learner and teacher, and evaluate their performance on examples motivated by robotic motion planning.