Satisfaction of linear temporal logic specifications through recurrence tools for hybrid systems
Systems and Control
2020-11-17 v1 Formal Languages and Automata Theory
Systems and Control
Dynamical Systems
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.
Cite
@article{arxiv.2011.07149,
title = {Satisfaction of linear temporal logic specifications through recurrence tools for hybrid systems},
author = {Andrea Bisoffi and Dimos V. Dimarogonas},
journal= {arXiv preprint arXiv:2011.07149},
year = {2020}
}
Comments
To appear in IEEE Transactions on Automatic Control