Mode sequences as symbolic states in abstractions of incrementally stable switched systems

We present a novel approach to the computation of symbolic abstractions of incrementally stable switched systems. The main novelty consists in using mode sequences of given length as symbolic states for our abstractions. We show that the resulting symbolic models are approximately bisimilar to the original switched system and that an arbitrary precision can be achieved by considering sufficiently long mode sequences. The advantage of this approach over existing ones is double: firstly, the transition relation of the symbolic model admits a very compact representation under the form of a shift operator; secondly, our approach does not use lattices over the state-space and can potentially be used for higher dimensional systems. We provide a theoretical comparison with the lattice-based approach and present a simple criterion enabling to choose the most appropriate approach for a given switched system. Finally, we show an application to a model of road traffic for which we synthesize a schedule for the coordination of traffic lights under constraints of safety and fairness.