Statistical Verification of Dynamical Systems Using Set Oriented Methods

Abstract:

Modeling, analyzing and verifying real physical systems have long been a changeling task since the dynamics are usually nonlinear and the state spaces are always continuous. In this work, we use linear inequality LTL (iLTL), a temporal logic, to specify the behavior of nonlinear dynamical systems over time and propose a framework for statistical verification of temporal formulae on nonlinear systems using set oriented methods. In the approach presented a discrete‐time nonlinear dynamical system is first transformed into a Markov process on the continuous state space. Then the Markov process is reduced to a new Markov process that is equivalent to a discrete time Markov chain (DTMC), using set oriented method. Furthermore, the iLTL formulae of the original Markov chain are also reduced to iLTL formulae of the new Markov chain. Finally, the reduced iLTL formulae are verified using a statistical model  checker. The correctness of this framework is guaranteed by combining the errors introduced in every step. We remark that this framework may also extend to the study of more general system models.