On the Metric Temporal Logic for Continuous Stochastic Processes

TL;DR

This paper establishes the measurability of events where continuous-time stochastic processes satisfy Metric Temporal Logic (MTL) formulas, addressing a key challenge in probabilistic verification of physical systems.

Contribution

It proves measurability of MTL satisfaction events for stochastic processes using stochastic analysis, and analyzes probability approximation issues in discretized MTL semantics.

Findings

Measurability of MTL satisfaction events is proven using stochastic analysis.

Discretized semantics probability converges to continuous semantics under certain restrictions.

Illustrates failure of probability approximation without restrictions.

Abstract

In this paper, we prove measurability of event for which a general continuous-time stochastic process satisfies continuous-time Metric Temporal Logic (MTL) formula. Continuous-time MTL can define temporal constrains for physical system in natural way. Then there are several researches that deal with probability of continuous MTL semantics for stochastic processes. However, proving measurability for such events is by no means an obvious task, even though it is essential. The difficulty comes from the semantics of "until operator", which is defined by logical sum of uncountably many propositions. Given the difficulty involved in proving the measurability of such an event using classical measure-theoretic methods, we employ a theorem from stochastic analysis. This theorem is utilized to prove the measurability of hitting times for stochastic processes, and it stands as a profound result within the theory of capacity. Next, we provide an example that illustrates the failure of probability approximation when discretizing the continuous semantics of MTL formulas with respect to time. Additionally, we prove that the probability of the discretized semantics converges to that of the continuous semantics when we impose restrictions on diamond operators to prevent nesting.