On a decidable formal theory for abstract continuous-time dynamical systems

Abstract

We propose a decidable formal theory which describes high-level properties of abstract continuous-time dynamical systems called Nondeterministic Complete Markovian Systems (NCMS). NCMS is a rather general class of systems which can represent discrete and/or continuous evolutions in continuous time and which is sufficient for modeling a wide range of real-time information processing and cyber-physical systems (CPS).We illustrate the obtained results with a proof of the mutual exclusion property of a CPS which implements Peterson’s algorithm.