A program logic to verify signal temporal logic specifications of hybrid systems
DOI10.1145/3447928.3456648arXiv2103.08117OpenAlexW3159513475WikidataQ130818558 ScholiaQ130818558MaRDI QIDQ6201590
Unnamed Author, Jean-Baptiste Jeannin
Publication date: 21 February 2024
Published in: Proceedings of the 24th International Conference on Hybrid Systems: Computation and Control (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/2103.08117
Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60) Control/observation systems governed by functional relations other than differential equations (such as hybrid and switching systems) (93C30)
Cites Work
- Unnamed Item
- Unnamed Item
- Differential dynamic logic for hybrid systems
- Descriptively complete process logic
- Process logic: Expressiveness, decidability, completeness
- An axiomatic approach to existence and liveness for differential equations
- STL model checking of continuous and hybrid systems
- TeLEx: learning signal temporal logic from positive examples using tightness metric
- Verifying safety and persistence in hybrid systems using flowpipes and continuous invariants
- Robust online monitoring of signal temporal logic
- Logics of Dynamical Systems
- Reactive synthesis from signal temporal logic specifications
- dTL2: Differential Temporal Dynamic Logic with Nested Temporalities for Hybrid Systems
- Differential-algebraic Dynamic Logic for Differential-algebraic Programs
- KeYmaera X: An Axiomatic Tactical Theorem Prover for Hybrid Systems
- KeYmaera: A Hybrid Theorem Prover for Hybrid Systems (System Description)
- Robust Satisfaction of Temporal Logic over Real-Valued Signals
- On Temporal Logic and Signal Processing
- Logical Analysis of Hybrid Systems
- Direct Formal Verification of Liveness Properties in Continuous and Hybrid Dynamical Systems
- Checking Temporal Properties of Discrete, Timed and Continuous Behaviors
- Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems
- Automated Technology for Verification and Analysis
This page was built for publication: A program logic to verify signal temporal logic specifications of hybrid systems
