Mitsumasa Ikeda ; Yoriyuki Yamagata ; Takayuki Kihara - On the Metric Temporal Logic for Continuous Stochastic Processes

lmcs:11692 - Logical Methods in Computer Science, June 13, 2024, Volume 20, Issue 2 - https://doi.org/10.46298/lmcs-20(2:14)2024
On the Metric Temporal Logic for Continuous Stochastic ProcessesArticle

Authors: Mitsumasa Ikeda ; Yoriyuki Yamagata ; Takayuki Kihara

    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.


    Volume: Volume 20, Issue 2
    Published on: June 13, 2024
    Accepted on: March 28, 2024
    Submitted on: August 3, 2023
    Keywords: Computer Science - Logic in Computer Science,Mathematics - Logic,Mathematics - Probability

    Consultation statistics

    This page has been seen 344 times.
    This article's PDF has been downloaded 129 times.