Amaury Pouly (MPI-SWS, Saarbrücken)

We consider the problem of checking whether a switching system can reach a particular state. We show that even this problem is undecidable but decidable in some restricted cases. A switching system is a particular form of hybrid system very commonly used to model electrical systems with several states. It consists of a finite number of state and in each state, the system evolves according to a linear differential equation. This type of model is also used in modelisation to over-approximate the possible behaviours of a physical system when the transition rules between states are unclear. Our result shows a surprising connection with number of theorems from algebraic and transcendental number theory, and Hilbert’s Tenth Problem. One possible interpretation of this work is that switching systems, despite their innocent look, are already too powerful a model of computation.