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语义的概率问题。然而，证明此类事件的可测性绝非易事，尽管这是基础性的工作。难度源于“直到算子”的语义，该语义由不可数多个命题的逻辑和定义。由于通过经典测度论方法难以证明此类事件的可测性，我们借助随机分析中用于证明随机过程命中时可测性的定理来解决这一问题。具体地，我们利用容量理论的一个深刻结果证明了命中时的可测性。随后，我们通过一个示例说明了在时间上离散化MTL公式连续语义时概率逼近的失效。此外，我们证明了对菱形算子施加限制以避免嵌套时，离散化语义的概率收敛于连续语义的概率。