Abstract
We consider temporal logic verification of (possibly nonlinear) dynamical systems evolving over continuous state spaces. Our approach combines automata-based verification and the use of so-called barrier certificates. Automata-based verification allows the decomposition the verification task into a finite collection of simpler constraints over the continuous state space. The satisfaction of these constraints in turn can be (potentially conservatively) proved by appropriately constructed barrier certificates. As a result, our approach, together with optimization-based search for barrier certificates, allows computational verification of dynamical systems against temporal logic properties while avoiding explicit abstractions of the dynamics as commonly done in literature.
Original language | English (US) |
---|---|
Pages (from-to) | 3344-3355 |
Number of pages | 12 |
Journal | IEEE Transactions on Automatic Control |
Volume | 61 |
Issue number | 11 |
DOIs | |
State | Published - Nov 2016 |
Bibliographical note
Funding Information:This work was supported in part by the AFOSR (FA9550-12-1-0302)
Publisher Copyright:
© 1963-2012 IEEE.
Keywords
- Automata
- barrier certificates
- linear temporal logic