一句话：证明连续时间MTL对随机过程的可测性，并给出离散化概率收敛条件。
本文研究连续时间度量时序逻辑（MTL）在一般连续时间随机过程上的语义可测性问题。由于 until 算子定义为不可数多个命题的逻辑和，经典测度论方法难以证明“随机过程满足 MTL 公式”这一事件可测。作者借助随机分析中关于首达时可测性的定理（来自容量理论）完成可测性证明。随后，论文给出一个例子，说明按时间离散化 MTL 连续语义时概率近似可能失败；并证明若限制 diamond 算子、禁止其嵌套，则离散化语义的概率收敛到连续语义的概率。结果为连续 MTL 的概率语义及离散近似提供了理论基础。
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.
@article{paperbot2754,
title = {On the Metric Temporal Logic for Continuous Stochastic Processes},
author = {Mitsumasa Ikeda and Yoriyuki Yamagata and Takayuki Kihara},
journal = {Logical Methods in Computer Science},
volume = {Volume 20, Issue 2},
year = {2024},
doi = {10.46298/lmcs-20(2:14)2024}
}