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. Since it is difficult to prove the measurability of such an event by a classical measure-theoretic method, we solve it using a theorem in stochastic analysis used to prove the measurability of hitting times for stochastic processes. Specifically, we prove the measurability of hitting times using a profound result of 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.

翻译：本文证明了对于一般连续时间随机过程满足连续时间度量时序逻辑（MTL）公式的事件可测性。连续时间MTL能够自然地定义物理系统的时间约束。现有若干研究处理随机过程连续MTL语义的概率问题。然而，证明此类事件的可测性绝非易事，尽管它至关重要。难点源于"until算子"的语义，该语义由不可数多个命题的逻辑析取定义。由于通过经典测度论方法证明此类事件可测性十分困难，我们利用随机分析中用于证明随机过程首达时间可测性的定理解决了该问题。具体而言，我们通过容量理论的一个深刻结论证明了首达时间的可测性。随后，我们给出一个实例，说明在时间上离散化MTL公式的连续语义时概率逼近的失效情况。此外，我们证明：当对菱形算子施加限制以避免嵌套时，离散化语义的概率收敛到连续语义的概率。