TY - GEN

T1 - Statistical verification of dynamical systems using set oriented methods

AU - Wang, Yu

AU - Roohi, Nima

AU - West, Matthew

AU - Viswanathan, Mahesh

AU - Dullerud, Geir E.

N1 - Publisher Copyright:
© 2015 ACM.

PY - 2015/4/14

Y1 - 2015/4/14

N2 - Modeling, analyzing and verifying real physical systems has long been a challenging task since the state space of the systems is usually infinite and the dynamics of the systems is generally nonlinear and stochastic. In this work, we employ an extension of linear temporal logic (LTL) to describe the behavior of discrete-time nonlinear stochastic systems; this extension is so-called linear inequality LTL (iLTL) which allows for atomic propositions that are linear inequalities on state spaces. To statistically verify iLTL formulas on the systems, we first reformulate discrete-time nonlinear stochastic dynamical systems into Markov processes on their continuous state spaces and then reduce them to discrete-time Markov chains (DTMC) using set-oriented methods. Furthermore, a statistical verification algorithm is proposed to verify iLTL formulas on the reduced systems. The correctness of this statistical verification algorithm is checked both by theoretical analysis and the simulation of a fluid problem. We will show in the successive work that the framework extends to hybrid systems, which is a significant motivation for the approach taken.

AB - Modeling, analyzing and verifying real physical systems has long been a challenging task since the state space of the systems is usually infinite and the dynamics of the systems is generally nonlinear and stochastic. In this work, we employ an extension of linear temporal logic (LTL) to describe the behavior of discrete-time nonlinear stochastic systems; this extension is so-called linear inequality LTL (iLTL) which allows for atomic propositions that are linear inequalities on state spaces. To statistically verify iLTL formulas on the systems, we first reformulate discrete-time nonlinear stochastic dynamical systems into Markov processes on their continuous state spaces and then reduce them to discrete-time Markov chains (DTMC) using set-oriented methods. Furthermore, a statistical verification algorithm is proposed to verify iLTL formulas on the reduced systems. The correctness of this statistical verification algorithm is checked both by theoretical analysis and the simulation of a fluid problem. We will show in the successive work that the framework extends to hybrid systems, which is a significant motivation for the approach taken.

UR - http://www.scopus.com/inward/record.url?scp=84940665176&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84940665176&partnerID=8YFLogxK

U2 - 10.1145/2728606.2728627

DO - 10.1145/2728606.2728627

M3 - Conference contribution

AN - SCOPUS:84940665176

T3 - Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control, HSCC 2015

SP - 169

EP - 178

BT - Proceedings of the 18th International Conference on Hybrid Systems

PB - Association for Computing Machinery

T2 - 18th ACM International Conference on Hybrid Systems: Computation and Control, HSCC 2015

Y2 - 14 April 2015 through 16 April 2015

ER -