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 -