Monitoring bounded LTL properties using interval analysis

DOI10.1016/j.entcs.2015.10.009zbMath1351.68163arXiv1506.01762OpenAlexW2964352321WikidataQ113317761 ScholiaQ113317761MaRDI QIDQ2520682

Naoki Yonezaki, Daisuke Ishii, Alexandre Goldsztejn

Publication date: 16 December 2016

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

zbMATH Keywords

hybrid systemsinterval analysislinear temporal logicbounded model checking

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44)

Uses Software

• VNODE
• SReach

Cites Work

• Unnamed Item
• Computing reachable sets for uncertain nonlinear hybrid systems using interval constraint-propagation techniques
• The algorithmic analysis of hybrid systems
• Derived eigenvalues of symmetric matrices, with applications to distance geometry
• Proving properties of continuous systems: Qualitative simulation and temporal logic
• Bayesian statistical model checking with application to Stateflow/Simulink verification
• Monte-carlo techniques for falsification of temporal properties of non-linear hybrid systems
• Delta-Decidability over the Reals
• Inner approximated reachability analysis
• Temporal Logic Verification Using Simulation
• SAT Modulo ODE: A Direct SAT Approach to Hybrid Systems
• Robust Satisfaction of Temporal Logic over Real-Valued Signals
• Falsification of LTL Safety Properties in Hybrid Systems
• The benefits of relaxing punctuality
• The Reach-and-Evolve Algorithm for Reachability Analysis of Nonlinear Dynamical Systems
• Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems
• Hybrid Systems: Computation and Control

This page was built for publication: Monitoring bounded LTL properties using interval analysis