Monitoring Temporal Properties using Interval Analysis

TL;DR

This paper introduces an interval-based method for verifying temporal logic properties in continuous systems, providing rigorous, efficient monitoring that handles inconclusive cases and is validated on complex nonlinear systems.

Contribution

It presents a novel interval analysis approach for bounded signal temporal logic verification, relaxing the problem to handle inconclusive results and demonstrating effectiveness on nonlinear systems.

Findings

Efficient and rigorous monitoring algorithm for continuous systems.

Capability to detect and validate time intervals where properties hold.

Experimental validation on nonlinear and complex systems.

Abstract

Verification of temporal logic properties plays a crucial role in proving the desired behaviors of continuous systems. In this paper, we propose an interval method that verifies the properties described by a bounded signal temporal logic. We relax the problem so that if the verification process cannot succeed at the prescribed precision, it outputs an inconclusive result. The problem is solved by an efficient and rigorous monitoring algorithm. This algorithm performs a forward simulation of a continuous-time dynamical system, detects a set of time intervals in which the atomic propositions hold, and validates the property by propagating the time intervals. In each step, the continuous state at a certain time is enclosed by an interval vector that is proven to contain a unique solution. We experimentally demonstrate the utility of the proposed method in formal analysis of nonlinear and complex continuous systems.