A hybrid barrier certificate approach to satisfy linear temporal logic specifications

TL;DR

This paper introduces a hybrid barrier certificate method to ensure physical systems satisfy linear temporal logic specifications, extending hybrid system frameworks with an eventuality property for improved formal verification.

Contribution

It develops a novel hybrid barrier certificate approach incorporating an extension of the hybrid system framework to verify LTL specifications.

Findings

Successfully formalizes LTL satisfaction via hybrid barrier certificates

Demonstrates effectiveness through simulations

Extends hybrid system formalism with an eventuality property

Abstract

In this work we formulate the satisfaction of a (syntactically co-safe) linear temporal logic specification on a physical plant through a recent hybrid dynamical systems formalism. In order to solve this problem, we introduce an extension to such a hybrid system framework of the so-called eventuality property, which matches suitably the condition for the satisfaction of such a temporal logic specification. The eventuality property can be established through barrier certificates, which we derive for the considered hybrid system framework. Using a hybrid barrier certificate, we propose a solution to the original problem. Simulations illustrate the effectiveness of the proposed method.