Monitoring Bounded LTL Properties Using Interval Analysis
For developers of safety-critical hybrid systems, this provides a rigorous monitoring method for bounded LTL properties, though it is an incremental improvement over existing verification techniques.
The paper proposes an interval-based monitoring algorithm for verifying bounded linear temporal logic (LTL) properties in hybrid systems, enabling decidable verification with inconclusive results when precision is insufficient. Experiments demonstrate its utility for nonlinear and complex hybrid systems.
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.