An Automaton Learning Approach to Solving Safety Games over Infinite Graphs
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 proposed 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 in dynamic environments.
Code (0)
등록된 구현이 없습니다.
Tasks
Motion PlanningSimilar Papers 제목 키워드 기반
Learning-Based Synthesis of Safety Controllers
We propose a machine learning framework to synthesize reactive controllers for systems whose interactions with their adversarial environment are modeled by infinite-duration, two-player games over (potentially) infinite …
Motion PlanningAsymmetric Equilibria in Symmetric Multiplayer Prisoners Dilemma Supergames
We propose a finite automaton-style solution concept for supergames. In our model, we define an equilibrium to be a cycle of state switches and a supergame to be an infinite walk on states of a finite stage game. We show…
A Finite Population Destroys a Traveling Wave in Spatial Replicator Dynamics
We derive both the finite and infinite population spatial replicator dynamics as the fluid limit of a stochastic cellular automaton. The infinite population spatial replicator is identical to the model used by Vickers an…
Ambiguity Hierarchy of Regular Infinite Tree Languages
An automaton is unambiguous if for every input it has at most one accepting computation. An automaton is k-ambiguous (for k > 0) if for every input it has at most k accepting computations. An automaton is boundedly ambig…
Bidding Games on Markov Decision Processes with Quantitative Reachability Objectives
Graph games are fundamental in strategic reasoning of multi-agent systems and their environments. We study a new family of graph games which combine stochastic environmental uncertainties and auction-based interactions a…