Monitoring bounded LTL properties using interval analysis

DOI10.1016/J.ENTCS.2015.10.009MaRDI QIDQ2520682zbMATH OpenOpenAlexWikidataFDO

Authors Daisuke Ishii, Naoki Yonezaki, 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) Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44) Logic in computer science (03B70)

Abstract: Verification of temporal logic properties plays a crucial role in proving the desired behaviors of hybrid systems. In this paper, we propose an interval method for verifying the properties described by a bounded linear temporal logic. We relax the problem to allow outputting an inconclusive result when verification process cannot succeed with a prescribed precision, and present an efficient and rigorous monitoring algorithm that demonstrates that the problem is decidable. This algorithm performs a forward simulation of a hybrid automaton, detects a set of time intervals in which the atomic propositions hold, and validates the property by propagating the time intervals. A continuous state at a certain time computed in each step is enclosed by an interval vector that is proven to contain a unique solution. In the experiments, we show that the proposed method provides a useful tool for formal analysis of nonlinear and complex hybrid systems.

Recommendations

• Direct formal verification of liveness properties in continuous and hybrid dynamical systems
• Hybrid diagrams: a deductive-algorithmic approach to hybrid system verification
• Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems
• GUARANTEED TERMINATION IN THE VERIFICATION OF LTL PROPERTIES OF NON-LINEAR ROBUST DISCRETE TIME HYBRID SYSTEMS
• scientific article; zbMATH DE number 1956650

Cites work

• scientific article; zbMATH DE number 3281219 (Why is no real title available?)
• Bayesian statistical model checking with application to Stateflow/Simulink verification
• Computing reachable sets for uncertain nonlinear hybrid systems using interval constraint-propagation techniques
• Derived eigenvalues of symmetric matrices, with applications to distance geometry
• Falsification of LTL Safety Properties in Hybrid Systems
• Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems
• Hybrid Systems: Computation and Control
• Inner approximated reachability analysis
• Monte-Carlo techniques for falsification of temporal properties of non-linear hybrid systems
• Proving properties of continuous systems: Qualitative simulation and temporal logic
• Robust satisfaction of temporal logic over real-valued signals
• SAT Modulo ODE: A Direct SAT Approach to Hybrid Systems
• Temporal Logic Verification Using Simulation
• The Reach-and-Evolve Algorithm for Reachability Analysis of Nonlinear Dynamical Systems
• The algorithmic analysis of hybrid systems
• The benefits of relaxing punctuality
• \(\delta\)-decidability over the reals

Cited in

(5)

• scientific article; zbMATH DE number 6930545 (Why is no real title available?)
• Direct formal verification of liveness properties in continuous and hybrid dynamical systems
• Monitoring timed properties (revisited)
• Trace analysis using an event-driven interval temporal logic
• From LTL to rLTL monitoring: improved monitorability through robust semantics

Describes a project that uses

Uses Software

• SReach
• VNODE

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

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