Safety synthesis for incrementally stable switched systems using discretization-free multi-resolution abstractions

Control of continuous and hybrid systems using discrete abstractions often suffers from scalability issues, due to the use of state space partitions as symbolic states. In this paper, for incrementally stable switched systems, we introduce a class of abstractions that do not rely on state space partitions but use mode sequences as symbolic states. Our approach differs from existing works by the possibility of considering sequences of varying length, giving the possibility to adjust locally the resolution of the abstraction. Temporal constraints on the switching signal can also be taken into account. We thus define multi-resolution bisimilar abstractions that enjoy interesting properties that can be used to design specific algorithms to synthesize safety controllers. These algorithms need not compute the full abstraction that is built incrementally during controller synthesis, exploring finer resolutions only when the specification cannot be enforced at the coarser level. We illustrate the approach by a numerical example inspired by road traffic regulation.