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.
CITATION STYLE
Selvaratnam, D., Cantoni, M., Davoren, J. M., & Shames, I. (2022). MITL Verification Under Timing Uncertainty. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 13465 LNCS, pp. 136–152). Springer Science and Business Media Deutschland GmbH. https://doi.org/10.1007/978-3-031-15839-1_8
Mendeley helps you to discover research relevant for your work.