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. 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. Numerical examples are provided to illustrate.
翻译:提出了中子间时空逻辑(MITL)核查算法,在不依赖高频取样的情况下核查连续时间信号,而是假定在个别原子主张真实存在时可以收集出超位和超位偏差间隔的收集结果,这些结合方法可产生对规定的MITL公式的相应超位和低位一致。 超位和超位偏差之间的差别反映了所核查信号的时间不确定性,从而提供了算法保守性的数量衡量标准。