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.
翻译:本文证明了在一般情况下,连续时间随机过程满足连续时间度量时序逻辑(MTL)公式的事件的可测性。连续时间MTL能够以自然方式定义物理系统的时间约束。已有若干研究涉及随机过程的连续MTL语义的概率问题。然而,证明此类事件的可测性并非易事,尽管这一点至关重要。困难源于“直到算子”的语义,该语义由不可数多个命题的逻辑析取定义。鉴于使用经典测度论方法证明此类事件可测性所面临的困难,我们采用了随机分析中的一个定理。该定理用于证明随机过程首中时间的可测性,是容量理论中的一个深刻结论。此外,我们提供了一个示例,说明在时间上对MTL公式的连续语义进行离散化时,概率逼近会失效。同时,我们证明,当对菱形算子施加限制以避免嵌套时,离散化语义的概率收敛于连续语义的概率。