MITL Verification Under Timing Uncertainty

Autor:	Selvaratnam, Daniel, Cantoni, Michael, Davoren, J. M., Shames, Iman
Rok vydání:	2022
Předmět:	Computer Science - Logic in Computer Science Electrical Engineering and Systems Science - Systems and Control
Druh dokumentu:	Working Paper
DOI:	10.1007/978-3-031-15839-1_8
Popis:	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. Comment: To appear in proceedings of FORMATS 2022
Databáze:	arXiv
Externí odkaz:	http://arxiv.org/abs/2204.10493 Zobrazit plný text záznamu View this record from Arxiv