On the Metric Temporal Logic for Continuous Stochastic Processes
Mitsumasa Ikeda, Yoriyuki Yamagata, Takayuki Kihara
TL;DR
The paper addresses the problem of defining and analyzing probabilities for events in which sample paths of a continuous-time stochastic process satisfy a continuous-time Metric Temporal Logic (MTL) formula $\phi$, with particular attention to measurability. It introduces reaching times $\tau_B(\omega,t)$ and capacity theory to prove that the satisfaction set $\llbracket \phi \rrbracket$ is measurable, enabling well-defined probabilities for all subformulas. A key negative result shows that discretizing time in general does not guarantee convergence to the continuous-time semantics when temporal operators are nested, via a Brownian-motion-based counterexample. Conversely, the paper proves a positive convergence result for the restricted class of flat $\flat$MTL formulas (no until and no nesting) under mild SDE conditions (e.g., Lipschitz $\sigma$, nondegenerate diffusion on compacts, bounded drift), showing $\chi^{(n)}_\phi(\omega,t) \rightarrow \chi_\phi(\omega,t)$ a.s. for all $t$. These results lay a rigorous foundation for probability computations under continuous-time MTL and clarify when discretization yields reliable approximations, informing verification of real-time stochastic systems.
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.