MITL Verification Under Timing Uncertainty

TL;DR

This paper introduces an MITL verification method that handles timing uncertainty by using over- and under-approximations of signal properties, avoiding high-frequency sampling and providing quantitative measures of conservativeness.

Contribution

It presents a novel MITL verification algorithm that accounts for timing uncertainty through interval approximations, enabling exact verification without dense sampling.

Findings

Verification is exact when over- and under-approximations match.

The method provides a quantitative measure of conservativeness.

Numerical examples demonstrate the effectiveness of the approach.

Abstract

A Metric Interval Temporal Logic (MITL) verification algorithm is presented. It verifies continuous-time signals without relying on high frequency sampling. Instead, it is assumed that collections of over- and under-approximating intervals are available for the times at which the individual atomic propositions hold true for a given signal. These are combined inductively to generate corresponding over- and under-approximations for the specified MITL formula. The gap between the over- and under-approximations reflects timing uncertainty with respect to the signal being verified, thereby providing a quantitative measure of the conservativeness of the algorithm. The verification is exact when the over-approximations for the atomic propositions coincide with the under-approximations. Numerical examples are provided to illustrate.