# Monitoring Bounded LTL Properties Using Interval Analysis

arXiv: https://arxiv.org/abs/1506.01762 · HTML: https://mlsanity.com/paper/1506.01762/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 5 Jun 2015.

## Built on by (most cited first, 1 of 1)

- [Reinforcement Learning Under Probabilistic Spatio-Temporal Constraints with Time Windows](https://mlsanity.com/paper/2307.15910/) (2023)

## Abstract (arXiv)

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.