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

Tichakorn Wongpiromsarn, Ufuk Topcu, Andrew Lamperski

Research output: Contribution to journalArticlepeer-review

27 Scopus citations


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
Issue number11
StatePublished - Nov 2016

Bibliographical note

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

Publisher Copyright:
© 1963-2012 IEEE.


  • Automata
  • barrier certificates
  • linear temporal logic


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