Automata Theory Meets Barrier Certificates: Temporal Logic Verification of Nonlinear Systems

Tichakorn Wongpiromsarn, Ufuk Topcu, Andrew Lamperski

Research output: Contribution to journalArticlepeer-review

10 Scopus citations

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 languageEnglish (US)
Pages (from-to)3344-3355
Number of pages12
JournalIEEE Transactions on Automatic Control
Volume61
Issue number11
DOIs
StatePublished - Nov 2016

Bibliographical note

Funding Information:
This work was supported in part by the AFOSR (FA9550-12-1-0302)

Keywords

  • Automata
  • barrier certificates
  • linear temporal logic

Fingerprint Dive into the research topics of 'Automata Theory Meets Barrier Certificates: Temporal Logic Verification of Nonlinear Systems'. Together they form a unique fingerprint.

Cite this