A hybrid barrier certificate approach to satisfy linear temporal logic specifications

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.

Cited by in corpus (4)

• Learning Hybrid Control Barrier Functions from Data
• Satisfaction of linear temporal logic specifications through recurrence tools for hybrid systems
• Technical Report: Reactive Planning for Mobile Manipulation Tasks in Unexplored Semantic Environments
• Reactive Temporal Logic Planning for Multiple Robots in Unknown Occupancy Grid Maps