Abstract

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.

Original languageEnglish (US)
Title of host publicationProceedings of the 18th International Conference on Hybrid Systems
Subtitle of host publicationComputation and Control, HSCC 2015
PublisherAssociation for Computing Machinery
Pages169-178
Number of pages10
ISBN (Electronic)9781450334334
DOIs
StatePublished - Apr 14 2015
Event18th ACM International Conference on Hybrid Systems: Computation and Control, HSCC 2015 - Seattle, United States
Duration: Apr 14 2015Apr 16 2015

Publication series

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

Other

Other18th ACM International Conference on Hybrid Systems: Computation and Control, HSCC 2015
Country/TerritoryUnited States
CitySeattle
Period4/14/154/16/15

ASJC Scopus subject areas

  • Computer Networks and Communications
  • Computer Science Applications
  • Control and Systems Engineering
  • Electrical and Electronic Engineering

Fingerprint

Dive into the research topics of 'Statistical verification of dynamical systems using set oriented methods'. Together they form a unique fingerprint.

Cite this