MITL Verification Under Timing Uncertainty
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.
Cite
@article{arxiv.2204.10493,
title = {MITL Verification Under Timing Uncertainty},
author = {Daniel Selvaratnam and Michael Cantoni and J. M. Davoren and Iman Shames},
journal= {arXiv preprint arXiv:2204.10493},
year = {2022}
}
Comments
To appear in proceedings of FORMATS 2022