Satisfaction of linear temporal logic specifications through recurrence tools for hybrid systems

TL;DR

This paper presents a method for ensuring that linear plants satisfy linear temporal logic specifications by leveraging recurrence concepts in hybrid systems, avoiding discretization and verified through simulations.

Contribution

It introduces a novel approach linking recurrence in hybrid systems to LTL satisfaction, with relaxed Lyapunov-like conditions for certification.

Findings

Certifies LTL satisfaction without plant discretization

Extends Lyapunov conditions for recurrence in hybrid systems

Validated approach through simulations

Abstract

In this work we formulate the problem of satisfying a linear temporal logic formula on a linear plant with output feedback, through a recent hybrid systems formalism. We relate this problem to the notion of recurrence introduced for the considered formalism, and we then extend Lyapunov-like conditions for recurrence of an open, unbounded set. One of the proposed relaxed conditions allows certifying recurrence of a suitable set, and this guarantees that the high-level evolution of the plant satisfies the formula, without relying on discretizations of the plant. Simulations illustrate the proposed approach.