Timed Game Abstraction of Control Systems

TL;DR

This paper introduces a method for abstracting control systems into timed game automata using Lyapunov-based state space partitioning, enabling automatic controller synthesis with soundness guarantees.

Contribution

It presents a novel abstraction technique that extends timed game automata to a broader class of control systems through Lyapunov functions and invariant sets.

Findings

Effective state space partitioning for control systems

Extension of timed game automata for richer control classes

Successful application to a navigation control problem

Abstract

This paper proposes a method for abstracting control systems by timed game automata, and is aimed at obtaining automatic controller synthesis. The proposed abstraction is based on partitioning the state space of a control system using positive and negative invariant sets, generated by Lyapunov functions. This partitioning ensures that the vector field of the control system is transversal to the facets of the cells, which induces some desirable properties of the abstraction. To allow a rich class of control systems to be abstracted, the update maps of the timed game automaton are extended. Conditions on the partitioning of the state space and the control are set up to obtain sound abstractions. Finally, an example is provided to demonstrate the method applied to a control problem related to navigation.