Stability of discrete-time switched linear systems with ω-regular switching sequences

In this paper, we develop tools to analyze stability properties of discrete-time switched linear systems driven by switching signals belonging to a given omega- regular language. More precisely, we assume switching signals to be generated by a Buchi automaton where the alphabet corresponds to the modes of the switched system. We define notions of attractivity and uniform stability for this type of systems and also of uniform exponential stability when the considered Buchi automaton is deterministic. We then provide sufficient conditions to check these properties using Lyapunov and automata theoretic techniques. For a subclass of such systems with invertible matrices, we show that these conditions are also necessary. We finally show an example of application in the context of synchronization of oscillators over a communication network.