Linear temporal logic for hybrid dynamical systems: characterizations and sufficient conditions

DOI10.1016/J.NAHS.2020.100865MaRDI QIDQ2178216zbMATH OpenOpenAlexFDO

Authors Hyejin Han, Ricardo G. Sanfelice

Publication date 7 May 2020

Published in Nonlinear Analysis. Hybrid Systems (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1807.02574

zbMATH Keywords

finite time attractivityforward invariancehybrid systemslinear temporal logic

Mathematics Subject Classification ID

Temporal logic (03B44) Control/observation systems governed by functional relations other than differential equations (such as hybrid and switching systems) (93C30)

Abstract: This paper introduces operators, semantics, characterizations, and solution-independent conditions to guarantee temporal logic specifications for hybrid dynamical systems. Hybrid dynamical systems are given in terms of differential inclusions -- capturing the continuous dynamics -- and difference inclusions -- capturing the discrete dynamics or events -- with constraints. State trajectories (or solutions) to such systems are parameterized by a hybrid notion of time. For such broad class of solutions, the operators and semantics needed to reason about temporal logic are introduced. Characterizations of temporal logic formulas in terms of dynamical properties of hybrid systems are presented -- in particular, forward invariance and finite time attractivity. These characterizations are exploited to formulate sufficient conditions assuring the satisfaction of temporal logic formulas -- when possible, these conditions do not involve solution information. Combining the results for formulas with a single operator, ways to certify more complex formulas are pointed out, in particular, via a decomposition using a finite state automaton. Academic examples illustrate the results throughout the paper.

Recommendations

• A Temporal Dynamic Logic for Verifying Hybrid System Invariants
• HRELTL: a temporal logic for hybrid systems
• Robust satisfaction of temporal logic over real-valued signals
• dTL\(^{2}\): differential temporal dynamic logic with nested temporalities for hybrid systems
• LTLC: Linear Temporal Logic for Control

Cites work

• A Fully Automated Framework for Control of Linear Systems from Temporal Logic Specifications
• An introduction to hybrid dynamical systems
• Dynamical properties of hybrid automata
• Finite time stability of sets for hybrid dynamical systems
• Formal methods for discrete-time dynamical systems
• Forward Invariance of Sets for Hybrid Dynamical Systems (Part I)
• HRELTL: a temporal logic for hybrid systems
• scientific article; zbMATH DE number 46303 (Why is no real title available?)
• scientific article; zbMATH DE number 1786477 (Why is no real title available?)
• Hybrid dynamical systems
• Hybrid dynamical systems. Modeling, stability, and robustness
• Impulsive and hybrid dynamical systems: stability, dissipativity, and control
• Invariance Principles for Hybrid Systems With Connections to Detectability and Asymptotic Stability
• Linear Time Logic Control of Discrete-Time Linear Systems
• LTL to Büchi automata translation: fast and more deterministic
• LTLC: Linear Temporal Logic for Control
• Nonlinear systems.
• On the equivalence between global recurrence and the existence of a smooth Lyapunov function for hybrid systems
• On the regularization of Zeno hybrid automata
• Reactive synthesis from signal temporal logic specifications
• Robustness of temporal logic specifications for continuous-time signals
• Temporal logic motion planning for dynamic robots

Cited in

(4)

• dTL\(^{2}\): differential temporal dynamic logic with nested temporalities for hybrid systems
• Robust satisfaction of temporal logic over real-valued signals
• Characterization of eventual conditional invariance for hybrid dynamical systems
• HRELTL: a temporal logic for hybrid systems

This page was built for publication: Linear temporal logic for hybrid dynamical systems: characterizations and sufficient conditions

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2178216)