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

作者：Wongpiromsarn Tichakorn^*; Topcu Ufuk; Lamperski Andrew

来源：IEEE Transactions on Automatic Control, 2016, 61(11): 3344-3355.

DOI：10.1109/TAC.2015.2511722

• Automata
• barrier certificates
• linear temporal logic

We consider temporal logic verification of (possibly nonlinear) dynamical systems evolvingover 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.

• 出版日期2016-11