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公式的连续语义进行时间离散化时,概率逼近将失效。此外,我们证明了在限制菱形算子以避免嵌套的条件下,离散化语义的概率将收敛于连续语义的概率。