Monitoring Bounded LTL Properties Using Interval Analysis

TL;DR

This paper introduces an interval analysis-based method for verifying bounded linear temporal logic properties in hybrid systems, allowing for inconclusive results when precision limits are reached, and demonstrating effectiveness through experiments.

Contribution

It presents a novel interval analysis algorithm for monitoring bounded LTL properties in hybrid systems, with a focus on decidability and handling inconclusive cases.

Findings

The method is effective for nonlinear and complex hybrid systems.

It provides rigorous verification with decidability guarantees.

The approach can output inconclusive results when necessary.

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.