20214 LABEL:LastPageAug. 03, 2023Jun. 13, 2024 [a] [a] [b]

# On the Metric Temporal Logic for
Continuous Stochastic Processes

Mitsumasa Ikeda0000-0003-1416-7672  National Institute of Advanced Industrial
Science and Technology (AIST), Osaka 563-8577, Japan
<EMAIL_ADDRESS><EMAIL_ADDRESS>,  Yoriyuki
Yamagata0000-0003-2096-677X  and  Takayuki Kihara0000-0002-1611-952X  Nagoya
University, Nagoya 464-8601, Japan<EMAIL_ADDRESS>
###### Abstract.

In this paper, we prove the measurability of an event for which a general
continuous–time stochastic process satisfies the continuous–time Metric
Temporal Logic (MTL) formula. Continuous–time MTL can define temporal
constraints for physical systems naturally. Several previous studies deal with
the probability of continuous MTL semantics for stochastic processes. However,
proving measurability for such events is not an obvious task, even though it
is essential. The difficulty comes from the semantics of “until operator,”
which is defined by the logical sum of uncountably many propositions. Given
the difficulty in proving such an event’s measurability 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.

###### Key words and phrases:

Stochastic systems, Temporal logic, Formal verification, Measure Theory,
Stochastic calculus

##  1\. Introduction

Stochastic processes have emerged as valuable tools for analyzing real-time
dynamics characterized by uncertainties. They consist of a family of random
variables indexed in real-time and find applications in diverse domains such
as molecular behavior, mathematical finance, and turbulence modeling. To
formally analyze the temporal properties of real-time systems, _Metric
Temporal Logic (MTL)_ has been introduced as a logical framework, specifying
constraints that real-time systems must satisfy (see Chapter VI in [Pri67]).
The increasing demand for MTL specifications in industrial applications
[Koy90, CZ11, KF08] has sparked interest in investigating the probability that
a stochastic process satisfies the semantics of MTL–formulas. In contrast to
discrete-time stochastic systems, which are limited to describing events
within a discretized time domain, continuous-time MTL allows for the precise
representation of constraints on events occurring between discrete times.

This paper focuses on MTL specifications on stochastic systems interpreted by
the continuous-time domain. In particular, we are interested in the
probability of an MTL–formula being satisfied by a continuous–time stochastic
system. However, before discussing the probability of event occurrences, it is
crucial to ensure their measurability. Although previous papers [FT15, JP14,
MLD16] considered the probability of events in which an MTL–formula or
MITL–formula, a restriction of MTL–formulas is satisfied, they did not prove
the measurability of such events. The subtle problem arises in the definition
of probability because unions of uncountably many sets define temporal
operators in MTL. At the same time, measurability is guaranteed in the case of
a union of countably many sets in general. The same problem persists even when
we restrict our attention to MITL–formulas because MITL–formulas contain
intervals in which uncountable instances of time are contained.

In this paper, we prove the measurability of events where sample paths of
stochastic processes satisfy the propositions defined by MTL under mild
assumptions. We assume that the stochastic process is measurable as a mapping
from the product space of the time domain and the sample space, a common
assumption in stochastic analysis. Although establishing measurability for
events represented by MTL–formulas with temporal operators is made challenging
by the presence of the union or intersection of uncountably many sets in the
definition, we overcome this difficulty by introducing the concept of reaching
time for sub-formulas of the given MTL–formula. By leveraging the reaching
time, we prove measurability inductively concerning the sub-formulas. In the
proof of measurability of MTL–formulas, we utilize the measurability of the
corresponding reaching times. The measurability of such reaching times is non-
trivial and proven using the theory of capacity (see [Del72]).

While establishing measurability shows that the probability of continuous–time
MTL semantics for stochastic processes is well-defined, the problem of
calculating such probabilities remains a challenge. Although [FT15, MLD16]
proposed an approximation by discretizing the semantics of MTL–formulas with
respect to time, we show that probability based on discretization does not
converge the probability based on continuous semantics in general. We give an
example that involves multi-level nested temporal operators. The example
motivates the need for a more comprehensive and precise discussion of
approximations, which has been generally overlooked in previous studies. As a
part of such an effort, we show that if a formula only has simplified temporal
operators, and these operators never appear in nested positions, the
discretization converges the continuous semantics.

This paper contributes to understanding the probability foundation and
approximation for stochastic processes satisfying continuous-time MTL
semantics. We investigate the measurability of events, provide proofs under
mild assumptions, and explore the possibility of approximation by
discretization with respect to time. Our findings highlight the challenges and
emphasize the importance of refining approximation techniques in future
studies.

This paper is organized as follows. In Section 2, we refer to some related
works and the novelty of our results compared to previous studies. In Section
3, we provide a comprehensive exposition of the fundamental concepts that will
be utilized extensively in this paper. These include the definitions of
measurability, probability space, stochastic process, Brownian motion,
stochastic differential equation, and metric temporal logic. In Section 4, we
prove the measurability of the set of paths of a stochastic process satisfying
the semantics of the MTL–formula in both continuous and discrete sense. In
Section 5, we provide a counterexample that the probability that a stochastic
process satisfies the discrete semantics of an MTL–formula does not converge
to the probability of path satisfying the semantics of the same MTL–formula in
a continuous sense. On the other hand, in Section 6, we prove the convergence
of probability of discrete semantics for general stochastic differential
equations (SDEs) under some restriction on the syntax of propositional
formulas. We set the restriction so that temporal operators do not nest.

In conclusion, we show that the convergence result relies on the depth of
nests of temporal operators in an MTL–formula.

##  2\. Related Works

Temporal reasoning has been extensively studied (for an overview, see [GR21]),
and it has gained increasing attention due to the growing demands in various
industrial applications for real-time systems.

Pnueli [Pnu77] introduced linear temporal logic (LTL) as a means to express
qualitative timing properties of real-time systems using temporal operators.
Koyman [Koy90] extended this logic to include quantitative specifications by
indexing the temporal operators with time intervals, leading to the
development of metric temporal logic (MTL). Unlike other extensions of LTL
with timing constraints, such as timed propositional temporal logic (TPTL)
[AH89], MTL does not allow explicit reference to clocks, making it practical
for implementation. A more detailed survey of temporal logic for real-time
systems can be found in [Kon13].

This paper focuses on MTL for a continuous-time stochastic process with a
continuous state space. Such processes are commonly used as probabilistic
models to describe phenomena with continuous or intermittent effects caused by
environmental noise. In particular, the process represented by the _stochastic
differential equation (SDE)_ is widely used for model statistical dynamics,
asset prices in mathematical finance [Shr05, Shr04], computer network [ARA00]
and future position of aircraft [HPS03], to named a few [KF08, JP14, PAM17].

Considering the wide range of applications, it is natural to consider the
probability that the given stochastic system satisfies properties defined by
MTL–formulas or MITL–formulas. The previous studies [FT15, MLD16] already
considered the probabilities in which stochastic systems satisfy MTL
properties and gave an approximation based on the discretization of time and
state spaces.

However, to talk probabilities consistently, we must show the measurability of
events under consideration. The subtle problem arises in the definition of
probability because unions of uncountably many sets define temporal operators
in MTL. At the same time, measurability is guaranteed for the unions of
countably many sets in general. Further, their approximation by discretization
assumed that the timed behavior of stochastic processes satisfies
Non–Zenoness, which means that the behavior does not change its value
infinitely in finite time. However, stochastic processes, such as solutions of
SDEs, generally do not satisfy Non–Zenoness assumption because of the inherent
“rough” properties of stochastic processes, as they are neither smooth nor
differentiable everywhere (see, for example, Chapter 2 in [KS91]).

In this paper, we prove the measurability of events in which stochastic
systems satisfy MTL–formulas interpreted by the continuous–time domain under
the mild assumption, using the fundamental theory of stochastic analysis,
which is developed to study the approximation of probability measures by
describing the structure of classes of sets [Del72, Kec95]. Our result
guarantees the existence of probability in which stochastic systems satisfy
MTL–formulas.

Further, we give examples in which probabilities defined by discretization do
not converge to probabilities specified in the continuous-time domain, even if
the time interval used for discretization goes to 0. Our examples show that
approximation by discretization, proposed by previous studies, does not
generally work. Our examples involve triple nesting “always” and “possibly”.

On the positive side, we show that if MTL–formulas only have “always” and
“possibly” operators and do not nest, time discretization converges to
probability defined in the continuous time domain. Furia and Rossi [FR10]
considered the relation between semantics based on discrete time and
continuous time. Although they do not consider the stochastic system, they
also find a correspondence between discrete time semantics and continuous
semantics when the formula does not have a nested temporal operator.
Therefore, we use the notation $\flat$MTL for our subsystem of MTL, borrowing
the symbol from their paper.

The model checking and satisfiability problems of MTL and other interval
temporal logics are considered in the previous works [AFH96, DM11, OW05].
Although our work concerns probability holding an MTL–formula, not its
validity, their works share the context with us as they concern formal
verification of real-time systems.

##  3\. Preliminaries

In this section, we introduce several fundamental concepts discussed
throughout this paper. Let us start with the definitions of measurability and
probability space. When defining an event, it is crucial to ensure that it is
measurable to give meaning to its probability. Once the probability space is
defined, we define the product space of two probability spaces. Next, we
define a general stochastic process and its path. Following that, we introduce
the definition of Brownian motion and stochastic differential equation. These
two concepts are fundamental to stochastic analysis and form its core. Lastly,
we introduce the syntax and semantics of MTL–formulas, which are defined for
every path of a stochastic process.

###  3.1. Measurability and Probability

This subsection introduces the basic definitions used in the measure theory
and probability. Readers who are familiar with these theories may skip this
subsection. More details are available in [Rud66].

[$\sigma$–algebra and Measurable space] Let $\Omega$ be a set and
$\mathcal{F}$ be a family of subsets of $\Omega$, i.e., $\mathcal{F}\subset
2^{\Omega}$. $\mathcal{F}$ is called a $\sigma$–algebra if it satisfies the
following three conditions:

  1. (1)

$\Omega\in\mathcal{F}$ and $\emptyset\in\mathcal{F}$.

  2. (2)

If $A\in\mathcal{F}$, then $\Omega\setminus A\in\mathcal{F}$.

  3. (3)

If $A_{n}\in\mathcal{F}$ for $i=1,2,3,\cdots$, then
$\bigcup_{i=1}^{\infty}A_{n}\in\mathcal{F}$ and
$\bigcap_{i=1}^{\infty}A_{n}\in\mathcal{F}$

If $\mathcal{F}$ is $\sigma$–algebra, $(\Omega,\mathcal{F})$ is called _a
measurable space_. If $(\Omega,\mathcal{F})$ is a measurable space and $A\in
F$, we say that $A$ is _$\mathcal{F}$ –measurable_ or merely _measurable_.

[Borel space] Let $E$ be a topological space. A measurable space is called
_Borel space_ on $E$, denoted by $(E,\mathcal{B}(E))$, if $\mathcal{B}(E)$ is
the smallest $\sigma$–algebra which contains every open set. Every set
belonging to $\mathcal{B}(E)$ is called _a Borel set_.

[Measure space and probability space] Let $(\Omega,\mathcal{F})$ be a
measurable space. A function $\mu:\mathcal{F}\rightarrow[0,\infty]$ is called
a _measure_ on $(\Omega,\mathcal{F})$ if $\mu$ satisfies the following two
conditions:

  1. (1)

$\mu(\emptyset)=0$.

  2. (2)

If $A_{i}\in\mathcal{F}$ for $i=1,2,3,\cdots$ and $A_{i}\cap A_{j}=\emptyset$
for $j\neq i$, then

$\displaystyle\mu(\bigcup_{i=1}^{\infty}A_{i})=\sum_{i=1}^{\infty}\mu(A_{i}).$

We call the triplets $(\Omega,\mathcal{F},\mu)$ _a measure space_.

Especially, if $\mu(\Omega)=1$, we refer to a measure $\mu$ on
$(\Omega,\mathcal{F})$ as a _probability measure_ , and call
$(\Omega,\mathcal{F},\mu)$ a _probability space_. We often write a probability
measure as $\mathbb{P}$.

[Lebesgue measure] Let $E=[0,\infty)$ or $\mathbb{R}^{n}$ endowed with the
usual topology and $(E,\mathcal{B}(E))$ be the Borel space on $E$. It is well
known that there exists a unique measure $\mu$ on $E$ such that

$\displaystyle\mu(\prod_{i=1}^{n}\langle
a_{i},b_{i}\rangle)=\prod_{i=1}^{n}(b_{i}-a_{i}),$ (1)

for every rectangle $\prod_{i=1}^{n}\langle a_{i},b_{i}\rangle$ on $E$. We
call such a measure _Lebesgue measure_.

[Complete probability space] A probability space
$(\Omega,\mathcal{F},\mathbb{P})$ is said to be _complete_ if every subset $G$
of a measurable set $F$ such that $\mathbb{P}(F)=0$ is also measurable.

[Almost sure] Let $(\Omega,\mathcal{F},\mathbb{P})$ be a probability space,
and let $P(\omega)$ be a proposition defined on $\omega\in\Omega$. We say that
$P(\omega)$ holds _almost surely_ if there exists a measurable set
$\tilde{\Omega}\in\mathcal{F}$ such that $\mathbb{P}(\tilde{\Omega})=1$ and
$\tilde{\Omega}\subset\\{\omega\in\Omega;P(\omega)\\}$.

In the context of probability theory, the phrase “almost surely” is often
denoted as “a.s.”. Hence, we frequently use the notation $P(\omega),\text{
a.s.}$ to indicate that $P(\omega)$ holds almost surely.

######  Remark 1.

Let $(\Omega,\mathcal{F},\mathbb{P})$ be a probability space and $P(\omega)$
be a proposition defined on $\omega\in\Omega$. Whether $P(\omega)$ holds
almost surely depends on the probability measure $\mathbb{P}$. For example,
let $\Omega=[0,1]$ and $\mathcal{F}:=\mathcal{B}([0,1])$. Let $\mathbb{P}$ be
the Lebesgue measure on $(\Omega,\mathcal{F})$. Then $\mathbb{P}$ is a
probability measure on $(\Omega,\mathcal{F})$. Now define another probability
measure $\tilde{\mathbb{P}}$ as follows:

$\displaystyle\begin{cases}\tilde{\mathbb{P}}(A)=1,&\text{ if }x\in A,\\\
\tilde{\mathbb{P}}(A)=0,&\text{ if }x\notin A,\end{cases}$

where $x\in[0,1]$. Define a proposition $P(\omega)$ for $\omega\in\Omega$ as
follows:

$\displaystyle P(\omega)\Leftrightarrow\omega=x.$

Then $\mathbb{P}(\omega\in\Omega;P(\omega))=0$, while
$\tilde{\mathbb{P}}(\omega\in\Omega;P(\omega))=1$. When we claim that
$P(\omega)$ holds almost surely focusing on the probability measure
$\mathbb{P}$, we express that “ _$P(\omega)$ holds almost surely
$\mathbb{P}$_” or “ _$P(\omega)$ holds a.s. $\mathbb{P}$_”.

######  Remark 2.

Let $P_{1}(\omega)$ and $P_{2}(\omega)$ be two proposition defined on
$\omega\in\Omega$. If $P_{1}(\omega)$ holds almost surely and $P_{2}(\omega)$
holds almost surely, then both $P_{1}(\omega)$ and $P_{2}(\omega)$ hold almost
surely. To see this, let $\Omega_{1}\in\mathcal{F}$ and
$\Omega_{2}\in\mathcal{F}$ and suppose that
$\Omega_{1}\subset\\{\omega\in\Omega;P_{1}(\omega)\\}$,
$\Omega_{2}\subset\\{\omega\in\Omega;P_{2}(\omega)\\}$, and
$\mathbb{P}(\Omega_{1})=\mathbb{P}(\Omega_{2})=1$. Then
$\Omega_{1}\cap\Omega_{2}\subset\\{\omega\in\Omega;P_{1}(\omega)\text{ and
}P_{2}(\omega)\\}$ and

$\displaystyle\mathbb{P}((\Omega_{1}\cap\Omega_{2})^{C})=\mathbb{P}(\Omega_{1}^{C}\cup\Omega_{2}^{C})\leq\mathbb{P}(\Omega_{1}^{C})+\mathbb{P}(\Omega_{2}^{C})-\mathbb{P}(\Omega_{1}^{C}\cap\Omega_{2}^{C})\leq\mathbb{P}(\Omega_{1}^{C})+\mathbb{P}(\Omega_{2}^{C})=0.$

Therefore, $\mathbb{P}(\Omega_{1}\cap\Omega_{2})=1$.

By repeating similar arguments, we can see the following statement: if
$P_{i}(\omega)$ holds almost surely for $i=1,\cdots,n$, then
$P_{1}(\omega)\wedge,\cdots,\wedge P_{n}(\omega)$ holds almost surely.

[Product measurable space] Let $(G,\mathcal{G})$ and $(H,\mathcal{H})$ be two
measurable spaces. The product $\sigma$–algebra of $\mathcal{G}$ and
$\mathcal{H}$, denoted $\mathcal{G}\otimes\mathcal{H}$, is the smallest
$\sigma$–algebra on $G\times H$ which contains all set of the form $A\times
B$, where $A\in\mathcal{G}$ and $B\in\mathcal{H}$. The resulting measurable
space $(G\times H,\mathcal{G}\otimes\mathcal{H})$ is called the product
measurable space of $(G,\mathcal{G})$ and $(H,\mathcal{H})$.

######  Fact 3.

Let $(G,\mathcal{G})$ and $(H,\mathcal{H})$ me two measurable space and
$E\in\mathcal{G}\otimes\mathcal{H}$. Then the following holds:

$\displaystyle\\{z\in H;(x,z)\in E\\}\in\mathcal{H},$ $\displaystyle\\{z\in
G;(z,y)\in E\\}\in\mathcal{G}.$

[Product measure space] Let $(\Omega,\mathcal{F},\mathbb{P})$ be a probability
space. Let $E=[0,\infty)$ or $\mathbb{R}^{n}$ endowed with the usual topology,
and $(E,\mathcal{B}(E),\mu)$ be the measure space with the Lebesgue measure
$\mu$ defined in Definition 3.1. It is well known that there is a unique
measure $\mathbb{P}\otimes\mu$ on $(\Omega\times
E,\mathcal{F}\otimes\mathcal{B}(E))$ such that

$\displaystyle\mathbb{P}\otimes\mu(A\times B)=\mathbb{P}(A)\times\mu(B)$ (2)

for every $A\in\mathcal{F}$ and $B\in\mathcal{B}(E)$. We call such measure
_the product measure_ of $\mathbb{P}$ and $\mu$. The resulting measure space
is denoted as $(\Omega\times
E,\mathcal{F}\otimes\mathcal{B}(E),\mathbb{P}\otimes\mu)$.

[Measurable function] Let $(G,\mathcal{G})$ and $(H,\mathcal{H})$ be two
measurable spaces. A function $X:G\rightarrow H$ is said to be
$\mathcal{G}/\mathcal{H}$–measurable if $X^{-1}(B)\in\mathcal{G}$ for every
$B\in\mathcal{H}$.

[Random variable] Let $(\Omega,\mathcal{F},\mathbb{P})$ be a probability space
and $(E,\mathcal{B}(E))$ be the Borel space on a topological space $E$. An
$E$–valued function $X$ on $(\Omega,\mathcal{F},\mathbb{P})$ is called a
random variable if $X$ is $\mathcal{F}/\mathcal{B}(E)$–measurable. If there is
no ambiguity, an $E$-valued random variable is simply called a random
variable.

[Law of a random variable] Let $(\Omega,\mathcal{F},\mathbb{P})$ be a
probability space, $(E,\mathcal{B}(E))$ be the Borel space on a topological
space $E$, and $X$ be an $E$-valued random variable. It is well-known that
$\sigma(X):=\\{X^{-1}(B);B\in\mathcal{B}(E)\\}$ is a sub $\sigma$–algebra of
$\mathcal{F}$, and thus the mapping $B\mapsto\mathbb{P}(X^{-1}(B))$ is a
probability measure on $(E,\mathcal{B}(E))$. We refer to this mapping as _the
law of $X$_, often denoted by $\mathbb{P}^{X}$.

[Lebesgue integral and expected value] Let
$(\mathbb{R},\mathcal{B}(\mathbb{R}))$ be the Borel space on $\mathbb{R}$.
Suppose that $(G,\mathcal{G},\mu)$ is a measure space and
$f:G\rightarrow\mathbb{R}$ be a
$\mathcal{G}/\mathcal{B}(\mathbb{R})$–measurable function. The _Lebesgue
integral_ is defined as the following four steps:

  1. (1)

Let $B\in\mathcal{G}$ and define $\mbox{1}\mbox{l}_{B}:G\rightarrow\\{0,1\\}$
as

$\displaystyle\mbox{1}\mbox{l}_{B}(x):=\begin{cases}1,&\text{ if }x\in B\\\
0,&\text{ if }x\notin B.\end{cases}$ (3)

We call $f:G\rightarrow[0,\infty)$ _Simple function_ if

$\displaystyle f=\sum_{i=1}^{n}\alpha_{i}\mbox{1}\mbox{l}_{B_{i}},$ (4)

where $B_{i},\ i=1,2,\cdots,n$ are elements in $\mathcal{G}$ and
$\alpha_{1},\alpha_{2},\cdots,\alpha_{n}$ are nonnegative real numbers. Let
$A\in\mathcal{G}$. Define _the Lebesgue integral of the simple function $f$
with respect to $\mu$_ as

$\displaystyle\int_{A}fd\mu:=\sum_{i=1}^{n}\alpha_{i}\mu(B_{i}\cap A).$ (5)

  2. (2)

Let $A\in\mathcal{G}$ and $f:G\rightarrow\mathbb{R}$ be a nonnegative
$\mathcal{G}/\mathcal{B}(\mathbb{R})$–measurable function. _The Lebesgue
integral_ of $f$ with respect to $\mu$ is defined as follows:

$\displaystyle\int_{A}fd\mu:=\sup\left\\{\int_{A}gd\mu\ ;\ g\text{ is simple
function such that }g\leq f\right\\}.$ (6)

  3. (3)

Let $A\in\mathcal{G}$ and $f:G\rightarrow\mathbb{R}$ be a
$\mathcal{G}/\mathcal{B}(\mathbb{R})$–measurable function. Let
$f^{+}:=\max\\{f,0\\}$ and $f^{-}:=-\min\\{f,0\\}$. It is well known that
$f^{+}$ and $f^{-}$ are $\mathcal{G}/\mathcal{B}(\mathbb{R})$–measurable and
then $\int_{A}f^{+}d\mu$ and $\int_{A}f^{-}d\mu$ can be defined. When
$\int_{A}f^{+}d\mu<\infty$ and $\int_{A}f^{-}d\mu<\infty$, we define _the
Lebesgue integral_ with respect to $\mu$ as

$\displaystyle\int_{A}fd\mu:=\int_{A}f^{+}d\mu-\int_{A}f^{-}d\mu.$ (7)

If $A=G$, then we denote $\int_{A}fd\mu$ as $\int fd\mu$.

  4. (4)

Let $(\Omega,\mathcal{F},\mathbb{P})$ be a probability space and $X$ be a
$\mathbb{R}$–valued random variable such that
$\int_{\Omega}X^{+}d\mathbb{P}<\infty$ and
$\int_{\Omega}X^{-}d\mathbb{P}<\infty$. Then $\int_{\Omega}Xd\mathbb{P}$ is
called _the expected value_ of $X$, denoted by $\mathbb{E}[X]$.

######  Remark 4.

In this paper, we use another type of notation for the Lebesgue integral to
accommodate different situations:

$\displaystyle\int_{A}fd\mu=\int_{A}f(x)\mu(dx)$ (8)

Especially, if $\mu$ is a Lebesgue measure, we denote the integral of
$x\mapsto f(x)$ as following:

$\displaystyle\int_{A}f(x)dx$ (9)

[Density of random variable and absolute continuity]

  1. (1)

Let $(\Omega,\mathcal{F},\mathbb{P})$ be a probability space,
$(\mathbb{R}^{n},\mathcal{B}(\mathbb{R}^{n}))$ be a Borel space, and $X$ be an
$\mathbb{R}^{n}$–valued random variable on $(\Omega,\mathcal{F},\mathbb{P})$.
Let $([0,\infty),\mathcal{B}([0,\infty)))$ is a Borel space on $[0,\infty)$
endowed with the usual topology. A
$\mathcal{B}(\mathbb{R}^{n})/\mathcal{B}([0,\infty))$–measurable function $f$
is called _the density_ of $X$ if the following holds:

$\displaystyle\mathbb{P}(X^{-1}(B))=\int_{B}f(x)dx,\hskip 10.0pt\forall
B\in\mathcal{B}(\mathbb{R}^{n}).$

If such a function $f$ exists, we say that $X$ has a density.

  2. (2)

If $X$ has a density, we say that the law of $X$ is _absolutely continuous_
with respect to the Lebesgue measure.

In the following sections, we frequently use the notion of almost sure
convergence of random variables:

[Almost sure convergence] Let $(\Omega,\mathcal{F},\mathbb{P})$ be a
probability space, and let $E$ be a metric space. Let $X$ and
$X_{n};n=1,2,\cdots$ be $E$–valued random variables. We say $X_{n}$ converges
almost surely to $X$ if there exists a measurable set $N\in\mathcal{F}$ such
that $\mathbb{P}(N)=0$ and

$\displaystyle
X_{n}(\omega)\overset{n\rightarrow\infty}{\longrightarrow}X(\omega)$

for every $\omega\notin N$.

###  3.2. Stochastic process

Let $(\Omega,\mathcal{F},\mathbb{P})$ be a probability space and $E$ be a
Polish space. A family of $E$–valued random variables $X:=\\{X_{t}\\}_{t\geq
0}$ indexed by time parameter $t$ is called a _stochastic process_ :

$\displaystyle\begin{array}[]{ccc}\Omega&\stackrel{{\scriptstyle
X_{t}}}{{\longrightarrow}}&E\\\
\rotatebox{90.0}{$\in$}&&\rotatebox{90.0}{$\in$}\\\
\omega&\longmapsto&X_{t}(\omega)\end{array}$ (13)

Following the convention of stochastic analysis, we say $X$ is _measurable_ if
it satisfies the following assumption: The function $(\omega,t)\mapsto
X_{t}(\omega)$ is $\mathcal{F}\otimes\mathcal{B}([0,\infty))$-measurable,
which means that the inverse image $\\{(\omega,t);X_{t}(\omega)\in B\\}$
belongs to $\mathcal{F}\otimes\mathcal{B}([0,\infty))$ whenever $B$ is a Borel
set in $E$.

######  Remark 5.

Under Assumption 3.2, it follows from Fact 3 that $X_{t}$ is
$\mathcal{F}/\mathcal{B}(E)$-measurable for all $t\in[0,\infty)$.

We denote a path $t\mapsto X_{t}(\omega)$ of $\\{X_{t}\\}_{t\geq 0}$ as
$X(\omega)$ for every $\omega\in\Omega$:

$\displaystyle\begin{array}[]{ccc}[0,\infty)&\stackrel{{\scriptstyle
X(\omega)}}{{\longrightarrow}}&E\\\
\rotatebox{90.0}{$\in$}&&\rotatebox{90.0}{$\in$}\\\
t&\longmapsto&X_{t}(\omega)\end{array}$ (17)

######  Remark 6.

Suppose that $(\Omega,\mathcal{F},\mathbb{P})$ is a complete probability
space. If $X_{t}$ is $\mathcal{F}$-measurable for all $t\in[0,\infty)$ and one
of the following holds, $X$ is known to be measurable (see 1.1.14 in [KS91]):

  1. (1)

The path $t\mapsto X_{t}$ is right–continuous almost surely $\mathbb{P}$.

  2. (2)

The path $t\mapsto X_{t}$ is left–continuous almost surely $\mathbb{P}$.

###  3.3. Brownian motion

When studying properties of distributions of general continuous stochastic
processes and topics such as convergence of discretization, including
numerical computations, it is common to first discuss examples related to a
Brownian motion as it is the most representative continuous stochastic
process. Now, we present the definition of the Brownian motion:

Let $(\Omega,\mathcal{F},\mathbb{P})$ be a probability space. A stochastic
process $X:=\\{X_{t}\\}_{t\geq 0}$ with state space $\mathbb{R}$ is called a
standard one-dimensional Brownian motion starting at $x\in\mathbb{R}$ if

  1. (1)

$\mathbb{P}(X_{0}=x)=1$,

  2. (2)

The path $t\mapsto X_{t}$ is continuous almost surely $\mathbb{P}$,

  3. (3)

For any $s,t\geq 0$, $t>s$ implies that $X_{t}-X_{s}\sim\mathcal{N}(0,t-s)$
i.e., $X_{t}-X_{s}$ has normal distribution with mean $0$ and variance $t-s$.

  4. (4)

If $s\leq t\leq u$, then $X_{u}-X_{t}$ is independent of $\sigma(X_{v};v\leq
s)$, where $\sigma(X_{v};v\leq s)$ is the smallest sigma algebra which
contains $\sigma(X_{v})$ for all $v\leq s$.

The existence of a Brownian motion is established in Section 2.2 of [KS91],
relying on the richness of the underlying probability space.

###  3.4. Stochastic differential equation (SDE)

Let us proceed to define one-dimensional stochastic differential equations
rigorously:

Let $(\Omega,\mathcal{F},\mathbb{P})$ be a probability space that supports a
Brownian motion $W$. Let $\sigma$ and $b$ be real–valued measurable functions
on $\mathbb{R}$. A strong solution of the stochastic differential equation
(SDE)

$\displaystyle\begin{cases}dX_{t}=b(X_{t})dt+\sigma(X_{t})dW_{t},\\\
X_{0}=\xi\in\mathbb{R}.\end{cases}$

on $(\Omega,\mathcal{F},\mathbb{P})$ with respect to $W$ and initial condition
$\xi$, is a process $X=\\{X_{t}\\}_{t\geq 0}$ with continuous sample paths and
with the following properties:

  1. (1)

$\\{X_{t}\\}_{t\geq 0}$ is adapted to the filtration induced by Brownian
motion (see 1.1.9 and 5.2.1 in [KS91]),

  2. (2)

$\mathbb{P}[\omega\in\Omega;X_{0}(\omega)=\xi]=1$,

  3. (3)

$\mathbb{P}[\omega\in\Omega;\int_{0}^{t}\\{|b(X_{s}(\omega))|+\sigma^{2}(X_{t}(\omega))\\}ds<\infty]=1$
holds for every $0\leq t<\infty$, and

  4. (4)

the integral version of (29)

$\displaystyle
X_{t}=X_{0}+\int_{0}^{t}b(X_{s})ds+\int_{0}^{t}\sigma(X_{s})dW_{s};\hskip
10.0pt0\leq t<\infty,$

holds almost surely. Here, the term $\int_{0}^{t}\sigma(X_{s})dW_{s}$
represents the Itô’s stochastic integral, defined as the limit of the
following stochastic process (refer to Chapter 3 in [KS91]):

$\displaystyle\sum_{k=1}^{\infty}\sigma(X_{\frac{k}{n}})(W_{\frac{k+1}{n}\wedge
t}-W_{\frac{k}{n}\wedge t}).$ (18)

######  Remark 7.

Brownian motion $\\{W_{t}\\}_{t\geq 0}$ starting at $x\in\mathbb{R}$ itself is
a solution $\\{X_{t}\\}_{t\geq 0}$ of following one–dimensional SDE:

$\displaystyle\begin{cases}X_{t}=\int_{0}^{t}1dW_{s},\\\ X_{0}=x.\end{cases}$

######  Remark 8.

Brownian motions and SDEs are well-known to be continuous stochastic
processes. Therefore, they satisfy Assumption 3.2.

###  3.5. Metric Temporal Logic (MTL) and its semantics

This section introduces the formal definition of MTL (Metric Temporal Logic)
formulas for a given path. We begin by assuming a set of atomic propositions,
denoted as $AP$, typically defined as a finite set. The MTL–formulas are then
defined as follows:

[Syntax of MTL–formulas] We define MTL–formulas for a continuous stochastic
process $\\{X_{t}\\}_{t\geq 0}$ using the following grammar:

  1. (1)

Every atomic proposition $a\in AP$ is an MTL–formula.

  2. (2)

If $\phi$ is an MTL–formula, then $\lnot\phi$ is also an MTL–formula.

  3. (3)

If $\phi_{1}$ and $\phi_{2}$ are MTL-formulas, then the conjunction of
$\phi_{1}$ and $\phi_{2}$, denoted as $\phi_{1}\wedge\phi_{2}$, is also an
MTL–formula.

  4. (4)

If $\phi_{1}$ and $\phi_{2}$ are MTL–formulas, and $I$ represents an interval
on the domain $[0,\infty)$, then the formula $\phi_{1}\mathcal{U}_{I}\phi_{2}$
is an MTL–formula.

The grammar above can be conveniently represented using the _Backus–Naur form_
:

$\displaystyle\phi::=a\mid\phi_{1}\wedge\phi_{2}\mid\lnot\phi\mid\phi_{1}\mathcal{U}_{I}\phi_{2},$

######  Remark 9 (“Until” operator).

In (3) in the definition 3.5, $\mathcal{U}_{I}$ is called an _until operator._
The interval $I$ appearing in the until operator $\mathcal{U}_{I}$ can be
closed, left open, right open, or purely open. This means that $I$ can take
the form $I=[a,b]$, $(a,b]$, $[a,b)$, or $(a,b)$, respectively. Furthermore,
when $I$ is unbounded, it can only be of the form $I=(a,b)$ or $I=[a,b)$,
where $b$ can take the value $\infty$.

We define two types of semantics for the previously presented syntax: one for
the continuous time domain and the other for the discrete–time domain.

[Continuous Semantics of MTL-Formulas] Consider a path $X(\omega)$ of the
stochastic process $\\{X\\}_{t\geq 0}$ with a fixed $\omega\in\Omega$.
Additionally, for each atomic proposition $a\in\mathrm{AP}$, let us assign a
Borel set $B_{a}$ on the domain $E$. The continuous semantics of MTL–formulas
are recursively defined as follows:

$\displaystyle X(\omega),t\models a$ $\displaystyle\iff$ $\displaystyle
X_{t}(\omega)\in B_{a}$ $\displaystyle X(\omega),t\models\lnot\phi$
$\displaystyle\iff$ $\displaystyle\text{not }[X(\omega),t\models\phi]$
$\displaystyle X(\omega),t\models\phi_{1}\wedge\phi_{2}$ $\displaystyle\iff$
$\displaystyle X(\omega),t\models\phi_{1}\text{ and
}X(\omega),t\models\phi_{2}$ $\displaystyle
X(\omega),t\models\phi_{1}\mathcal{U}_{I}\phi_{2}$ $\displaystyle\iff$
$\displaystyle\exists s\in I\text{ s.t.: }X(\omega),t+s\models\phi_{2}\text{
and }$ $\displaystyle\forall s^{\prime}\in[t,t+s),\
X(\omega),s^{\prime}\models\phi_{1}$

[Time set] We introduce the notations $\llbracket\phi\rrbracket$,
$\llbracket\phi\rrbracket(t)$, and $\llbracket\phi\rrbracket_{\omega}$ as
follows:

$\displaystyle\llbracket\phi\rrbracket$
$\displaystyle:=\\{(\omega,t);X(\omega),t\models\phi\\},$
$\displaystyle\llbracket\phi\rrbracket(t)$
$\displaystyle:=\\{\omega;X(\omega),t\models\phi\\},$
$\displaystyle\llbracket\phi\rrbracket_{\omega}$ $\displaystyle:=\\{t\geq
0;X(\omega),t\models\phi\\}.$

In particular, we refer to $\llbracket\phi\rrbracket_{\omega}$ as the “time
set” associated with $\phi$.

[Discrete Semantics of MTL-Formulas] Let us consider the path $X(\omega)$ of
$\\{X_{t}\\}_{t\geq 0}$ and the assignment $B_{a}$ for an atomic proposition
$a\in\mathrm{AP}$, as well as Definition 9. For any $n\in\mathbb{N}$, we
denote $\\{k/n;k\in\mathbb{N}\\}$ as $\mathbb{N}/n$. The discrete semantics of
MTL–formulas for any $t\in\mathbb{N}/n$ is defined recursively as follows:

$\displaystyle X(\omega),t\models_{n}a$ $\displaystyle\iff$ $\displaystyle
X_{t}(\omega)\in B_{a}$ $\displaystyle X(\omega),t\models_{n}\lnot\phi$
$\displaystyle\iff$ $\displaystyle\text{not }[X(\omega),t\models_{n}\phi]$
$\displaystyle X(\omega),t\models_{n}\phi_{1}\wedge\phi_{2}$
$\displaystyle\iff$ $\displaystyle X(\omega),t\models_{n}\phi_{1}\text{ and
}X(\omega),t\models_{n}\phi_{2}$ $\displaystyle
X(\omega),t\models_{n}\phi_{1}\mathcal{U}_{I}\phi_{2}$ $\displaystyle\iff$
$\displaystyle\exists s\in I\cap\mathbb{N}/n\text{ s.t.:
}X(\omega),t+s\models_{n}\phi_{2}\text{ and }$ $\displaystyle\forall
s^{\prime}\in[t,t+s)\cap\mathbb{N}/n,\
X(\omega),s^{\prime}\models_{n}\phi_{1}$

For $t\in\mathbb{N}/n$, we denote by $\llbracket\phi\rrbracket_{n}(t)$ the set
$\\{\omega;X(\omega),t\models_{n}\phi\\}$.

######  Remark 10 (Constants, Disjunction, Diamond operator and Box Operator).

We often use two constants of propositional logic _$\top$ (top) _ and _$\bot$
(bottom)_. Top means undoubted tautology whose truth nobody could ever
question, while bottom means undoubted contradiction. These two constants can
be represented as

$\displaystyle\top=\phi\vee\lnot\phi$ $\displaystyle\bot=\phi\wedge\lnot\phi$

by arbitrary MTL–formula $\phi$. We often use the following notation:

$\displaystyle\phi_{1}\vee\phi_{2}$
$\displaystyle=\lnot((\lnot\phi_{1})\wedge(\lnot\phi_{2})),$
$\displaystyle\Diamond_{I}\phi$ $\displaystyle=\top\mathcal{U}_{I}\phi,$
$\displaystyle\Box_{I}\phi$ $\displaystyle=\lnot(\Diamond_{I}\lnot\phi),$

We refer to $\Diamond_{I}$ and $\Box_{I}$ as the diamond and box operators,
respectively. In the continuous and discrete semantics, the following
equivalences hold:

$\displaystyle X(\omega),t\models\Diamond_{I}\phi\Leftrightarrow$
$\displaystyle(\exists s\in I)[X(\omega),t+s\models\phi],$ $\displaystyle
X(\omega),t\models\Box_{I}\phi\Leftrightarrow$ $\displaystyle(\forall s\in
I)[X(\omega),t+s\models\phi].$ $\displaystyle
X(\omega),t\models_{n}\Diamond_{I}\phi\Leftrightarrow$ $\displaystyle(\exists
s\in I\cap\mathbb{N}/n)[X(\omega),t+s\models_{n}\phi],$ $\displaystyle
X(\omega),t\models_{n}\Box_{I}\phi\Leftrightarrow$ $\displaystyle(\forall s\in
I\cap\mathbb{N}/n)[X(\omega),t+s\models_{n}\phi].$

##  4\. Proof of Measurability

As introduced in Definition 3.1, the probability $\mathbb{P}(F)$ can only be
defined for a measurable set $F$. Therefore, in order to define
$\mathbb{P}(\omega\in\Omega;X(\omega),t\models\phi)$ or
$\mathbb{P}(\omega\in\Omega;X(\omega),t\models_{n}\phi)$, it is necessary to
show the measurability of
$\llbracket\phi\rrbracket(t)=\\{\omega\in\Omega;X(\omega),t\models\phi\\}$ or
$\llbracket\phi\rrbracket_{n}(t)=\\{\omega\in\Omega;X(\omega),t\models_{n}\phi\\}$,
respectively. Since the definition of the discrete semantics of MTL involves
the intersection or union of at most countably many sets, the measurability of
$\llbracket\phi\rrbracket_{n}(t)$ follows directly from Definition 3.1 of the
$\sigma$-algebra. Then
$\mathbb{P}(\omega\in\Omega;X(\omega),t\models_{n}\phi)$ can be defined.
However, the measurability of $\llbracket\phi\rrbracket(t)$ is not
straightforward. Then, it is not apparent whether
$\mathbb{P}(\omega\in\Omega;X(\omega),t\models\phi)$ can be defined.

To illustrate the difficulty, let $X$ be an $E$–valued stochastic process,
$a,b$ be atomic propositions, and $I$ be an interval on $[0,\infty)$. Then
$X(\omega),t\models a$ is equivalent to $X_{t}(\omega)\in B_{a}$ for some
Borel set $B_{a}$, and $X(\omega),t\models b$ is equivalent to
$X_{t}(\omega)\in B_{b}$ for some Borel set $B_{b}$. Since $X_{t}$ is
$\mathcal{F}/\mathcal{B}(E)$–measurable, then $\llbracket
a\rrbracket(t)=\\{\omega\in\Omega;X_{t}(\omega)\in B_{a}\\}$ belongs to
$\mathcal{F}$ and hence $\mathbb{P}(\omega\in\Omega;X(\omega),t\models a)$ can
be defined. $\mathbb{P}(\omega\in\Omega;X(\omega),t\models b)$ can be defined
for the same reason.

However, can we define $\mathbb{P}(\omega\in\Omega;X(\omega),t\models
a\mathcal{U}_{I}b)$? From the definition of the until operator,
$X(\omega),t\models a\mathcal{U}_{I}b$ is equivalent to the following:

$\displaystyle(\exists s\in I)[X_{t+s}(\omega)\in B_{b}\text{ and }(\forall
s^{\prime}\in[0,s))[X_{t+s^{\prime}}\in B_{a}]].$

Therefore,

$\displaystyle\llbracket a\mathcal{U}_{I}b\rrbracket(t)=\bigcup_{s\in
I}\bigcap_{s^{\prime}\in[0,s)}\\{\omega\in\Omega;X_{t+s}(\omega)\in
B_{b}\\}\cap\\{\omega\in\omega;X_{t+s^{\prime}}(\omega)\in B_{a}\\}.$

Although the measurability of $\\{\omega\in\Omega:X_{t+s}(\omega)\in
B_{b}\\}\cap\\{\omega\in\Omega:X_{t+s^{\prime}}(\omega)\in B_{a}\\}$ follows
from the $\mathcal{F}/\mathcal{B}(E)$-measurability of $X_{t+s}$ and
$X_{t+s^{\prime}}$, the representation of $\llbracket
a\mathcal{U}_{I}b\rrbracket(t)$ involves uncountable intersections and unions
of these sets. Since Definition 3.1 guarantees that measurability is preserved
under countable unions or intersections, the semantics of negation ”$\lnot$”
and logical conjunction ”$\wedge$” inherits the measurability. On the other
hand, the measurability of $\llbracket
a\mathcal{U}_{I}b\rrbracket(t)=\\{\omega\in\Omega;X(\omega),t\models
a\mathcal{U}_{I}b\\}$ is not obvious. Thus, we have observed that the
challenge arises when showing the preservation of the measurability under
until operator $\mathcal{U}_{I}$.

Toward this goal, we utilize a profound theorem from the theory of capacity.
We obtain a representation of the until operator $\mathcal{U}_{I}$ using the
inverse image of the _reaching time_ (or _debut_) of a set $B$ on
$\Omega\times[0,\infty]$. Then the inverse image is represented as the
projection of a measurable set on $\Omega\times[0,\infty)$ to $\Omega$. By
employing capacity theory and the representation of the until operator by the
reaching times, we show that the measurability saves under the until operator.

Now let us introduce reaching time: Consider a subset $B$ of
$\Omega\times[0,\infty)$. _The reaching time_ or _debut_ $\tau_{B}(\omega,t)$
of $B$ is defined for each $\omega\in\Omega$ as the first time $s>t$ at which
$(\omega,s)$ reaches $B$, given by:

$\displaystyle\tau_{B}(\omega,t):=\inf\\{s>t;(\omega,s)\in B\\},$

where $\tau_{B}(\omega,t):=\infty$ if $\\{s>t;(\omega,s)\in B\\}=\emptyset$.

######  Lemma 11.

Let $B$ be a subset of $\Omega\times[0,\infty)$. Then, the reaching time
$t\mapsto\tau_{B}(\omega,t)$ is right-continuous for every $\omega\in\Omega$.

######  Proof 4.1.

Assume $\tau_{B}(\omega,t)>t$. We can express $\tau_{B}(\omega,t)$ as
$t+\alpha$ for some $\alpha>0$. According to the definition of
$\tau_{B}(\omega,t)$, for every $s$ in the interval $(t,t+\alpha)$, it holds
that $(\omega,s)\notin B$. Therefore, we have $\tau_{B}(\omega,s)=t+\alpha$
for such $s$, and as a result, $\lim_{s\downarrow
t}\tau_{B}(\omega,s)=t+\alpha=\tau_{B}(\omega,t)$.

Assume $\tau_{B}(\omega,t)=t$. For every $\epsilon>0$, there exists
$\delta\in(0,\epsilon)$ such that $(\omega,t+\delta)\in B$. Therefore,
$\tau_{B}(\omega,s)\leq t+\delta<t+\epsilon$ for every $s\in(t,t+\delta)$,
which implies $\lim_{s\downarrow t}\tau_{B}(\omega,s)=t=\tau_{B}(\omega,t)$.

The following lemma is an abstract version of Proposition 1.1.13 in [KS91].

######  Lemma 12.

Let $(\Omega,\mathcal{F},\mathbb{P})$ be a complete probability space. Suppose
that a $[0,\infty]$–valued stochastic process $\\{Y_{t}\\}_{t\geq 0}$
satisfies the following:

  * •

$Y_{t}$ is $\mathcal{F}/\mathcal{B}([0,\infty])$–measurable for every
$t\in[0,\infty)$, i.e., $Y_{t}^{-1}(B)\in\mathcal{F}$ for every
$B\in\mathcal{B}([0,\infty])$.

  * •

$t\mapsto Y_{t}(\omega)$ is right continuous for every $\omega\in\Omega$.

Then, $\\{(\omega,t);Y_{t}(\omega)\in
B\\}\in\mathcal{F}\otimes\mathcal{B}([0,\infty))$ for every
$B\in\mathcal{B}([0,\infty])$ holds. In other word, $(\omega,t)\mapsto
Y_{t}(\omega)$ is
$\mathcal{F}\otimes\mathcal{B}([0,\infty))/\mathcal{B}([0,\infty])$-measurable.

######  Proof 4.2.

For $t>0$, $n\geq 1$, and $k=0,1,\ldots$, we define
$Y_{t}^{(n)}(\omega)=Y_{(k+1)/2^{n}}(\omega)$ for
$\frac{k}{2^{n}}<t\leq\frac{k+1}{2^{n}}$, and $Y^{(n)}_{0}=Y_{0}(\omega)$. The
mapping $(\omega,t)\mapsto Y^{(n)}_{t}(\omega)$ from $\Omega\times[0,\infty)$
to $[0,\infty]$ is demonstrably
$\mathcal{F}\otimes\mathcal{B}([0,\infty))/\mathcal{B}([0,\infty])$-measurable.
Furthermore, by right–continuity, we have $Y^{(n)}_{t}(\omega)\rightarrow
Y_{t}(\omega)$ if $n\rightarrow\infty$ for any
$(\omega,t)\in[0,\infty)\times\Omega$. Consequently, the limit mapping
$(\omega,t)\mapsto Y_{t}(\omega)$ is also
$\mathcal{F}\otimes\mathcal{B}([0,\infty))/\mathcal{B}([0,\infty])$-measurable.

Now, let us show the measurability of the reaching time when considering it as
a stochastic process. This result is derived from capacity theory, which
guarantees the measurability of the projection (of a well-behaved set).

######  Lemma 13.

If $B$ belongs to $\mathcal{F}\otimes\mathcal{B}([0,\infty))$, the mapping
$(\omega,t)\mapsto\tau_{B}(\omega,t)$ is
$\mathcal{F}\otimes\mathcal{B}([0,\infty))/\mathcal{B}([0,\infty])$-measurable,
i.e., $\\{(\omega,t);\tau_{B}(\omega,t)\in
A\\}\in\mathcal{F}\otimes\mathcal{B}([0,\infty))$ for all
$A\in\mathcal{B}([0,\infty])$.

######  Proof 4.3.

From Lemma 11, the reaching times
$\tau_{B}(t,\omega):=\inf\\{s>t;(\omega,s)\in B\\}$ are right-continuous with
respect to $t\in[0,\infty)$. Then it is enough to show that
$\omega\mapsto\tau_{B}(\omega,t)$ is
$\mathcal{F}/\mathcal{B}([0,\infty])$–measurable because of Lemma 12. From the
definition of $\tau_{B}(\omega,t)$, we can represent
$\\{\omega;\tau_{B}(\omega,t)<u\\}$ by using projection mapping
$\pi:\Omega\times[0,\infty]\rightarrow\Omega$ as

$\displaystyle\\{\omega;\tau_{B}(\omega,t)<u\\}=\pi(B\cap\\{\Omega\times(t,u)\\}),\hskip
10.0pt\forall u\in[0,\infty].$

Since $[0,\infty]$ is a locally compact space with countable basis,
$\mathcal{F}$ is complete, and the set $B\cap\\{\Omega\times(t,u)\\}$ belongs
to $\mathcal{F}\otimes\mathcal{B}([0,\infty))$, we can apply _Theorem I-4.14
in[RY91]_ to show $\pi(B\cap\\{\Omega\times(t,u)\\})\in\mathcal{F}$.
Therefore, $\\{\omega\in\Omega;\tau_{B}(\omega,t)<u\\}\in\mathcal{F}$ for all
$u\geq 0$, which implies the
$\mathcal{F}/\mathcal{B}([0,\infty])$–measurability of the map
$\omega\mapsto\tau_{B}(\omega,t)$.

The subsequent lemma regarding the two types of subsets follows directly from
basic arguments in measure theory.

######  Lemma 14.

Let $B\in\mathcal{F}\otimes\mathcal{B}([0,\infty))$. Let $f$ and $g$ be
functions from $\Omega\times[0,\infty)$ to $[0,\infty]$, which are
$\mathcal{F}\otimes\mathcal{B}([0,\infty))/\mathcal{B}([0,\infty])$-measurable.
Then, the following sets belong to
$\mathcal{F}\otimes\mathcal{B}([0,\infty))$.

$\displaystyle\\{(\omega,t)\in\Omega\times[0,\infty);f(\omega,t)\geq
g(\omega,t)\\},$ (19)
$\displaystyle\\{(\omega,t)\in\Omega\times[0,\infty);(\omega,f(\omega,t))\in
B\\}.$ (20)

######  Proof 4.4.

Since $f$ and $g$ are
$\mathcal{F}\otimes\mathcal{B}([0,\infty))/\mathcal{B}([0,\infty])$–measurable,
the set (19) is $\mathcal{F}\otimes\mathcal{B}([0,\infty))$–measurable.

Because $f$ is a
$\mathcal{F}\otimes\mathcal{B}([0,\infty))/\mathcal{B}([0,\infty])$ measurable
function, $\tilde{f}(\omega,t)=(\omega,f(\omega,t))$ is
$\mathcal{F}\otimes\mathcal{B}([0,\infty))/\mathcal{F}\otimes\mathcal{B}([0,\infty])$–measurable
function. By considering $B$ as a subset of $\Omega\times[0,\infty]$, it
becomes $\mathcal{F}\otimes\mathcal{B}([0,\infty])$–measurable. Consequently,
$\tilde{f}^{-1}(B)$ is $\mathcal{F}\otimes\mathcal{B}([0,\infty))$–measurable.
Because

$\\{(\omega,t)\in\Omega\times[0,\infty);(\omega,f(\omega,t))\in
B\\}=\tilde{f}^{-1}(B)\in\mathcal{F}\otimes\mathcal{B}([0,\infty)),$

The lemma holds.

Now, we can prove the measurability of $\llbracket\phi\rrbracket$ and
$\llbracket\phi\rrbracket(t)$.

######  Lemma 15.

Let $\phi_{1}$ and $\phi_{2}$ be two MTL-formulas and suppose that both
$\llbracket\phi_{1}\rrbracket$ and $\llbracket\phi_{2}\rrbracket$ are in
$\mathcal{F}\otimes\mathcal{B}([0,\infty))$. Then
$\\{(\omega,t);X(\omega),t\models\phi_{1}\mathcal{U}_{I}\phi_{2}\\}$ belongs
to $\mathcal{F}\otimes\mathcal{B}([0,\infty))$.

We prove Lemma 15 using the right continuity of $\tau_{i}(t),\ i=1,2$ and
Lemma 12.

######  Proof 4.5.

To prove this lemma, we put

$\displaystyle\tau_{1}(\omega,t)$
$\displaystyle:=\tau_{\llbracket\phi_{1}\rrbracket^{C}}(\omega,t)=\inf\\{s>t;X(\omega),s\not\models\phi_{1}\\},$
$\displaystyle\tau_{2}(\omega,t)$
$\displaystyle:=\tau_{\llbracket\phi_{2}\rrbracket}(\omega,t)=\inf\\{s>t;X(\omega),s\models\phi_{2}\\}.$

By Lemma 12, $\tau_{1}$ and $\tau_{2}$ are
$\mathcal{F}\otimes\mathcal{B}([0,\infty))/\mathcal{B}([0,\infty])$-measurable.

We only prove the case where $I=[a,b]$. The cases for other forms of $I$ can
be proved in similar ways. For simplicity, suppose that $a>0$. Then
$X(\omega),t\models\phi_{1}\mathcal{U}_{I}\phi_{2}$ holds if and only if
$X(\omega),t\models\phi_{1}$ holds and one of the following possibilities
holds:

  1. (1)

$X(\omega),t+a\models\phi_{2}$ holds and $\tau_{1}(\omega,t)\geq t+a$

  2. (2)

$X(\omega),t+b\models\phi_{2}$ holds and $\tau_{1}(\omega,t)\geq t+b$ holds

  3. (3)

$\tau_{2}(\omega,t+a)<t+b$, $X(\omega),\tau_{2}(\omega,t+a)\models\phi_{2}$
and $\tau_{1}(\omega,t)\geq\tau_{2}(\omega,t+a)$ hold

  4. (4)

$\tau_{2}(\omega,t+a)<t+b$,
$X(\omega),\tau_{2}(\omega,t+a)\not\models\phi_{2}$ and
$\tau_{1}(\omega,t)>\tau_{2}(\omega,t+a)$ hold

By
$\mathcal{F}\otimes\mathcal{B}([0,\infty))/\mathcal{B}([0,\infty])$–measurability
of $\tau_{1}$ and $\tau_{2}$,

$\displaystyle\\{(\omega,t);\tau_{1}(\omega,t)\geq t+a\\},$
$\displaystyle\\{(\omega,t);\tau_{1}(\omega,t)\geq t+b\\},\text{ and}$
$\displaystyle\\{(\omega,t);\tau_{2}(\omega,t+a)<t+b\\}$

are in $\mathcal{F}\otimes\mathcal{B}([0,\infty))$. Thanks to Lemma 14,

$\displaystyle\\{(\omega,t);\tau_{1}(\omega,t)\geq\tau_{2}(\omega,t+a)\\}\text{
and}$ $\displaystyle\\{(\omega,t);\tau_{1}(\omega,t)>\tau_{2}(\omega,t+a)\\}$

are in $\mathcal{F}\otimes\mathcal{B}([0,\infty))$. Since
$\tau_{2}(\omega,t+a)$ is
$\mathcal{F}\otimes\mathcal{B}([0,\infty))/\mathcal{B}([0,\infty])$–measurable
and then

$\displaystyle\\{(\omega,t);X(\omega),\tau_{2}(\omega,t+a)\models\phi_{2}\\}$
$\displaystyle=\\{(\omega,t);(\omega,\tau_{2}(\omega,t+a))\in\llbracket\phi_{2}\rrbracket\\},$
$\displaystyle\\{(\omega,t);X(\omega),\tau_{2}(\omega,t+a)\not\models\phi_{2}\\}$
$\displaystyle=\\{(\omega,t);(\omega,\tau_{2}(\omega,t+a))\notin\llbracket\phi_{2}\rrbracket\\}.$

From Lemma 14, both sets are in $\mathcal{F}\otimes\mathcal{B}([0,\infty))$.
This completes the proof of
$\mathcal{F}\otimes\mathcal{B}([0,\infty))$-measurability of
$X(\omega),t\models\phi_{1}\mathcal{U}_{I}\phi_{2}$.

######  Theorem 16.

For each MTL-formula $\phi$, $\llbracket\phi\rrbracket$ is
$\mathcal{F}\otimes\mathcal{B}([0,\infty))$-measurable and
$\llbracket\phi\rrbracket(t)$ is $\mathcal{F}$-measurable for all $t\geq 0$.

######  Proof 4.6.

We can prove the measurability of $\llbracket\phi\rrbracket$ by induction on
$\phi$.

  * •

Atomic Formula: If $\phi$ is an atomic formula, then
$\llbracket\phi\rrbracket$ belongs to
$\mathcal{F}\otimes\mathcal{B}([0,\infty))$ because the mapping
$(\omega,t)\mapsto X_{t}(\omega)$ is
$\mathcal{F}\otimes\mathcal{B}([0,\infty))/\mathcal{B}(E)$-measurable.

  * •

Negation: If $\llbracket\phi\rrbracket$ belongs to
$\mathcal{F}\otimes\mathcal{B}([0,\infty))$, then
$\llbracket\lnot\phi\rrbracket=\llbracket\phi\rrbracket^{C}$ clearly belongs
to $\mathcal{F}\otimes\mathcal{B}([0,\infty))$.

  * •

Conjunction: Suppose $\phi_{1}$ and $\phi_{2}$ are two MTL–formulas, and
$\llbracket\phi_{i}\rrbracket$ is
$\mathcal{F}\otimes\mathcal{B}([0,\infty))$-measurable for $i=1,2$. Then it is
straightforward to show that
$\llbracket\phi_{1}\wedge\phi_{2}\rrbracket=\llbracket\phi_{1}\rrbracket\cap\llbracket\phi_{2}\rrbracket$
is also $\mathcal{F}\otimes\mathcal{B}([0,\infty))$-measurable.

  * •

Until Operator: From Lemma 15, we can obtain
$\mathcal{F}\otimes\mathcal{B}([0,\infty))$-measurability of
$\llbracket\phi_{1}\mathcal{U}_{I}\phi_{2}\rrbracket$.

Once we have shown that $\llbracket\phi\rrbracket$ belongs to
$\mathcal{F}\otimes\mathcal{B}([0,\infty))$, the fact that
$\llbracket\phi\rrbracket(t)\in\mathcal{F}$ follows from Fact 3.

Since the domain of $\mathbb{P}$ is $\mathcal{F}$, we can define
$\mathbb{P}(\omega;X(\omega),t\models\phi)$ for all $\phi$ and
$t\in[0,\infty)$.

##  5\. Discretization of MTL–formula: Counterexample

Fu and Ufuk [FT15] proposed a methodology for approximating the probability
that the solution of a controlled stochastic differential equation (SDE)
satisfies an MITL–formula. Their approach involves discretizing both the time
and state space of the SDE. They derive probabilities based on this
discretized semantics by utilizing a reachability problem for a timed
automaton generated by the SDE and MITL–formula.

The authors argue that their simulation’s convergence results from the
convergence in distribution of the approximated SDE, whose state space has
been discretized. They claim that the probability obtained from the
discretized approach converges to the probability derived from the
continuous–time semantics of the original SDE.

However, here, we demonstrate that for a one-dimensional Brownian motion,
denoted as X, the probability obtained using the discretized semantics does
not necessarily converge to the probability obtained using continuous
semantics. This failure arises because a reaching time of the Brownian motion
may have positive density.

It is worth noting that Brownian motion can be viewed as the solution of a
stochastic differential equation (SDE) (see Remark 7). Furthermore, every SDE
without control can be regarded as a special case of controlled SDEs.
Consequently, Brownian motion can be an illustrative example of a solution to
a controlled SDE. Hence, our counterexample aligns with the scenario presented
in [FT15]. Consider that $X$ is a one-dimensional Brownian motion starting
from $0$.

The one of the ideas of our construction is that, we can define a MTL–formula
depending on a behavior of $X$ in a single time instance by nested temporal
operators on open intervals. In fact, our example falls under MITL–formulas,
because there is no temporal operators defined on a single instance of time.

Let $p$ be an atomic formula, $B_{p}:=[1,\infty)$ be the set associated with
$p$ and $\tau_{p}(\omega):=\inf\\{t\geq 0;X_{t}\in B_{p}\\}$. In other words,
$X(\omega),t\models p\Leftrightarrow X_{t}(\omega)\geq 1$ and
$\tau_{p}(\omega)=\inf\\{t\geq 0;X(\omega),t\models p\\}$.

Put

$\displaystyle\phi_{1}$
$\displaystyle:=\Box_{(1,2)}(\Diamond_{(1,4)}p\wedge\lnot\Diamond_{(1,3)}p)$
(21) $\displaystyle\phi_{2}$
$\displaystyle:=(\Diamond_{(1,3)}\phi_{1})\wedge(\lnot\Diamond_{(1,2)}\phi_{1})\wedge(\lnot\Diamond_{(2,3)}\phi_{1}),$
(22) $\displaystyle\phi_{3}$ $\displaystyle:=\Diamond_{(1,2)}\phi_{2},$ (23)
$\displaystyle\psi$ $\displaystyle:=(\lnot
p)\wedge(\lnot\Diamond_{(0,8)}p)\wedge\phi_{3}.$ (24)

In one line,

$\displaystyle\psi:=(\lnot
p)\wedge(\lnot\Diamond_{(0,8)}p)\wedge\Diamond_{(1,2)}[($
$\displaystyle\Diamond_{(1,3)}\Box_{(1,2)}(\Diamond_{(1,4)}p\wedge\lnot\Diamond_{(1,3)}p))$
(25) $\displaystyle\wedge$
$\displaystyle(\lnot\Diamond_{(1,2)}\Box_{(1,2)}(\Diamond_{(1,4)}p\wedge\lnot\Diamond_{(1,3)}p))$
(26) $\displaystyle\wedge$
$\displaystyle(\lnot\Diamond_{(2,3)}\Box_{(1,2)}(\Diamond_{(1,4)}p\wedge\lnot\Diamond_{(1,3)}p))].$
(27)

In this setting, the following statements hold. [[KS91, Remark 2.8.3]]
$\tau_{p}(\omega)$ has positive density on $[0,\infty)$.

We will take $\psi$ as a counterexample that
$\mathbb{P}(\omega\in\Omega;X(\omega),0\models_{n}\psi)$ does not converges to
$\mathbb{P}(\omega\in\Omega;X(\omega),0\models\psi)$. We show that
$\mathbb{P}(\omega\in\Omega;X(\omega),0\models_{n}\psi)=0$ for sufficiently
large $n\in\mathbb{N}$, while
$\mathbb{P}(\omega\in\Omega;X(\omega),0\models\psi)>0$.

Before showing that $\psi$ is the counterexample, let us describe the meaning
of the formula $\psi$. Note that the following equivalences hold:

$\displaystyle X(\omega),0\models\psi$
$\displaystyle\Leftrightarrow[X(\omega),0\models(\lnot
p)\wedge(\lnot\Diamond_{(0,8)}p)]\text{ and }[X(\omega),0\models\phi_{3}],$
$\displaystyle X(\omega),0\models_{n}\psi$
$\displaystyle\Leftrightarrow[X(\omega),0\models_{n}(\lnot
p)\wedge(\lnot\Diamond_{(0,8)}p)]\text{ and
}[X(\omega),0\models_{n}\phi_{3}].$

Let
$\tau^{(n)}_{p}(\omega):=\min\\{t\in\mathbb{N}/n;X(\omega),t\models_{n}p\\}$.
Then $X(\omega),0\models(\lnot p)\wedge(\lnot\Diamond_{(0,8)}p)$ and
$X(\omega),0\models_{n}(\lnot p)\wedge(\lnot\Diamond_{(0,8)}p)$ means that
$\tau_{p}\geq 8$ and $\tau^{(n)}_{p}\geq 8$, respectively. By combining these
meanings with the semantics of $X(\omega),0\models\phi_{3}$ and
$X(\omega),0\models_{n}\phi_{3}$ respectively, we show that
$X(\omega),0\models\psi$ is equivalent to $\tau_{p}\in(8,9)$ almost surely,
while $X(\omega),0\models_{n}\psi$ is equivalent to
$X(\omega),0\models_{n}\bot$ almost surely.

Now we estimate the probability
$\mathbb{P}(\omega\in\Omega;X(\omega),0\models\psi)$ of continuous semantics
of $\psi$.

######  Lemma 17.

Suppose that $\tau_{p}(\omega)\geq 6$. Then
$\llbracket\phi_{1}\rrbracket_{\omega}$ has an isolated point
$\tau_{p}(\omega)-5$ with positive probability. Moreover,
$X(\omega),t\not\models\phi_{1}$ for
$t\in[0,\tau_{p}(\omega)-5)\cup(\tau_{p}(\omega)-5,\tau_{p}(\omega)-3)$. In
other words,

$\displaystyle\begin{cases}X(\omega),t\not\models\phi_{1}&\text{ for }0\leq
t<\tau_{p}(\omega)-5,\\\ X(\omega),t\models\phi_{1}&\text{ for
}t=\tau_{p}(\omega)-5,\\\ X(\omega),t\not\models\phi_{1}&\text{ for
}\tau_{p}(\omega)-5<t<\tau_{p}(\omega)-3.\end{cases}$

$t$Truth value of
$X(\omega),t\models\phi_{1}$$0$TRUE$\tau_{p}(\omega)$$\tau_{p}(\omega)-5$$\tau_{p}(\omega)-3$FALSE
Figure 1. The truth value of “$X(\omega),t\models\phi_{1}$”.

######  Proof 5.1.

Note that $\tau_{p}(\omega)<\infty$ almost surely. Suppose
$\tau_{p}(\omega)\geq 6$. Then $X(\omega),t\not\models p$ for
$t<\tau_{p}(\omega)$ and $\inf\\{t\geq 0;X(\omega),t\models
p\\}=\tau_{p}(\omega)$.

Truth value of $X(\omega),t\models p$$0$$t$TRUE$6$$\tau_{p}(\omega)$FALSE

From the definition of $\tau_{p}(\omega)$, if $t\leq\tau_{p}(\omega)-4$, there
is no $s\in(t+1,t+4)$ such that $X(\omega),s\models p$, which implies
$X(\omega),t\not\models\Diamond_{(1,4)}p$. Again from the definition of
$\tau_{p}(\omega)$, if $t\in(\tau_{p}(\omega)-4,\tau_{p}(\omega)-1)$, there
exists some $s\in(t+1,t+4)$ such that $X(\omega),s\models p$. Thus we obtain

$\displaystyle\begin{cases}X(\omega),t\not\models\Diamond_{(1,4)}p&\text{ for
}t\leq\tau_{p}(\omega)-4,\\\ X(\omega),t\models\Diamond_{(1,4)}p&\text{ for
}\tau_{p}(\omega)-4<t<\tau_{p}(\omega)-1.\end{cases}$

Truth value of $X(\omega),t\models
p$$0$$t$TRUE$6$$\tau_{p}(\omega)$FALSE$t$$t+1$$t+4$Truth value of
$X(\omega),t\models\Diamond_{(1,4)}p$$0$TRUE$t$$\tau_{p}(\omega)$$\tau_{p}(\omega)-4$$\tau_{p}(\omega)-1$FALSE

Similarly, we can show that

$\displaystyle\begin{cases}X(\omega),t\models\lnot\Diamond_{(1,3)}p&\text{ for
}0\leq t\leq\tau_{p}(\omega)-3,\\\
X(\omega),t\not\models\lnot\Diamond_{(1,3)}p&\text{ for
}\tau_{p}(\omega)-3<t<\tau_{p}(\omega)-1.\end{cases}$

Truth value of
$X(\omega),t\models\lnot\Diamond_{(1,3)}p$FALSE$0$$t$$\tau_{p}$$\tau_{p}-3$$\tau_{p}-1$TRUE

Consequently,
$X(\omega),t\models\Diamond_{(1,4)}p\wedge(\lnot\Diamond_{(1,3)}p)$ does not
hold for any $t\in[0,\tau_{p}(\omega)-4]$ and
$t\in(\tau_{p}(\omega)-3,\tau_{p}(\omega)-1)$, but it holds for
$(\tau_{p}(\omega)-4,\tau_{p}(\omega)-3]$. Namely,

$\displaystyle\begin{cases}X(\omega),t\not\models\Diamond_{(1,4)}p\wedge(\lnot\Diamond_{(1,3)}p)&\text{
for }0\leq t\leq\tau_{p}(\omega)-4,\\\
X(\omega),t\models\Diamond_{(1,4)}p\wedge(\lnot\Diamond_{(1,3)}p)&\text{ for
}\tau_{p}-4(\omega)<t\leq\tau_{p}(\omega)-3,\\\
X(\omega),t\not\models\Diamond_{(1,4)}p\wedge(\lnot\Diamond_{(1,3)}p)&\text{
for }\tau_{p}(\omega)-3<t<\tau_{p}(\omega)-1.\end{cases}$

Truth value of
$X(\omega),t\models\Diamond_{(1,4)}p\wedge(\lnot\Diamond_{(1,3)}p)$TRUE$t$$0$$\tau_{p}$$\tau_{p}-1$$\tau_{p}-3$$\tau_{p}-4$FALSE

To satisfy $X(\omega),t\models\phi_{1}$, it must holds that
$X(\omega),s\models\Diamond_{(1,4)}p\wedge(\lnot\Diamond_{(1,3)}p)$ for every
$s\in(t+1,t+2)$. Then $X(\omega),t\models\phi_{1}$ does not holds for
$t\in[0,\tau_{p}(\omega)-5)$ and $t\in(\tau_{p}(\omega)-5,\tau_{p}(\omega)-3)$
and holds on $t=\tau_{p}(\omega)-5$. We obtain the required claim since such
an isolated point occurs whenever $\tau_{p}(\omega)\geq 6$.

Truth value of
$X(\omega),t\models\Diamond_{(1,4)}p\wedge(\lnot\Diamond_{(1,3)}p)$TRUE$t$$0$$\tau_{p}$$\tau_{p}-1$$\tau_{p}-3$$\tau_{p}-4$$\tau_{p}-5$FALSE$t$$t+1$$t+2$$t$$t+1$$t+2$$t$$t+1$$t+2$$t$Truth
value of
$X(\omega),t\models\phi_{1}$$0$TRUE$\tau_{p}$$\tau_{p}-5$$\tau_{p}-3$FALSE

######  Lemma 18.

$X(\omega),0\models\psi$ is equivalent to $\tau_{p}(\omega)\in(8,9)$ almost
surely. In particular, $\mathbb{P}(X(\omega),0\models\psi)>0$.

######  Proof 5.2.

First, we note that $X(\omega),0\models(\lnot
p)\wedge(\lnot\Diamond_{(0,8)}p)$ is equivalent to $\tau_{p}(\omega)\geq 8$.
Since $\tau_{p}(\omega)$ has density, $X(\omega),0\models\psi$ implies
$\tau_{p}(\omega)>8$ almost surely.

Suppose that $\tau_{p}(\omega)>8$. Define

$\displaystyle\tau_{1}(\omega):=\inf\\{t;X(\omega),t\models\phi_{1}\\},$
$\displaystyle\tau_{2}(\omega):=\inf\\{t;X(\omega),t\models\phi_{2}\\}.$

Then, from Lemma 17,

$\displaystyle\begin{cases}X(\omega),t\not\models\phi_{1},&\text{ for
}t\in[0,\tau_{p}(\omega)-5),\\\ X(\omega),t\models\phi_{1},&\text{ at
}t=\tau_{p}(\omega)-5,\\\ X(\omega),t\not\models\phi_{1},&\text{ for
}t\in(\tau_{p}(\omega)-5,\tau_{p}(\omega)-3).\end{cases}$ (28)

Hence $\tau_{1}(\omega)=\tau_{p}(\omega)-5$. Furthermore,
$X(\omega),t\models\phi_{2}$ means

$\displaystyle\begin{cases}X(\omega),s\not\models\phi_{1},&\text{ for
}s\in(t+1,t+2),\\\ X(\omega),s\models\phi_{1},&\text{ at }s=t+2,\\\
X(\omega),s\not\models\phi_{1},&\text{ for }s\in(t+2,t+3).\end{cases}$

Then we can conclude from (28) that

$\displaystyle\begin{cases}X(\omega),t\models\lnot\phi_{2},&\text{ for
}t\in[0,\tau_{p}(\omega)-7)\\\ X(\omega),t\models\phi_{2},&\text{ at
}t=\tau_{p}(\omega)-7,\\\ X(\omega),t\models\lnot\phi_{2},&\text{ for
}t\in(\tau_{p}(\omega)-7,\tau_{p}(\omega)-5).\end{cases}$

This means exactly $\tau_{2}(\omega)=\tau_{p}(\omega)-7$.

Suppose that $\tau_{p}(\omega)\geq 9$. Then
$\tau_{2}(\omega)=\tau_{p}(\omega)-7\geq 2$. Since
$X(\omega),0\models\phi_{3}$ is equivalent to $\tau_{2}(\omega)\in(1,2)$,
$X(\omega),0\models\phi_{3}$ does not hold. Then $X(\omega),0\models\psi$
implies $\tau_{p}(\omega)<9$. Consequently, we obtain that
$X(\omega),0\models\psi$ implies $\tau_{p}(\omega)\in(8,9)$ almost surely.

Conversely, as we have seen that $\tau_{p}(\omega)>8$ implies
$\tau_{2}(\omega)=\tau_{p}(\omega)-7$, $\tau_{p}(\omega)\in(8,9)$ implies
$\tau_{2}(\omega)\in(1,2)$. Then $X(\omega),0\models\phi_{3}$, and together
with $\tau_{p}>8$, we can conclude that $X(\omega),0\models\psi$.

######  Lemma 19.

Let $n\geq 2$,
$\tau_{p}^{(n)}(\omega):=\inf\\{t\in\mathbb{N}/n;X(\omega),t\models_{n}p\\}$,
and suppose that $\tau^{(n)}_{p}(\omega)\geq 6$. Then it holds that

$\displaystyle\begin{cases}X(\omega),t\not\models_{n}\phi_{1}&\text{ for
}t=0,1/n,\cdots,\tau_{p}^{(n)}(\omega)-5-1/n,\\\
X(\omega),t\models_{n}\phi_{1}&\text{ for
}t=\tau_{p}^{(n)}(\omega)-5,\tau_{p}^{(n)}(\omega)-5+1/n,\\\
X(\omega),t\not\models_{n}\phi_{1}&\text{ for
}t=\tau_{p}^{(n)}(\omega)-5+2/n,\cdots,\tau_{p}^{(n)}(\omega)-2-2/n.\end{cases}$

######  Proof 5.3.

By the definition of diamond operator,
$X(\omega),t\models_{n}\Diamond_{(1,4)}p$ is equivalent to

$\displaystyle(\exists s\in\\{t+1+1/n,t+1+2/n\cdots
t+4-1/n\\})[X,s\models_{n}p].$

Then we observe from the definition of $\tau_{p}^{(n)}(\omega)$ that

$\displaystyle\begin{cases}X(\omega),t\not\models_{n}\Diamond_{(1,4)}p&\text{
for }t=0,1/n,\cdots,\tau_{p}^{(n)}(\omega)-4\\\
X(\omega),t\models_{n}\Diamond_{(1,4)}p&\text{ for
}t=\tau_{p}^{(n)}(\omega)-4+1/n,\tau_{p}^{(n)}(\omega)-4+2/n,\cdots,\tau_{p}^{(n)}(\omega)-1-1/n.\end{cases}$

Similarly, we have

$\displaystyle\begin{cases}X(\omega),t\models_{n}\Diamond_{(1,3)}p&\text{ for
}t=0,1/n,\cdots,\tau_{p}^{(n)}(\omega)-3\\\
X(\omega),t\not\models_{n}\Diamond_{(1,3)}p&\text{ for
}t=\tau_{p}^{(n)}(\omega)-3+1/n,\tau_{p}^{(n)}(\omega)-3+2/n,\cdots,\tau_{p}^{(n)}(\omega)-1-1/n.\end{cases}$

Then we obtain

$\displaystyle\begin{cases}X(\omega),t\not\models_{n}\Diamond_{(1,4)}p\wedge\lnot\Diamond_{(1,3)}p&\text{
for }t=0,\cdots,\tau_{p}^{(n)}(\omega)-4,\\\
X(\omega),t\models_{n}\Diamond_{(1,4)}p\wedge\lnot\Diamond_{(1,3)}p&\text{ for
}t=\tau_{p}^{(n)}(\omega)-4+1/n,\cdots\tau_{p}^{(n)}(\omega)-3,\\\
X(\omega),t\not\models_{n}\Diamond_{(1,4)}p\wedge\lnot\Diamond_{(1,3)}p&\text{
for
}t=\tau_{p}^{(n)}(\omega)-3+1/n,\cdots,\tau_{p}^{(n)}(\omega)-1-1/n.\end{cases}$

From the definition of Box operator, $X,t\models_{n}\phi_{1}$ is equivalent to

$\displaystyle(\forall
s\in\\{t+1+1/n,\cdots,t+2-1/n\\})[X(\omega),t\models_{n}\Diamond_{(1,4)}p\wedge\lnot\Diamond_{(1,3)}p].$

Then we observe that

$\displaystyle\begin{cases}X(\omega),t\not\models_{n}\phi_{1}&\text{ for
}t=0,1/n,\cdots,\tau_{p}^{(n)}(\omega)-5-1/n,\\\
X(\omega),t\models_{n}\phi_{1}&\text{ for
}t=\tau_{p}^{(n)}(\omega)-5,\tau_{p}^{(n)}(\omega)-5+1/n,\\\
X(\omega),t\not\models_{n}\phi_{1}&\text{ for
}t=\tau_{p}^{(n)}(\omega)-5+2/n,\cdots,\tau_{p}^{(n)}(\omega)-2-2/n.\end{cases}$
$\tau_{p}^{(n)}$ $\tau_{p}^{(n)}$ $\tau_{p}^{(n)}$

######  Lemma 20.

Let $n\geq 2$. Then $X(\omega),0\not\models_{n}\psi$ for every
$\omega\in\Omega$.

######  Proof 5.4.

Define $\tau_{p}^{(n)}(\omega)$ as Lemma 19. Since
$X(\omega),0\models_{n}\psi$ implies $X(\omega),0\models_{n}(\lnot
p)\wedge(\lnot\Diamond_{(0,8)}p)$, $\tau_{p}^{(n)}(\omega)\geq 8$. Then we
obtain from Lemma 19 that

$\displaystyle\begin{cases}X(\omega),t\not\models_{n}\phi_{1}&\text{ for
}t=0,1/n,\cdots,\tau_{p}^{(n)}(\omega)-5-1/n,\\\
X(\omega),t\models_{n}\phi_{1}&\text{ for
}t=\tau_{p}^{(n)}(\omega)-5,\tau_{p}^{(n)}(\omega)-5+1/n,\\\
X(\omega),t\not\models_{n}\phi_{1}&\text{ for
}t=\tau_{p}^{(n)}(\omega)-5+2/n,\cdots,\tau_{p}^{(n)}(\omega)-2-2/n.\end{cases}$

From the definition of the discrete semantics,
$X(\omega),t\models_{n}\phi_{2}$ is equivalent to

$\displaystyle\begin{cases}X(\omega),s\not\models_{n}\phi_{1}&\text{ for
}s=t+1+1/n,\cdots,t+2-1/n,\\\ X(\omega),s\models_{n}\phi_{1}&\text{ for
}s=t+2,\\\ X(\omega),s\not\models_{n}\phi_{1}&\text{ for
}s=t+2+1/n,\cdots,t+3-1/n.\end{cases}$

In other words, for $X(\omega),t\models_{n}\phi_{2}$ to hold,
$X(\omega),s\models_{n}\phi_{1}$ must hold exactly on $s=t+2$, and
$X(\omega),s\models_{n}\phi_{1}$ must not hold for other $s\in\mathbb{N}$ such
that $t+1+1/n\leq s\leq t+3-1/n$. However, $X(\omega),s\models_{n}\phi_{1}$
holds at two adjacent $s$ values, namely $s=\tau_{p}^{(n)}(\omega)-5$ and
$s=\tau_{p}^{(n)}(\omega)-5+1/n$, and does not hold for other $s$ values such
that $0\leq s\leq\tau^{(n)}_{p}(\omega)-2-2/n$. Therefore,
$X(\omega),t\models_{n}\phi_{2}$ does not hold as long as
$t+2\leq\tau^{(n)}_{p}(\omega)-2-2/n$, which implies
$t\leq\tau^{(n)}_{p}(\omega)-4-2/n$. Since $\tau_{p}(\omega)\geq 8$,
$X(\omega),t\models_{n}\phi_{2}$ does not hold as long as $t\leq 4-2/n$ and
hence $X(\omega),0\not\models_{n}\Diamond_{(1,2)}\phi_{2}$.

######  Theorem 21.

Put $\psi$ as Lemma 18. Then
$\mathbb{P}(\omega;X(\omega),0\models_{n}\phi_{3})$ does not converges to
$\mathbb{P}(\omega;X(\omega),0\models\phi_{3})$.

######  Proof 5.5.

From Lemma 18, we have
$\mathbb{P}(\omega;X(\omega),0\models\psi)=\mathbb{P}(\omega;\tau_{p}(\omega)\in(8,9))>0$.
On the other hand, from Lemma 20, we have
$\mathbb{P}(\omega;X(\omega),0\models_{n}\psi)=0$ for every $n$ larger than
$2$. Therefore, $\mathbb{P}(\omega;X(\omega),0\models_{n}\psi)$ never
converges to $\mathbb{P}(\omega;X(\omega),0\models\psi)$.

######  Remark 22.

In the above counterexample, the subscripted intervals for the diamond
operator are restricted to be open. If we restrict the intervals to be left–
or right–open, we can construct similar counterexamples. However, it remains
an open problem whether we can create a counterexample when we restrict all
intervals to be closed.

##  6\. Discretization of MTL–formula: Convergence Result of
MTL–formula without until and nested temporal operators

In the previous section, we presented a counterexample of an MTL–formula,
illustrating a case where its probability in discrete semantics does not
converge to that in continuous semantics. In contrast, in this section, we
establish the convergence of such probabilities by restricting MTL–formulas in
which no until operator and nested diamond and box operators appear. We refer
to these restricted formulas as $\flat$MTL–formulas. While we discussed
MTL–formulas for a Brownian motion in the preceding sections, we will now
present the convergence result for general one-dimensional stochastic
differential equations:

$\displaystyle\begin{cases}dX_{t}=b(X_{t})dt+\sigma(X_{t})dW_{t},\\\
X_{0}=\xi\in\mathbb{R}.\end{cases}$ (29)

We impose the following conditions on the SDE to establish the convergence
result for $\flat$MTL–formulas (29). These conditions are also sufficient to
ensure the solution’s existence, uniqueness, and absolute continuity.(see
Appendix A):

  1. (1)

For every compact set $K\subset\mathbb{R}$, $\inf\sigma(K)>0$.

  2. (2)

$\sigma$ is Lipschitz continuous.

  3. (3)

$b$ is bounded and Borel measurable.

Now let us define $\flat$MTL–formulas rigorously. [Syntax of
$\flat$MTL–formula] Let $AP$ be a finite set of atomic formulas. We define the
syntax of $\flat$MTL by the following induction.

  1. (1)

All atomic formulas are $\flat$MTL–formulas.

  2. (2)

If $\phi$ is an $\flat$MTL–formula, $\lnot\phi$ is an $\flat$MTL–formula.

  3. (3)

If $\phi_{1}$ and $\phi_{2}$ are $\flat$MTL–formulas, then
$\phi_{1}\wedge\phi_{2}$ is an $\flat$MTL–formula.

  4. (4)

If $p$ is a propositional formula and $I$ is a positive interval on
$[0,\infty)$, then $\Diamond_{I}p$ is an $\flat$MTL–formula. We assume that
$I=\langle S,T\rangle$ where $0\leq S<T$ in which $T$ can be infinite $\infty$
and the boundaries of $I$ can be either open or closed.

Here, we define the propositional formula as follows:

  1. (1)

All atomic formulas are propositional formulas.

  2. (2)

If $p$ is a propositional formula, $\lnot p$ is a propositional formula.

  3. (3)

If $p_{1}$ and $p_{2}$ are propositional formulas, then $p_{1}\wedge p_{2}$ is
a propositional formula.

######  Remark 23.

For a MTL–formula $\phi$, $\square_{I}\phi$ is represented by
$\neg\diamond_{I}\neg\phi$ using De Morgan duality. We focus $\square$ and
$\diamond$ operators and does not treat the until operator. The condition of
convergence for the until operator is a future work.

The semantics of $\flat$MTL are given in the same way as MTL–formulas.
[Semantics of $\flat$MTL–formulas] Let $B_{i},\ i=1,\cdots,k$ be Borel sets on
$\mathbb{R}$ and $AP=\\{a_{i};i=1,\cdots,k\\}$ be the set of $k$ atomic
formulas. The semantics of $\flat$MTL–formulas are defined inductively as
follows.

  1. (1)

$X(\omega),t\models a_{i}\Leftrightarrow X_{t}(\omega)\in B_{i}$ for
$i=1,\cdots,k$.

  2. (2)

$X(\omega),t\models\phi_{1}\wedge\phi_{2}$ is equivalent to
$X(\omega),t\models\phi_{1}\text{ and }X(\omega),t\models\phi_{2}$.

  3. (3)

$X(\omega),t\models\Diamond_{I}p$ is equivalent to $(\exists s\in
I)[X(\omega),t+s\models p]$.

We will show the convergence result for $\flat$MTL in Section 6.2. We show the
convergence of the probability by showing the convergence of the indicator
function of $\flat$MTL–formulas. Let us define the indicator functions for
MTL–formulas as follows: Let $\phi$ be an $\flat$MTL–formula and define random
indicator functions $\chi_{\phi}(\omega,t)$ and $\chi^{(n)}_{\phi}(t)$ as

$\displaystyle\chi_{\phi}(\omega,t)$ $\displaystyle:=\begin{cases}1&\text{ if
}X(\omega),t\models\phi\\\ 0&\text{ if
}X(\omega),t\not\models\phi,\end{cases}$
$\displaystyle\chi^{(n)}_{\phi}(\omega,t)$
$\displaystyle:=\begin{cases}1&\text{ if
}X(\omega),\Lambda_{n}(t)\models_{n}\phi\\\ 0&\text{ if
}X(\omega),\Lambda_{n}(t)\not\models_{n}\phi,\end{cases}$

where $\Lambda_{n}(t):=\frac{\lfloor nt\rfloor}{n}$.

The convergence of the indicator function for a formula implies the
convergence of the probability of the formula. More precisely, our proof of
the convergence is based on the following lemma:

######  Lemma 24.

Suppose that $\chi^{(n)}_{\phi}(\omega,t)\rightarrow\chi_{\phi}(\omega,t)$
almost surely. Then
$\mathbb{P}(\omega;X(\omega),\Lambda_{n}(t)\models_{n}\phi)\rightarrow\mathbb{P}(\omega;X(\omega),t\models\phi)$
as $n\rightarrow\infty$.

######  Proof 6.1.

From the definition of $\chi_{\phi}(\omega,t)$ and
$\chi_{\phi}^{(n)}(\omega,t)$, $\chi_{\phi}(\omega,t)=1$ and
$\chi^{(n)}_{\phi}(\omega,t)=1$ is equivalent to $X(\omega),t\models\phi$ and
$X(\omega),\Lambda_{n}(t)\models_{n}\phi$, respectively. Then
$\mathbb{P}(\omega\in\Omega;X(\omega),t\models\phi)=\mathbb{E}[\chi_{\phi}(\omega,t)]$
and
$\mathbb{P}(\omega\in\Omega;X(\omega),\Lambda_{n}(t)\models_{n}\phi)=\mathbb{E}[\chi_{\phi}^{(n)}(\omega,t)]$.
Since $\chi_{\phi}(\omega,t)\leq 1$, $\chi_{\phi}^{(n)}(\omega,t)\leq 1$, and
$\mathbb{E}[1]=1$, we can apply _Lebesgue’s dominated convergence theorem_
(see Theorem 1.34 in [Rud66]) to observe
$\mathbb{E}[\chi_{\phi}^{(n)}(\omega,t)]\rightarrow\mathbb{E}[\chi_{\phi}(\omega,t)]$.

###  6.1. The case of $\Diamond_{\langle S,T\rangle}p$ with $p$ corresponding
to a union of intervals

Before proving the convergence of general $\flat$MTL–formulas, we first show
the convergence for a particular type of $\flat$MTL–formulas. In the
subsequent subsection, we will present the proof for the convergence of
$\flat$MTL–formulas in the general case. In this subsection, we consider
$\flat$MTL–formulas of the form $\Diamond_{\langle S,T\rangle}p$, where $p$ is
a propositional formula. Here, $\langle S,T\rangle$ denotes a positive
interval on $[0,\infty)$, specifically, $\langle S,T\rangle$ represents an
interval with endpoints $S$ and $T$ such that $0\leq S<T$. Note that the
interval $\langle S,T\rangle$ can be open, left open, right open, or closed.
In the proof of convergence in this case, we utilize deep insights from
stochastic calculus, namely, the notion of _local maxima and local minima_ of
SDE (see Definition 6.1), and _the dense property of the zero set_ of SDE (see
Lemma 27).

To prove the convergence in the particular case of $\Diamond_{\langle
S,T\rangle}p$, we will introduce certain conditions on the propositional
formula $p$.

Let $B_{1},\cdots,B_{n}$ be a finite family of Borel sets on $\mathbb{R}$. A
pair $B_{i},B_{j}$ is said to be _separated_ when
$\overline{B_{i}}\cap\overline{B_{j}}=\emptyset$. We say the set
$\\{B_{1},\cdots,B_{n}\\}$ is _pairwise separated_ when all pairs of different
elements are separated.

Now we prove the following theorem:

######  Theorem 25.

Let $X$ be the strong solution of (29) satisfying Assumption 6. Let $p$ be an
MTL–formula such that $X(\omega),t\models p$ is equivalent to $X_{t}\in
B_{p}$, where

$\displaystyle B_{p}:=\bigcup_{i=1}^{k}\langle x_{i},y_{i}\rangle$ (30)

is a union of pairwise separated positive intervals $\\{\langle
x_{i},y_{i}\rangle;i=1,\cdots,k\\}$ on $\mathbb{R}$. Here $B_{p}$ possibly
equals the empty set or $\mathbb{R}$. Define $X(\omega),t\models_{n}p$
similarly. Define $\phi:=\Diamond_{\langle S,T\rangle}p$, and
$\psi:=\Box_{\langle S,T\rangle}p$ where $\langle S,T\rangle$ is a positive
interval on $[0,\infty)$. Then the following statements hold:

$\displaystyle\chi_{\phi}^{(n)}(\omega)$
$\displaystyle\overset{n\rightarrow\infty}{\longrightarrow}\chi_{\phi}(\omega),\hskip
10.0pt\text{a.s. },$ $\displaystyle\chi_{\psi}^{(n)}(\omega)$
$\displaystyle\overset{n\rightarrow\infty}{\longrightarrow}\chi_{\psi}(\omega),\hskip
10.0pt\text{a.s. }$

In particular,

$\displaystyle\mathbb{P}(\omega;X(\omega),\Lambda_{n}(t)\models_{n}\phi)\overset{n\rightarrow\infty}{\rightarrow}\mathbb{P}(\omega;X(\omega),t\models\phi),$
$\displaystyle\mathbb{P}(\omega;X(\omega),\Lambda_{n}(t)\models_{n}\psi)\overset{n\rightarrow\infty}{\rightarrow}\mathbb{P}(\omega;X(\omega),t\models\psi).$

The key to proving the convergence of MTL–formulas with the diamond operator
lies in the following inclusions:

$\displaystyle\llbracket\phi\rrbracket_{\omega}$
$\displaystyle\subset\overline{\mathrm{int}\llbracket\phi\rrbracket_{\omega}}\
\text{almost surely},$ (31)
$\displaystyle\llbracket\lnot\phi\rrbracket_{\omega}$
$\displaystyle\subset\overline{\mathrm{int}\llbracket\lnot\phi\rrbracket_{\omega}}\
\text{almost surely},$ (32)

where the time set $\llbracket\phi\rrbracket_{\omega}$ of MTL–formula $\phi$
is defined in Definition 9.

To show Theorem 25, we will first prove a simplified version of the theorem in
which the propositional formula corresponds to an interval. First, let us show
(31) and (32) in this case:

######  Lemma 26.

Let $X=\\{X_{t}\\}_{t\geq 0}$ be the strong solution of the SDE (29)
satisfying Assumption 6. Let $p$ be a propositional formula defined as
$X(\omega),t\models p\Leftrightarrow X_{t}(\omega)\in\langle
y_{1},y_{2}\rangle$, where $\langle y_{1},y_{2}\rangle$ is a positive interval
on $\mathbb{R}$. Then $p$ satisfies (31) and (32) almost surely. Namely,

$\displaystyle\llbracket p\rrbracket_{\omega}$
$\displaystyle\subset\overline{\mathrm{int}\llbracket
p\rrbracket_{\omega}},\hskip 10.0pt\text{a.s. },$
$\displaystyle\llbracket\lnot p\rrbracket_{\omega}$
$\displaystyle\subset\overline{\mathrm{int}\llbracket\lnot
p\rrbracket_{\omega}},\hskip 10.0pt\text{a.s. }$

To prove this lemma, we have to introduce local minima and local maxima of
$X$:

  1. (1)

Let $f:[0,\infty)\rightarrow\mathbb{R}$ be a given function. A number $t\geq
0$ is called a point of local maximum, if there exists a number $\delta>0$
with $f(s)\leq f(t)$ valid for every $s\in[(t-\delta)^{+},t+\delta]$; and a
point of strict local maximum, if there exists a number $\delta>0$ with
$f(s)<f(t)$ valid for every $s\in[(t-\delta)^{+},t+\delta]\setminus\\{t\\}$.

  2. (2)

Let $f:[0,\infty)\rightarrow\mathbb{R}$ be a given function. A number $t\geq
0$ is called a point of local minimum, if there exists a number $\delta>0$
with $f(s)\geq f(t)$ valid for every $s\in[(t-\delta)^{+},t+\delta]$; and a
point of strict local minimum, if there exists a number $\delta>0$ with
$f(s)>f(t)$ valid for every $s\in[(t-\delta)^{+},t+\delta]\setminus\\{t\\}$.

To show Lemma 26, we use some pathological property of the SDE: Under
Assumption 6, the SDE has the quite zig–zag sample path. Then, once it reaches
a region associated with an atomic proposition, it immediately hits the region
with high frequency.

######  Lemma 27.

Let $X=\\{X_{t}\\}_{t\geq 0}$ be the strong solution of the SDE (29)
satisfying Assumption 6. Then, the following statements hold (see A for the
proof):

  1. (1)

Let $a\in\mathbb{R}$ and put

$\displaystyle\mathcal{L}^{a}_{\omega}:=\\{t\geq 0;X_{t}(\omega)=a\\},\hskip
10.0pt\ \omega\in\Omega.$ (33)

Then $\mathcal{L}^{a}_{\omega}$ is dense–in–itself almost surely.

  2. (2)

For almost every $\omega\in\Omega$, the set of points of local maximum and
local minimum for the path $t\mapsto X(\omega)$ is dense in $[0,\infty)$, and
all local maxima and local minima are strict.

######  Lemma 28.

Let $X=\\{X_{t}\\}_{t\geq 0}$ be the strong solution of the SDE (29)
satisfying Assumption 6. Let us define an atomic formula $a$ as
$X(\omega),t\models a\Leftrightarrow X_{t}(\omega)\in\langle y,\infty)$, where
$\langle y,\infty)$ is half-line with open or closed endpoint
$y\in\mathbb{R}$. Then $a$ satisfies (31) and (32) almost surely. Namely,

$\displaystyle\llbracket a\rrbracket_{\omega}$
$\displaystyle\subset\overline{\mathrm{int}\llbracket
a\rrbracket_{\omega}},\hskip 10.0pt\text{a.s. },$
$\displaystyle\llbracket\lnot a\rrbracket_{\omega}$
$\displaystyle\subset\overline{\mathrm{int}\llbracket\lnot
a\rrbracket_{\omega}},\hskip 10.0pt\text{a.s. }$

######  Proof 6.2.

Put $\tilde{\Omega}$ be the set of $\omega\in\Omega$ with the following
properties:

  1. (1)

The map $t\mapsto X_{t}(\omega)$ is continuous,

  2. (2)

$\mathcal{L}^{y}_{\omega}:=\\{t\geq 0;X_{t}(\omega)=y\\}$ is dense–in–itself,

  3. (3)

the set of local maximum and local minimum of $t\mapsto X_{t}(\omega)$ is
dense in $[0,\infty)$, and

  4. (4)

all the local minima and the local maxima are strict

Then there exists some $\hat{\Omega}\in\mathcal{F}$ such that
$\hat{\Omega}\subset\tilde{\Omega}$ and $\mathbb{P}(\hat{\Omega})=1$ because
of Definition 3.4, Lemma 27. Indeed, let
$\Omega_{1},\Omega_{1},\Omega_{3},\Omega_{4}\in\mathcal{F}$ be the sets of
$\omega$ such that (i)–(iv) holds respectively and
$\mathbb{P}(\Omega_{1})=\mathbb{P}(\Omega_{2})=\mathbb{P}(\Omega_{3})=\mathbb{P}(\Omega_{4})=1$,
then $\mathbb{P}(\bigcap_{i=1}^{4}\Omega_{i})=1$ follows from Remark 2. From
now on, let us prove that the formula $a$ satisfies (31) and (32) for all
$\omega\in\hat{\Omega}$.

Let $\langle y,\infty)$ be the left-closed interval $[y,\infty)$. The
statement $t\in\llbracket\lnot a\rrbracket_{\omega}$ is equivalent to
$X_{t}(\omega)<y$. Since $t\mapsto X_{t}(\omega)$ is continuous, the set

$\displaystyle\llbracket\lnot a\rrbracket_{\omega}=\\{t\geq
0;X_{t}(\omega)<y\\}$

is an open set, and therefore inclusion (32) holds clearly. On the other hand,
due to the continuity of $t\mapsto X_{t}(\omega)$, if $X_{t}(\omega)>y$, then
it implies that $t\in\text{ int }\llbracket a\rrbracket_{\omega}$. Hence, it
remains to show that $X_{t}(\omega)=y$ implies
$t\in\overline{\mathrm{int}\llbracket a\rrbracket_{\omega}}$. Suppose
$X_{t}(\omega)=y$ and $t\notin\overline{\text{int}{\llbracket
a\rrbracket_{\omega}}}$. Then, there exists $\varepsilon>0$ such that
$(t-\varepsilon,t+\varepsilon)\cap\text{int}\llbracket
a\rrbracket_{\omega}=\emptyset$. Since $(\exists
s\in(t-\varepsilon,t+\varepsilon))[X_{s}(\omega)>y]$ implies
$(t-\varepsilon,t+\varepsilon)\cap\text{int}\llbracket
a\rrbracket_{\omega}\neq\emptyset$, it follows that $(\forall
s\in(t-\varepsilon,t+\varepsilon))[X_{s}(\omega)\leq y]$. By applying (iii),
we can conclude that $t$ is a strict local maximum, i.e., $(\forall
s\in(t-\varepsilon,t+\varepsilon)\setminus\\{t\\})[X_{s}(\omega)<y]$, and
thus, $t$ is an isolated point of $\\{t\geq 0;X_{t}(\omega)=y\\}$. However,
this contradicts (ii). Therefore, we obtain the inclusion (31).

On the other hand, consider $\langle y,\infty)$ as the left-open interval
$(y,\infty)$. Now, $t\in\llbracket a\rrbracket_{\omega}$ is equivalent to
$X_{t}(\omega)>y$. Since $t\mapsto X_{t}(\omega)$ is continuous, the set

$\displaystyle\llbracket a\rrbracket_{\omega}=\\{t\geq 0;X_{t}(\omega)>y\\}$

is an open set, and thus inclusion (31) holds clearly. Moreover, due to the
continuity of $t\mapsto X_{t}(\omega)$, if $X_{t}(\omega)<y$, then it implies
$t\in\text{ int }\llbracket\lnot a\rrbracket_{\omega}$. Therefore, we need to
show the inclusion (32) when $t\in\llbracket\lnot a\rrbracket_{\omega}$ and
$X_{t}(\omega)=y$. Suppose $t\notin\overline{\text{int}{\llbracket\lnot
a\rrbracket_{\omega}}}$, which implies the existence of $\varepsilon>0$ such
that $(t-\varepsilon,t+\varepsilon)\cap\text{int}\llbracket\lnot
a\rrbracket_{\omega}=\emptyset$. If $(\exists
s\in(t-\varepsilon,t+\varepsilon))[X_{s}(\omega)<y]$, then it implies
$(t-\varepsilon,t+\varepsilon)\cap\text{int}\llbracket\lnot
a\rrbracket_{\omega}\neq\emptyset$. Consequently, it holds that $(\forall
s\in(t-\varepsilon,t+\varepsilon))[X_{s}(\omega)\geq y]$. By applying 27–(ii),
we can deduce that $t$ is a strict local minimum, i.e., $(\forall
s\in(t-\varepsilon,t+\varepsilon)\setminus\\{t\\})[X_{s}(\omega)>y]$, which
means $t$ is an isolated point of $\llbracket\lnot a\rrbracket_{\omega}$.
However, this contradicts (ii). Thus, we establish (32).

######  Proof 6.3 (Proof of Lemma 26).

Let us define atomic formulas $a,b$ as

$\displaystyle X(\omega),t\models a$ $\displaystyle\Leftrightarrow
X_{t}(\omega)\in\langle y_{1},\infty),$ (34) $\displaystyle X(\omega),t\models
b$ $\displaystyle\Leftrightarrow X_{t}(\omega)\in\langle y_{2},\infty),$ (35)

where left endpoints $y_{1},y_{2}$ can be open or closed and satisfy
$y_{1}<y_{2}$. Then we can define $X(\omega),t\models p$ is equivalent to
$X(\omega),t\models a\wedge\lnot b$ and hence it is enough to show that
$a\wedge\lnot b$ satisfies (31) and (32) almost surely. To see this, let
$\tilde{\Omega}$ be the set of $\omega\in\Omega$ with the following properties

  1. (i)

The map $t\mapsto X_{t}(\omega)$ is continuous,

  2. (ii)

the formula $a$ satisfies (31) and (32), and

  3. (iii)

the formula $b$ satisfies (31) and (32).

Then Definition 3.4 and Lemma 28 imply that there exists some
$\hat{\Omega}\in\mathcal{F}$ such that $\mathbb{P}(\hat{\Omega})=1$ and every
$\omega\in\hat{\Omega}$ satisfies (i)–(iii). Lemma 28. Now let us show (31)
and (32) for every $\omega\in\hat{\Omega}$.

(31):

Given that

$\displaystyle\llbracket a\wedge\lnot
b\rrbracket_{\omega}\subset(\mathrm{int}\llbracket
a\rrbracket_{\omega}\cap\mathrm{int}\llbracket\lnot
b\rrbracket_{\omega})\cup\partial\llbracket
a\rrbracket_{\omega}\cup\partial\llbracket\lnot b\rrbracket_{\omega},$

and

$\displaystyle\text{int}\llbracket
a\rrbracket_{\omega}\cap\mathrm{int}\llbracket\lnot
b\rrbracket_{\omega}=\text{int}\llbracket a\wedge\lnot
b\rrbracket_{\omega}\subset\overline{\mathrm{int}\llbracket a\wedge\lnot
b\rrbracket_{\omega}},$

then it is enough to show

$\displaystyle\llbracket a\wedge\lnot
b\rrbracket_{\omega}\cap\partial\llbracket
a\rrbracket_{\omega}\subset\overline{\mathrm{int}\llbracket a\wedge\lnot
b\rrbracket_{\omega}}$ $\displaystyle\llbracket a\wedge\lnot
b\rrbracket_{\omega}\cap\partial\llbracket\lnot
b\rrbracket_{\omega}\subset\overline{\mathrm{int}\llbracket a\wedge\lnot
b\rrbracket_{\omega}}.$

Suppose that $t\in\llbracket a\wedge\lnot
b\rrbracket_{\omega}\cap\partial{\llbracket a\rrbracket_{\omega}}$. If $O$ is
a neighborhood of $t$, $O\cap\mathrm{int}\llbracket
a\rrbracket_{\omega}\neq\emptyset$ because $O\cap\llbracket
a\rrbracket_{\omega}\neq\emptyset$ and (ii) hold. Since the path $t\mapsto
X(\omega)$ is continuous, $t\in\partial\llbracket a\rrbracket_{\omega}$
implies $X_{t}(\omega)=y_{1}<y_{2}$ and hence $t\in\mathrm{int}\llbracket\lnot
b\rrbracket_{\omega}$. Let $\varepsilon>0$. Since
$(t-\varepsilon,t+\varepsilon)\cap\mathrm{int}\llbracket\lnot
b\rrbracket_{\omega}$ is a neighborhood of $t$,

$\displaystyle(t-\varepsilon,t+\varepsilon)\cap\mathrm{int}\llbracket
a\rrbracket_{\omega}\cap\mathrm{int}\llbracket\lnot
b\rrbracket_{\omega}=(t-\varepsilon,t+\varepsilon)\cap\mathrm{int}\llbracket
a\wedge\lnot b\rrbracket_{\omega}\neq\emptyset,\hskip 10.0pt\text{a.s. },$

and hence $t\in\overline{\mathrm{int}\llbracket a\wedge\lnot
b\rrbracket_{\omega}}$.

The same argument can be applied when $t\in\llbracket a\wedge\lnot
b\rrbracket_{\omega}\cap\partial\llbracket\lnot b\rrbracket_{\omega}$. Thus,
we have shown (31).

(32):

Suppose that $t\in\llbracket\lnot a\vee b\rrbracket_{\omega}$ and let $O$ be a
neighborhood of $t$. Since $t\in\llbracket\lnot a\rrbracket_{\omega}$ or
$t\in\llbracket b\rrbracket_{\omega}$, (ii) and (iii) imply that
$O\cap\mathrm{int}\llbracket\lnot a\rrbracket_{\omega}\neq\emptyset$ or
$O\cap\mathrm{int}\llbracket b\rrbracket_{\omega}\neq\emptyset$ holds. Since
$\mathrm{int}\llbracket\lnot a\rrbracket_{\omega}\cup\mathrm{int}\llbracket
b\rrbracket_{\omega}\subset\mathrm{int}(\llbracket\lnot
a\rrbracket_{\omega}\cup\llbracket b\rrbracket_{\omega})$, it holds that
$O\cap\mathrm{int}\llbracket\lnot a\vee
b\rrbracket_{\omega}=O\cap\mathrm{int}(\llbracket\lnot
a\rrbracket_{\omega}\cup\llbracket b\rrbracket_{\omega})\neq\emptyset$. Then
$t\in\overline{\mathrm{int}\llbracket\lnot a\vee b\rrbracket_{\omega}}$.

We can interpret the boundary $\partial\llbracket\phi\rrbracket_{\omega}$ of
time set $\llbracket\phi\rrbracket_{\omega}$ as the time that the indicator
function $\chi_{\phi}(\omega,t)$ in Definition 6 changes its value. The
following lemma shows that the boundary
$\partial\llbracket\phi\rrbracket_{\omega}$ of every MTL–formula $\phi$ has
Lebesgue measure zero almost surely if $X_{t}$ has a density for all $t>0$ and
$AP$ is distinct in the sense of the following definition. A Borel set $B$ on
$\mathbb{R}$ is _distinct_ if its boundary $\partial B$ has Lebesgue measure
zero. An atomic formula $a\in AP$ is _distinct_ when the corresponding set
$B_{a}$ is distinct. The set of $AP$ of atomic formulas is said to be
_distinct_ when all $a\in AP$ are distinct.

######  Lemma 29.

Consider the case of the distinct set $AP$ of atomic formulas. Let
$(\Omega,\mathcal{F},\mathbb{P})$ be a complete probability space. Suppose
that $X$ is an almost surely continuous stochastic process such that $X_{t}$
has a density for every $t\in(0,\infty)$. Then, for every MTL–formula $\phi$
there exists some measurable set
$K\in\mathcal{F}\otimes\mathcal{B}([0,\infty))$ such that

  1. (i)

$\\{t;(\omega,t)\in K\\}$ is almost surely closed,

  2. (ii)

$\\{t;(\omega,t)\in K\\}$ has Lebesgue measure zero almost surely,

  3. (iii)

$\mathbb{P}(\\{\omega;(\omega,t)\in K\\})=0$ for every $t\in(0,\infty)$, and

  4. (iv)

$\partial\llbracket\phi\rrbracket_{\omega}\subset\\{t;(\omega,t)\in K\\}$.

For this proposal, in the following lemma, we show that the boundary of the
time set of the form $\Diamond_{\langle S,T\rangle}\phi$ is restricted to the
shift of the boundary of the form $\phi$.

######  Lemma 30.

Let $\phi$ be an MTL–formula and $\langle S,T\rangle$ be a positive interval
on $[0,\infty)$. Then it holds almost surely that

$\displaystyle\partial\llbracket\Diamond_{\langle
S,T\rangle}\phi\rrbracket_{\omega}\subset[(\partial\llbracket\phi\rrbracket_{\omega}\ominus
S)\cup(\partial\llbracket\phi\rrbracket_{\omega}\ominus T)],$ (36)

where $\partial\llbracket\phi\rrbracket_{\omega}\ominus
S:=\\{t-S;t\in\partial\llbracket\phi\rrbracket_{\omega}\\}\cap[0,\infty)$ and
$\partial\llbracket\phi\rrbracket_{\omega}\ominus
T:=\\{t-T;t\in\partial\llbracket\phi\rrbracket_{\omega}\\}\cap[0,\infty)$.

######  Proof 6.4.

Let $\langle S,T\rangle$ be the closed interval $[S,T]$. Suppose that
$t\in\partial\llbracket\Diamond_{\langle S,T\rangle}\phi\rrbracket_{\omega}$.
Then it is clear that
$(t+S,t+T)\cap\llbracket\phi\rrbracket_{\omega}=\emptyset$. If not, there
exists some neighborhood of $t$ whose every element $s$ satisfies
$(s+S,s+T)\cap\llbracket\phi\rrbracket_{\omega}\neq\emptyset$ and hence
$t\notin\partial\llbracket\Diamond_{\langle
S,T\rangle}\phi\rrbracket_{\omega}$. Again from
$t\in\partial\llbracket\Diamond_{\langle S,T\rangle}\phi\rrbracket_{\omega}$,
one of the following two statement holds:

  1. (i)

There exist some sequence $t_{n},\ n=1,2,3,\cdots$ in
$\llbracket\Diamond_{[S,T]}\phi\rrbracket_{\omega}$ such that
$\sup_{n}t_{n}=t$.

  2. (ii)

There exist some sequence $t_{n},\ n=1,2,3,\cdots$ in
$\llbracket\Diamond_{[S,T]}\phi\rrbracket_{\omega}$ such that
$\inf_{n}t_{n}=t$.

It is enough to show $S+t\in\partial\llbracket\phi\rrbracket_{\omega}$ or
$T+t\in\partial\llbracket\phi\rrbracket_{\omega}$ for (i) and (ii).

  1. (1)

Since $(S+t,T+t)\subset\llbracket\lnot\phi\rrbracket_{\omega}$,
$(S+t,S+t+\varepsilon)\cap\llbracket\lnot\phi\rrbracket_{\omega}\neq\emptyset$
for every positive $\varepsilon$. Together with
$\llbracket\phi\rrbracket_{\omega}\cap[S+t_{n},T+t_{n}]\neq\emptyset$,
$(S+t,T+t)\subset\llbracket\lnot\phi\rrbracket_{\omega}$ also implies
$[S+t_{n},S+t]\cap\llbracket\phi\rrbracket_{\omega}\neq\emptyset$ for every
$n\in\mathbb{N}$. Then
$(S+t-\varepsilon,S+t]\cap\llbracket\phi\rrbracket_{\omega}\neq\emptyset$ for
every positive $\varepsilon$.

  2. (2)

We can show
$(T+t-\varepsilon,T+t)\cap\llbracket\lnot\phi\rrbracket_{\omega}\neq\emptyset$
and $[T+t,T+t+\varepsilon)\cap\llbracket\phi\rrbracket_{\omega}\neq\emptyset$
by showing $[T+t,T+t_{n}]\cap\llbracket\phi\rrbracket_{\omega}\neq\emptyset$.
Indeed, $(S+t,T+t)\cap\llbracket\phi\rrbracket_{\omega}=\emptyset$ and
$[S+t_{n},T+t_{n}]\cap\llbracket\phi\rrbracket_{\omega}\neq\emptyset$ implies
$[T+t,T+t_{n}]\cap\llbracket\phi\rrbracket_{\omega}\neq\emptyset$.

Thus, we show the statement when $\langle S,T\rangle$ is closed. We can prove
the case of $\langle a,b\rangle=(S,T),[S,T),[S,T)$ in exactly the same way.

######  Proof 6.5 (Proof of Lemma 29).

Since the map $t\mapsto X_{t}(\omega)$ is almost surely continuous, there
exists some $N\in\mathcal{F}$ such that $\mathbb{P}(N)=0$ and $t\mapsto
X_{t}(\omega)$ is continuous whenever $\omega\notin N$. Suppose $a$ is an
atomic formula and $t\in\partial\llbracket a\rrbracket_{\omega}$. For any
positive $\varepsilon$, we can find $s$ and $s^{\prime}$ in the interval
$(t-\varepsilon,t+\varepsilon)$ such that $X_{s}(\omega)\in B_{a}$ and
$X_{s^{\prime}}(\omega)\notin B_{a}$. This is because $t$ is a boundary point
of the satisfaction set $\llbracket a\rrbracket_{\omega}$. Since the mapping
$t\mapsto X_{t}(\omega)$ is continuous for $\omega\notin N$, it follows that
$X_{t}(\omega)$ lies on the boundary $\partial B_{a}$. In other words,
$X_{t}(\omega)$ is located on the boundary of the set defined by the atomic
formula $a$. Put $K:=\\{(\omega,t);X_{t}(\omega)\in\partial B_{a}\\}\cup
N\times[0,\infty)$ and $K_{\omega}:=\\{t;(\omega,t)\in K\\}$. Hence, we get
$\partial\llbracket a\rrbracket_{\omega}\subset K_{\omega}$. Since $t\mapsto
X_{t}(\omega)$ is continuous almost surely and $X_{t}$ has a density for every
$t>0$, $K$ is measurable, $K_{\omega}$ is almost surely closed,

$\displaystyle\mathbb{P}(\\{\omega;(\omega,t)\in
K\\})\leq\mathbb{P}(\omega;X_{t}(\omega)\in\partial
B_{a})+\mathbb{P}(N)=0\hskip 10.0pt\forall t\in(0,\infty).$

Then it holds that

$\displaystyle\int_{[0,\infty)}\left\\{\int_{\Omega}\mbox{1}\mbox{l}_{K}(\omega,t)\mathbb{P}(d\omega)\right\\}dt=0.$
(37)

By using Fubini’s Theorem (see Theorem 8.8 in [Rud66]), we have

$\displaystyle\int_{\Omega}\left\\{\int_{[0,\infty)}\mbox{1}\mbox{l}_{K}(\omega,t)dt\right\\}\mathbb{P}(d\omega)=0,$

which implies that $K_{\omega}$ has Lebesgue measure zero almost surely (see
(b) of Theorem 1.39 in [Rud66]). When $K$ corresponds to a formula $\phi$ with
(i)-(iv), then $K$ also satisfies (i)-(iv) for$\lnot\phi$, since
$\partial\llbracket\lnot\phi\rrbracket_{\omega}=\partial\llbracket\phi\rrbracket_{\omega}$.
When $K_{1}$ and $K_{2}$ satisfy (i)-(iv) for $\phi_{1}$ and $\phi_{2}$
respectively, $K_{1}\cup K_{2}$ satisfies (i)-(iv) for
$\phi_{1}\wedge\phi_{2}$, since $\\{t;(\omega,t)\in K_{1}\cup K_{2}\\}$ is
closed, $\mathbb{P}(\omega;(\omega,t)\in K_{1}\cup K_{2})=0$ for
$t\in(0,\infty)$, and
$\partial\llbracket\phi_{1}\wedge\phi_{2}\rrbracket_{\omega}\subset\\{t;(\omega,t)\in
K_{1}\cup K_{2}\\}$. Suppose that $K$ satisfies (i)-(iv) for $\phi$. We show
that $\\{(\omega,t);t\in[(K_{\omega}\ominus S)\cup(K_{\omega}\ominus T)]\\}$
satisfies (i)–(iv) for $\Diamond_{\langle S,T\rangle}\phi$.

  1. (1)

Since $K_{\omega}$ is closed almost surely, $(K_{\omega}\ominus S)$ and
$(K_{\omega}\ominus T)$ are almost surely closed and then $(K_{\omega}\ominus
S)\cup(K_{\omega}\ominus T)$ is closed almost surely.

  2. (2)

From (37), it holds that

$\displaystyle\int_{[0,\infty)}\left\\{\int_{\Omega}\mbox{1}\mbox{l}_{\\{t\in
K_{\omega}\ominus
S\\}}(\omega,t)\mathbb{P}(d\omega)\right\\}dt=\int_{[S,\infty)}\left\\{\int_{\Omega}\mbox{1}\mbox{l}_{\\{t\in
K_{\omega}\\}}(\omega,t)\mathbb{P}(d\omega)\right\\}dt=0,$
$\displaystyle\int_{[0,\infty)}\left\\{\int_{\Omega}\mbox{1}\mbox{l}_{\\{t\in
K_{\omega}\ominus T\\}}(\omega,t)\
\mathbb{P}(d\omega)\right\\}dt=\int_{[T,\infty)}\left\\{\int_{\Omega}\mbox{1}\mbox{l}_{\\{t\in
K_{\omega}\\}}(\omega,t)\mathbb{P}(d\omega)\right\\}dt=0.$

By Fubini’s theorem, we have

$\displaystyle\int_{\Omega}\left\\{\int_{[0,\infty)}\mbox{1}\mbox{l}_{\\{t\in
K_{\omega}\ominus S\\}}(\omega,t)dt\right\\}\mathbb{P}(d\omega)$
$\displaystyle=0,$
$\displaystyle\int_{\Omega}\left\\{\int_{[0,\infty)}\mbox{1}\mbox{l}_{\\{t\in
K_{\omega}\ominus T\\}}(\omega,t)dt\right\\}\mathbb{P}(d\omega)$
$\displaystyle=0,$

which implies that $\\{(\omega,t);t\in(K_{\omega}\ominus
S)\cup(K_{\omega}\ominus T)\\}$ has Lebesgue measure zero almost surely.

  3. (3)

When $t>0$, we have

$\displaystyle\mathbb{P}(\omega;t\in(K_{\omega}\ominus
S)\cup(K_{\omega}\ominus T))$ $\displaystyle\leq$
$\displaystyle\mathbb{P}(\omega;t\in(K_{\omega}\ominus
S))+\mathbb{P}(\omega;t\in(K_{\omega}\ominus T))$ $\displaystyle\leq$
$\displaystyle\mathbb{P}(\omega;t+S\in K_{\omega})+\mathbb{P}(\omega;t+T\in
K_{\omega})=0.$

  4. (4)

From Lemma 30, $\partial\llbracket\Diamond_{\langle
S,T\rangle}\phi\rrbracket_{\omega}\subset[(\partial\llbracket\phi\rrbracket_{\omega}\ominus
S)\cup(\partial\llbracket\phi\rrbracket_{\omega}\ominus
T)]\subset[(K_{\omega}\ominus S)\cup(K_{\omega}\ominus T)]$ almost surely.

In the following lemma, we give a sufficient condition for convergence of the
indicator function of the formula with diamond or box operator.

######  Lemma 31.

Let $X$ be the solution of SDE (29) satisfying Assumption 6. Define an
MTL–formula $p$ as

$\displaystyle X(\omega),t\models p\Leftrightarrow X_{t}(\omega)\in B_{p}$

for some distinct set $B_{p}$ on $\mathbb{R}$. Let $\langle S,T\rangle$ be a
positive interval on $[0,\infty)$. If $p$ satisfies (31) and (32), the
following statements hold:

  1. (1)

Define $\phi:=\Diamond_{\langle S,T\rangle}p$. Then
$\chi^{(n)}_{\phi}(\omega,t)\rightarrow\chi_{\phi}(\omega,t)$ for every
$t\in[0,\infty)$.

  2. (2)

Define $\psi:=\Box_{\langle S,T\rangle}p$. Then
$\chi^{(n)}_{\psi}(\omega,t)\rightarrow\chi_{\psi}(\omega,t)$ for every
$t\in[0,\infty)$.

Here, $\chi_{\phi}^{(n)}(\omega,t)$, $\chi_{\psi}^{(n)}(\omega,t)$,
$\chi_{\phi}(\omega,t)$, and $\chi_{\psi}(\omega,t)$ are the indicator
functions defined in Definition 6.

######  Proof 6.6.

First, let us show that $\langle t+S,t+T\rangle\cap\llbracket
p\rrbracket_{\omega}\neq\emptyset$ implies
$(t+S,t+T)\cap\mathrm{int}\llbracket p\rrbracket_{\omega}\neq\emptyset$ almost
surely. If $\partial\llbracket p\rrbracket_{\omega}\cap\langle
t+S,t+T\rangle=\emptyset$ and $\langle t+S,t+T\rangle\cap\llbracket
p\rrbracket_{\omega}\neq\emptyset$, then it follows that $X(\omega),s\models
p$ for all $s\in\langle t+S,t+T\rangle$, and therefore, $\langle
t+S,t+T\rangle\subset\llbracket p\rrbracket_{\omega}$. Consequently,
$(t+S,t+T)\cap\mathrm{int}\llbracket p\rrbracket_{\omega}\neq\emptyset$. Next,
suppose $\partial\llbracket p\rrbracket_{\omega}\cap\langle
t+S,t+T\rangle\neq\emptyset$ and $\langle t+S,t+T\rangle\cap\llbracket
p\rrbracket_{\omega}\neq\emptyset$. Since $\\{X_{t}\\}_{t\geq 0}$ satisfies
Assumption 6, $X_{t}$ has a density for $t>0$ by A.1. When $t+S>0$, we have
$t+T>t+S>0$, and Lemma 29 implies that $t+S$ and $t+T$ do not belong to
$\partial\llbracket p\rrbracket_{\omega}$ almost surely. Thus, we have
$\partial\llbracket p\rrbracket_{\omega}\cap(t+S,t+T)\neq\emptyset$, which
implies $\llbracket p\rrbracket_{\omega}\cap(t+S,t+T)\neq\emptyset$.
Therefore, we conclude from (31) that $(t+S,t+T)\cap\mathrm{int}\llbracket
p\rrbracket_{\omega}\neq\emptyset$. If $t+S=0$, $\partial\llbracket
p\rrbracket_{\omega}$ intersects the open set of the form $[0,t+T)$ or
$(0,t+T)$ on $[0,\infty)$. Then, from (31), we can conclude
$\mathrm{int}\llbracket p\rrbracket_{\omega}\cap(t+S,t+T)\neq\emptyset$.

We can show in similar way that $\langle t+S,t+T\rangle\cap\llbracket\lnot
p\rrbracket_{\omega}\neq\emptyset$ implies
$(t+S,t+T)\cap\mathrm{int}\llbracket\lnot p\rrbracket_{\omega}\neq\emptyset$
almost surely.

Now let us prove (i) and (ii). Suppose $X(\omega),t\models\phi$. Since
$(t+S,t+T)\cap\mathrm{int}\llbracket p\rrbracket_{\omega}$ is a nonempty open
set, there exists $s\in(\Lambda_{n}(t)+S,\Lambda_{n}(t)+T)\cap\mathbb{N}/n$
such that $X(\omega),s\models_{n}p$ for sufficiently large $n$. Hence,
$X,\Lambda_{n}(t)\models_{n}\phi$. By applying the same argument, we can show
from (32) that if $X(\omega),t\not\models\psi$, then
$X(\omega),\Lambda_{n}(t)\not\models_{n}\psi$ for sufficiently large $n$.

On the other hand, suppose $X(\omega),t\not\models\phi$. Then $\llbracket
p\rrbracket_{\omega}\cap(S,T)=\emptyset$ and $\partial\llbracket
p\rrbracket_{\omega}\cap(S,T)=\emptyset$. If $t+S>0$, according to A.1 and
Lemma 29, $t+S$ and $t+T$ do not belong to $\partial\llbracket
p\rrbracket_{\omega}$ almost surely. Thus, there exists $\varepsilon>0$ such
that $(t+S-\varepsilon,t+T-\varepsilon)\subset\llbracket\lnot
p\rrbracket_{\omega}$, and hence
$(\Lambda_{n}(t)+S,\Lambda_{n}(t)+T)\cap\llbracket
p\rrbracket_{\omega}=\emptyset$ for sufficiently large $n$. If $t+S=0$, since
$\Lambda_{n}(t)=t=0$, it holds that

$\displaystyle X(\omega),\Lambda_{n}(t)\not\models_{n}\phi\Leftrightarrow
X(\omega),0\not\models_{n}\Diamond_{\langle 0,T\rangle}p,$ $\displaystyle
X(\omega),t\not\models\phi\Leftrightarrow
X(\omega),0\not\models\Diamond_{\langle 0,T\rangle}p.$

Then it is clear that $X(\omega),t\not\models\phi$ implies
$X(\omega),\Lambda_{n}(t)\not\models_{n}\phi$. Now we have shown that
$X(\omega),t\not\models_{n}\phi$ for sufficiently large $n$. The same argument
can be applied to prove that if $X(\omega),t\models\psi$, then
$X(\omega),\Lambda_{n}(t)\models_{n}\psi$ for sufficiently large $n$.

######  Lemma 32.

Suppose that a propositional formula $p$ satisfies the conditions introduced
in the statement of Theorem 25. Specifically, let $\langle
x_{i},y_{i}\rangle,\ i=1,\cdots,k$ be pairwise disjoint positive intervals,
and define $B_{p}:=\bigcup_{i=1}^{k}\langle x_{i},y_{i}\rangle$. Define a
propositional formula $p,p_{1},\cdots,p_{k}$ by

$\displaystyle X(\omega),t\models p\Leftrightarrow X_{t}(\omega)\in B_{p},$
$\displaystyle X(\omega),t\models_{n}p\Leftrightarrow X_{t}(\omega)\in B_{p},$
$\displaystyle X(\omega),t\models p_{i}\Leftrightarrow X_{t}(\omega)\in\langle
x_{i},y_{i}\rangle\quad\text{for }i=1\cdots,k,$ $\displaystyle
X(\omega),t\models_{n}p_{i}\Leftrightarrow X_{t}(\omega)\in\langle
x_{i},y_{i}\rangle\quad\text{for }i=1\cdots,k.$

Then $p$ satisfies (31) and (32). Namely,

$\displaystyle\llbracket p\rrbracket_{\omega}$
$\displaystyle\subset\overline{\mathrm{int}\llbracket
p\rrbracket_{\omega}},\hskip 10.0pt\text{a.s. },$
$\displaystyle\llbracket\lnot p\rrbracket_{\omega}$
$\displaystyle\subset\overline{\mathrm{int}\llbracket\lnot
p\rrbracket_{\omega}},\hskip 10.0pt\text{a.s. }$

######  Proof 6.7.

First note that

$\displaystyle X(\omega),t\models p\Leftrightarrow
X(\omega),t\models\bigvee_{i=1}^{k}p_{i},$ $\displaystyle
X(\omega),t\models_{n}p\Leftrightarrow
X(\omega),t\models_{n}\bigvee_{i=1}^{k}p_{i},$

where $\bigvee_{i=1}^{k}p_{i}=p_{1}\vee p_{2}\vee\cdots\vee p_{k}$. If
$B_{p}=\emptyset$ or $B_{p}=\mathbb{R}$, clearly $\llbracket
p\rrbracket_{\omega}=\emptyset$ or $\llbracket
p\rrbracket_{\omega}=[0,\infty)$, respectively. Hence (31) and (32) holds.
Otherwise, From Lemma 26, every $p_{i}$ satisfies (31) and (32) almost surely.
Now we show that $\llbracket
p\rrbracket_{\omega}(=\llbracket\bigvee_{i=1}^{k}p_{i}\rrbracket_{\omega})$
satisfies (31) and (32).

(31):

Let $t\in\llbracket\bigvee_{i=1}^{k}p_{i}\rrbracket_{\omega}$ and $O$ be a
neighborhood of $t$. Since
$\llbracket\bigvee_{i=1}^{k}p_{i}\rrbracket_{\omega}=\bigcup_{i=1}^{k}\llbracket
p_{i}\rrbracket_{\omega}$, there exists some $i\in\\{1,\cdots,k\\}$ such that
$t\in\llbracket p_{i}\rrbracket_{\omega}$. Since $\llbracket
p_{i}\rrbracket_{\omega}$ satisfies (31) almost surely and
$\mathrm{int}\llbracket
p_{i}\rrbracket_{\omega}\subset\mathrm{int}\llbracket\bigvee_{i=1}^{k}p_{i}\rrbracket_{\omega}$,
$O\cap\mathrm{int}\llbracket\bigvee_{i=1}^{k}p_{i}\rrbracket_{\omega}\neq\emptyset$
almost surely. Then $\bigvee_{i=1}^{k}p_{i}$ satisfies (31) almost surely.

(32):

Let $t\in\llbracket\lnot\bigvee_{i=1}^{k}p_{i}\rrbracket_{\omega}$. If
$t\in\mathrm{int}\llbracket\lnot\bigvee_{i=1}^{k}p_{i}\rrbracket_{\omega}$,
then for any neighborhood $O$ of $t$, we have
$O\cap\mathrm{int}\llbracket\lnot\bigvee_{i=1}^{k}p_{i}\rrbracket_{\omega}\neq\emptyset$.
Thus, it suffices to show that
$O\cap\mathrm{int}\llbracket\lnot\bigvee_{i=1}^{k}p_{i}\rrbracket_{\omega}\neq\emptyset$
for any neighborhood $O$ of $t$ whenever
$t\in\partial\llbracket\lnot\bigvee_{i=1}^{k}p_{i}\rrbracket_{\omega}$. Since
$\mathrm{int}\llbracket\lnot\bigvee_{i=1}^{k}p_{i}\rrbracket_{\omega}=\mathrm{int}(\bigcap_{i=1}^{k}\llbracket\lnot
p_{i}\rrbracket_{\omega})=\bigcap_{i=1}^{k}\mathrm{int}\llbracket\lnot
p_{i}\rrbracket_{\omega}$, there must exist some $i\in{1,\cdots,k}$ such that
$t\in\partial\llbracket\lnot p_{i}\rrbracket_{\omega}$. Indeed, if
$t\in\mathrm{int}\llbracket\lnot p_{i}\rrbracket_{\omega}$ for every $i$, then
$t\in\mathrm{int}\llbracket\lnot\bigvee_{i=1}^{k}p_{i}\rrbracket_{\omega}$.
Since $t\mapsto X_{t}(\omega)$ is continuous almost surely and $\langle
x_{1},y_{1}\rangle,\cdots\langle x_{k},y_{k}\rangle$ are pairwise separated,
we have $X_{t}(\omega)\in[x_{j},y_{j}]^{C}$ when $j\neq i$ almost surely, and
hence $t\in\mathrm{int}\llbracket\lnot p_{j}\rrbracket_{\omega}$ for $i\neq j$
almost surely. Therefore, $t\in\bigcap_{j\neq i}\mathrm{int}\llbracket\lnot
p_{j}\rrbracket_{\omega}$. Then,
$(t-\delta,t+\delta)\cap[0,\infty)\subset\bigcap_{j\neq
i}\mathrm{int}\llbracket\lnot p_{j}\rrbracket_{\omega}$ for sufficiently small
$\delta>0$. Now, since $p_{i}$ satisfies (31), we have
$(t-\delta,t+\delta)\cap\mathrm{int}\llbracket\lnot
p_{i}\rrbracket_{\omega}\neq\emptyset$. Hence,
$(t-\delta,t+\delta)\cap\mathrm{int}\llbracket\bigvee_{j=1}^{k}\lnot
p_{j}\rrbracket_{\omega}=(t-\delta,t+\delta)\cap{\bigcap_{j=1}^{k}\mathrm{int}\llbracket\lnot
p_{j}\rrbracket_{\omega}}=(t-\delta,t+\delta)\cap\mathrm{int}\llbracket\lnot
p_{i}\rrbracket_{\omega}\neq\emptyset$.

######  Proof 6.8 (Proof of Theorem 25).

From the condition on $B_{p}$, it is a distinct set. Then Lemma 31 and Lemma
32 implies the almost sure convergence of $\chi^{(n)}{\phi}(\omega,t)$ and
$\chi^{(n)}{\psi}(\omega,t)$ for every $t\in[0,\infty)$. Finally, Lemma 24 can
be employed to show the convergence of probability.

###  6.2. The case of $\flat$MTL–formulas

Now, we prove the convergence result for general $\flat$MTL–formulas. Let $X$
be the solution of SDE (29) with Assumption 6. Henceforth, we discuss under
the following assumption: For every propositional formula $p$,

$\displaystyle X(\omega),t\models p\Leftrightarrow X_{t}(\omega)\in B_{p},$
(38)

for some $B_{p}$, which is a union of pairwise separated positive intervals on
$\mathbb{R}$. Here $B_{p}$ may possibly be $\emptyset$ or $\mathbb{R}$.

######  Remark 33.

We give some examples of setting so that every propositional formula satisfies
Assumption 6.2. Let $B_{1},\cdots,B_{k}$ be positive intervals on $\mathbb{R}$
such that

  1. (i)

$\bigcup_{i=1}^{k}B_{i}=\mathbb{R}$.

  2. (ii)

$B_{i}\cap B_{j}=\emptyset$ if $i\neq j$.

We define the semantics of atomic formulas $AP:=\\{a_{1},\cdots,a_{k}\\}$ as
$X(\omega),t\models a_{i}\Leftrightarrow X_{t}(\omega)\in B_{i}$ for
$i=1,\cdots,k$. Then, every propositional formula clearly satisfies Assumption
6.2. Given this fact, if a propositional formula $p$ satisfies Assumption 6.2,
$\lnot p$ also satisfies Assumption 6.2.

Under these settings, we show the following statement.

######  Theorem 34.

Suppose that $\\{X_{t}\\}_{t\geq 0}$ is the solution of SDE (29) with
Assumption 6. Let $AP$ be the set of atomic formulas such that every
propositional formula satisfies Assumption 6.2. Let $\phi$ be a
$\flat$MTL–formula. Then
$\chi^{(n)}_{\phi}(\omega,t)\rightarrow\chi_{\phi}(\omega,t)$ almost surely
for every $t\in[0,\infty)$. In particular,
$\mathbb{P}(\omega;X(\omega),\Lambda_{n}(t)\models_{n}\phi)\rightarrow\mathbb{P}(\omega;X(\omega),t\models\phi)$
for all $t\in[0,\infty)$.

######  Remark 35.

Under Assumption 6.2, every $\flat$MTL–formula $\phi$ is the following form:

$\displaystyle\phi=\bigodot_{i=1}^{k}\phi_{i}$

where $\bigodot_{i=1}^{k}:\\{0,1\\}^{k}\rightarrow\\{0,1\\}$ is a Boolean
combination and every $\phi_{i}$ satisfies one of the following:

  * •

$\phi_{i}$ is a propositional formula with Assumption 6.2.

  * •

$\phi_{i}=\Diamond_{I}p$ with a positive interval $I$ and a propositional
formula $p$ satisfying Assumption 6.2.

  * •

$\phi_{i}=\Box_{I}p$ with a positive interval $I$ and a propositional formula
$p$ satisfying Assumption 6.2.

In other words, $\flat$MTL is an MTL in which every temporal operator is
constructed using a diamond operator, and no temporal operator is nested. On
the other hand, the counterexample presented in Section 5 is an MTL–formula
with the quadruple nested diamond operator. Then, the convergence result for
MTL–formulas with diamond operators depends on the nesting level.

######  Lemma 36.

Put Assumption 6 and Assumption 6.2. Let $p$ be a propositional formula. Then
$\chi^{(n)}_{p}(\omega,t)\rightarrow\chi_{p}(\omega,t)$ almost surely, for
every $t\in(0,\infty)$. In particular,
$\mathbb{P}(\omega;X(\omega),\Lambda_{n}(t)\models_{n}p)\rightarrow\mathbb{P}(\omega;X(\omega),t\models
p)$.

######  Proof 6.9.

First note that $X(\omega),t\models p$ is equivalent to $X_{t}(\omega)\in
B_{p}$ for some $B_{p}\subset\mathbb{R}$. Let $t=0$. Then $\Lambda_{n}(0)=0$
and hence $X(\omega),\Lambda_{n}(0)\models_{n}p$ is equivalent to
$X(\omega),0\models B_{p}$. Next, let $t>0$. By the definition of indicator
functions , $\chi_{p}(\omega,t)=1$ is equivalent to $X_{t}(\omega)\in B_{p}$
and $\chi^{(n)}_{p}(\omega,t)=1$ is equivalent to
$X_{\Lambda_{n}(t)}(\omega)\in B_{p}$. From Assumption 6.2, $B_{p}$ is
distinct, then Lemma 29 implies that $t\notin\partial\llbracket
p\rrbracket_{\omega}$ almost surely. Then almost surely there exists some
$\varepsilon>0$ such that $\chi_{p}(\omega,s)=\chi_{p}(\omega,t)$ for every
$s\in(t-\varepsilon,t+\varepsilon)\cap[0,\infty)$. Then it holds almost surely
that
$\chi^{(n)}_{p}(\omega,t)=\chi_{p}(\omega,\Lambda_{n}(t))=\chi_{p}(\omega,t)$
for sufficiently large $n$.

######  Proof 6.10 (Proof of Theorem 34).

Fix $t\in[0,\infty)$. It is clear that $\phi$ is Boolean combination of
$\\{\phi_{i},i=1,\cdots,k\\}$, where $\phi_{i}$ is a propositional formula or
formula of the form $\Diamond_{\langle S,T\rangle}p$ where $\langle
S,T\rangle$ is positive interval and $p$ is propositional formula. Then there
exists some function
$\bigodot_{i=1}^{k}:\\{0,1\\}^{k}\longrightarrow\\{0,1\\}$ such that

$\displaystyle\chi_{\phi}(\omega,t)$
$\displaystyle=\bigodot_{i=1}^{k}\chi_{\phi_{i}}(\omega,t),$ (39)
$\displaystyle\chi^{(n)}_{\phi}(\omega,t)$
$\displaystyle=\bigodot_{i=1}^{k}\chi^{(n)}_{\phi_{i}}(\omega,t).$ (40)

From Assumption 6.2 and Lemma 32, every propositional formula satisfies (31)
and (32). Then we can apply Lemma 31 and Lemma 36 to show that
$\chi^{(n)}_{\phi_{i}}(\omega,t)$ converges almost surely to
$\chi_{\phi_{i}}(\omega,t)$ for every $i=1,\cdots,k$. Then, almost surely,
there exists some large $N\in\mathbb{N}$ such that
$\chi^{(n)}_{\phi_{i}}(\omega,t)=\chi_{\phi_{i}}(\omega,t)$ for $n\geq N$ and
$i=1,\cdots,k$. Therefore the left–hand side of (40) converges to the left
side of (39) almost surely. Once we have shown the almost sure convergence of
(40) to (39), one can apply Lemma 24 to see the convergence of the
probability.

######  Remark 37.

In Assumption 6.2, we represent every propositional formula as a union of
pairwise separated sets. It is one of the vital assumptions in our result. Let
$X:=\\{X_{t}\\}_{t\geq 0}$ be one-dimensional Brownian motion starting at
zero. Consider the case that $a,b$ are atomic formulas such that
$X(\omega),\models a\Leftrightarrow X_{t}\in B_{a}$ and $X(\omega),t\models
B_{b}$, where $B_{a}:=(-\infty,1)$ and $B_{b}:=(1,\infty)$. Let
$p:=\lnot(a\wedge b)$ and $\phi:=\Diamond_{\langle S,T\rangle}p$. Since
$\overline{B_{a}}\cap\overline{B_{b}}\neq\emptyset$, $B_{a}$ and $B_{b}$ is
not separated. Since $X_{0}\neq 1$ and $X_{t}$ has density for all $t>0$,
$\mathbb{P}(\omega;X_{t}(\omega)=1)=0$ for all $t\in[0,\infty)\cap\mathbb{Q}$.
Hence the sigma-additivity of probability measure implies $\mathbb{P}(\exists
t\in[0,\infty)\cap\mathbb{Q},\ X_{t}=1)=0$. Then
$\mathbb{P}(\omega;X(\omega),\Lambda_{n}(0)\models_{n}\Diamond_{\langle
S,T\rangle}p)=0$ for every $n,S,T$ and then
$\mathbb{P}(\omega;X(\omega),\Lambda_{n}(0)\models_{n}\phi)=0$. On the other
hand, if $\tau_{1}(\omega):=\inf\\{t\geq 0;X_{t}(\omega)=1\\}\in(S,T)$ then
$X(\omega),0\models\phi$. From Theorem 5 and the monotonicity of probability
measures, then
$\mathbb{P}(\omega;X(\omega),0\models\phi)\geq\mathbb{P}(\tau_{1}\in(S,T))>0$
and then $\mathbb{P}(\omega;X(\omega),0\models_{n}\phi)$ does not converge to
$\mathbb{P}(\omega;X(\omega),0\models\phi)$.

###  6.3. Example of convergence

Let us show an example of an MTL–formula for standard Brownian motion to
illustrate the convergence result Theorem 34. Consider the following settings:

  * •

$X:=\\{X_{t}\\}_{t\geq 0}$ is a standard Brownian motion starting at
$x\in\mathbb{R}$.

  * •

$p$ is an atomic formula defined as

$\displaystyle X(\omega),t\models p\iff X_{t}(\omega)\in(x,\infty),$
$\displaystyle t\in[0,\infty),$ (41) $\displaystyle
X(\omega),t\models_{n}p\iff X_{t}(\omega)\in(x,\infty),$ $\displaystyle
t\in\mathbb{N}/n.$ (42)

  * •

$\phi=\lnot(\Diamond_{(0,1)}p)$.

It is well–known that the path of standard Brownian motion has a quite zig–zag
sample path:

######  Fact 38 (see 2.7.18 in [KS91]).

With probability one, the path $t\mapsto\\{X_{t}(\omega)-x\\}$ changes its
sign infinitely many times in any time interval $[0,\epsilon],\ \epsilon>0$.

Then there exists $t\in I$ such that $X_{t}(\omega)\in(x,\infty)$ almost
surely, which implies

$\displaystyle(\exists t\in(0,1))[X(\omega),t\models p]$

almost surely. Therefore we have
$\mathbb{P}(\omega\in\Omega;X(\omega),0\models\phi)=0$. On the other hand, the
joint density function of $X$ has the following form (see Chapter 2 in
[KS91]):

$\displaystyle\mathbb{P}(X_{t_{1}}\in(-\infty,x],X_{t_{2}}\in(-\infty,x],\cdots,X_{t_{n}}\in(-\infty,x])$
$\displaystyle=$
$\displaystyle\int_{-\infty}^{x}\int_{-\infty}^{x}\cdots\int_{-\infty}^{x}p(t_{1};x,y_{1})p(t_{2}-t_{1};y_{1},y_{2})\cdots
p(t_{n}-t_{n-1};y_{n-1},y_{n})dy_{1}dy_{2}\cdots dy_{n},$ (43)

where $t_{1}<t_{2}<\cdots<t_{n}$ and

$\displaystyle p(t,x,y)=\frac{1}{\sqrt{2\pi
t}}\exp\left\\{-\frac{(x-y)^{2}}{2t}\right\\},\hskip 10.0ptt>0,\
x,y\in\mathbb{R}.$

Since $p(t,x,y)$ is positive for all $t$, $x$, $y$, the probability (43) is
positive, namely, $\mathbb{P}(\omega\in\Omega;X(\omega),0\models_{n}\phi)>0$
for every $n\in\mathbb{N}$. Despite its positivity, Theorem 34 assures that
$\mathbb{P}(\omega\in\Omega;X(\omega),0\models_{n}\phi)\rightarrow\mathbb{P}(\omega\in\Omega;X(\omega),0\models\phi)=0$
as $n\rightarrow\infty$.

##  7\. Conclusion

In conclusion, this study has examined the measurability of events defined by
continuous MTL–formulas, assuming that the underlying stochastic process is
measurable as a mapping from sample to time.

Moreover, we demonstrated a counterexample that highlights the lack of
convergence of the probability derived from discrete semantics to that derived
from continuous semantics, specifically when the intervals within diamond
operators are allowed to be bounded open.

Furthermore, the study explored the case of $\flat$MTL–formulas, which only
have $\Box$ or $\Diamond$ without nest as modalities, and demonstrated that
the probability obtained from discrete semantics converges to the probability
obtained from continuous semantics for every formula within this framework.
This finding suggests that $\flat$MTL–formulas exhibit a desirable convergence
property, highlighting their applicability and reliability in capturing system
behaviors.

In light of these results, our future work should focus on understanding the
underlying factors and mechanisms that contribute to the convergence or
divergence of probability between discrete and continuous semantics in various
formula contexts. By gaining deeper insights into these dynamics, we may
enhance the effectiveness and accuracy of probability simulations and
predictions within formal verification and system analysis.

## References

  * [AFH96] Rajeev Alur, Tomás Feder, and Thomas A Henzinger.  The benefits of relaxing punctuality.  J. ACM, 43(1):116–146, January 1996.
  * [AH89] R. Alur and T.A. Henzinger.  A really temporal logic.  30th Annual Symposium on Foundations of Computer Science, Foundations of Computer Science, 1989., 30th Annual Symposium on, pages 164 – 169, 1989.  doi:10.1109/SFCS.1989.63473.
  * [ARA00] A.A. Abouzeid, S. Roy, and M. Azizoglu.  Stochastic modeling of TCP over lossy links.  In Proceedings IEEE INFOCOM 2000. Conference on Computer Communications. Nineteenth Annual Joint Conference of the IEEE Computer and Communications Societies (Cat. No. 00CH37064), volume 3, pages 1724–1733. IEEE, 2000.  doi:10.1109/INFCOM.2000.832572.
  * [CZ11] E.M. Clarke and P. Zuliani.  Statistical Model Checking for Cyber-Physical Systems., volume 6996 of Lecture Notes in Computer Science. 6996.  Springer Berlin Heidelberg, 2011.  doi:10.1007/978-3-642-24372-1.
  * [Del72] C. Dellacherie.  Capacités et processus stochastiques. Ergebnisse der Mathematik und ihrer Grenzgebiete: Bd. 67. Springer-Verlag, 1972.
  * [DM11] Dario Della Monica.  Expressiveness, decidability, and undecidability of interval temporal logic.  PhD thesis, April 2011.
  * [FP10] N. Fournier and J. Printems.  Absolute continuity for some one-dimensional processes.  Bernoulli, 16(2):343 – 360, 2010.  doi:10.3150/09-BEJ215.
  * [FR10] Carlo A Furia and Matteo Rossi.  A theory of sampling for continuous-time metric temporal logic.  ACM Trans. Comput. Log., 12(1):1–40, November 2010.
  * [FT15] J. Fu and U. Topcu.  Computational methods for stochastic control with metric interval temporal logic specifications.  CDC, pages 7440 – 7447, 2015.  doi:10.1109/CDC.2015.7403395.
  * [GR21] V. Goranko and A. Rumberg.  Temporal Logic.  In Edward N. Zalta, editor, The Stanford Encyclopedia of Philosophy. Metaphysics Research Lab, Stanford University, Fall 2021 edition, 2021.  URL: https://plato.stanford.edu/archives/fall2023/entries/logic-temporal/.
  * [HPS03] J. Hu, M. Prandini, and S. Sastry.  Probabilistic safety analysis in three dimensional aircraft flight.  42nd IEEE International Conference on Decision and Control (IEEE Cat. No.03CH37475), Decision and Control, 2003. Proceedings. 42nd IEEE Conference on, Decision and control, 5:5335, 2003.  doi:10.1109/CDC.2003.1272485.
  * [JP14] L. Jun and P. Prabhakar.  Switching control of dynamical systems from metric temporal logic specifications.  2014 IEEE International Conference on Robotics and Automation (ICRA), Robotics and Automation (ICRA), 2014 IEEE International Conference on, pages 5333 – 5338, 2014.  doi:10.1109/ICRA.2014.6907643.
  * [Kec95] A.S. Kechris.  Classical Descriptive Set Theory. Graduate Texts in Mathematics. ISSN:00725285: 156. Springer New York, 1995\.
  * [KF08] S. Karaman and E. Frazzoli.  Vehicle routing problem with metric temporal logic specifications.  2008 47th IEEE Conference on Decision and Control, Decision and Control, 2008. CDC 2008. 47th IEEE Conference on, pages 3953 – 3958, 2008.  doi:10.1109/CDC.2008.4739366.
  * [Kon13] S. Konur.  A survey on temporal logics for specifying and verifying real-time systems.  Frontiers of Computer Science: Selected Publications from Chinese Universities, 7(3):370 – 403, 2013.  doi:10.1007/s11704-013-2195-2.
  * [Koy90] R. Koymans.  Specifying real-time properties with metric temporal logic.  Real-Time Systems, 2(4):255–299, 1990.  doi:10.1007/BF01995674.
  * [KS91] I. Karatzas and S.E. Shreve.  Brownian motion and stochastic calculus, volume 113 of Graduate Texts in Mathematics.  Springer-Verlag, New York, second edition, 1991.  doi:10.1007/978-1-4612-0949-2.
  * [MLD16] F.J Montana, J. Liu, and T.J. Dodd.  Sampling-based stochastic optimal control with metric interval temporal logic specifications.  2016 IEEE Conference on Control Applications (CCA), Control Applications (CCA), 2016 IEEE Conference on, pages 767 – 773, 2016.  doi:10.1109/CCA.2016.7587911.
  * [OW05] J Ouaknine and J Worrell.  On the decidability of metric temporal logic.  In 20th Annual IEEE Symposium on Logic in Computer Science (LICS’ 05), pages 188–197. IEEE, 2005.
  * [PAM17] Y.V. Pant, H. Abbas, and R. Mangharam.  Smooth operator: Control using the smooth robustness of temporal logic.  In 1st Annual IEEE Conference on Control Technology and Applications, CCTA 2017, pages 1235–1240 – 1240, 2017.  doi:10.1109/CCTA.2017.8062628.
  * [Pnu77] A. Pnueli.  The temporal logic of programs.  18th Annual Symposium on Foundations of Computer Science (sfcs 1977), pages 46–57, 1977.  doi:10.1109/SFCS.1977.32.
  * [Pri67] A.N. Prior.  Past, present and future. Clarendon Press, 1967.
  * [Rud66] Walter Rudin.  Real and complex analysis. McGraw-Hill series in higher mathematics. McGraw-Hill, 1966.
  * [RY91] D. Revuz and M. Yor.  Continuous Martingales and Brownian Motion. Grundlehren der mathematischen Wissenschaften, A Series of Comprehensive Studies in Mathematics. ISSN:00727830: 293. Springer Berlin Heidelberg : Imprint: Springer, 1991.
  * [Shr04] S.E. Shreve.  Stochastic calculus for finance. [Vol.] 2, Continuous-time models.  Springer, 2004.
  * [Shr05] S.E. Shreve.  Stochastic calculus for finance. [Vol.] 1, The binomial asset pricing model.  Springer, 2005.

##  Appendix A Some appendices for stochastic calculus

In this section, we prove Lemma 27. Let us recall the claim:

######  Lemma 39.

Let $X$ be a strong solution of SDE (29) on $(\Omega,\mathcal{F},\mathbb{P})$.
Put Assumption 6. Then, the following statements hold:

  1. (1)

Put

$\displaystyle\mathcal{L}^{a}_{\omega}:=\\{t\geq 0;X_{t}(\omega)=a\\},\hskip
10.0pta\in\mathbb{R},\ \omega\in\Omega.$ (44)

Then $\mathcal{L}^{a}_{\omega}$ is dense in itself, almost surely, for all
$a\in\mathbb{R}$.

  2. (2)

Almost surely, the set of points of local maximum and local minimum for the
path $t\mapsto X(\omega)$ is dense in $[0,\infty)$, and all local maxima and
local minima are strict.

Toward this goal, we cite a similar fact about Brownian motion: [2.9.7 and
2.9.12 in [KS91]] Let $X$ be a Brownian motion on
$(\Omega,\mathcal{F},\mathbb{P})$. Then the following statements hold:

  1. (1)

Put

$\displaystyle\mathcal{L}^{a}_{\omega}:=\\{t\geq 0;X_{t}(\omega)=a\\},\hskip
10.0pta\in\mathbb{R},\ \omega\in\Omega.$ (45)

Then $\mathcal{L}^{a}_{\omega}$ is dense in itself, almost surely, for all
$a\in\mathbb{R}$.

  2. (2)

Almost surely, the set of points of local maximum for the Brownian path is
dense in $[0,\infty)$, and all local maxima are strict.

######  Lemma 40.

Almost surely, the set of points of local minimum for the Brownian path
$t\mapsto W_{t}(\omega)$ is dense in $[0,\infty)$, and all local minima are
strict.

######  Proof A.1.

Let $X$ be Brownian motion and define $\tilde{X}:=\\{\tilde{X}_{t}\\}_{t\geq
0}$ by $\tilde{X}_{t}(\omega):=-X_{t}(\omega)$. By rotational invariance (see
3.3.18 in [KS91]), $\tilde{X}$ is also Brownian motion. We can apply Theorem
39 so that the set of local maximum for $\tilde{X}(\omega)$ is dense, and all
the local maxima are strict, almost surely. Now, since all the local minima of
$X(\omega)$ are local maxima of $\tilde{X}(\omega)$, then our statement holds.

Now, we have shown Lemma 27 for the case of Brownian motion. It remains to
extend this statement to the case of SDE (29) under Assumption 6. Before
showing the solution of such an SDE, we have to guarantee the existence and
uniqueness of SDE:

[5.5.17 in [KS91]] Assume that $b:\mathbb{R}\rightarrow\mathbb{R}$ is bounded
and $\sigma:\mathbb{R}\rightarrow\mathbb{R}$ is Lipschitz continuous with
$\sigma^{2}$ bounded away from zero on every compact subset of $\mathbb{R}$.
Then, for every initial $\xi\in\mathbb{R}$, equation (29) has unique strong
solution.

Furthermore, we show the convergence of the probability of MTL–formula for
SDEs with a density function. The following proposition assures the existence
of density for SDE (29):

[Theorem 2.1 in [FP10]] Let $\xi$ be the constant value in $\mathbb{R}$.
Assume that $\sigma$ is Hölder continuous with exponent $\theta\in[1/2,1]$ and
that $b$ is measurable and at most linear growth. Consider a continuous
solution $\\{X_{t}\\}_{t\geq 0}$ to (29). Then, for all $t>0$, the law of
$X_{t}$ has a density on the set $\\{x\in\mathbb{R};\sigma(x)\neq 0\\}$. It is
easy to make sure that the above two propositions can be applied to the unique
existence and absolute continuity of $X$ under Assumption 6.

To extend Theorem 39 and Lemma 40 to the case of the stochastic differential
equation (29), we can make use of the following representation of the solution
$X$ as a time change of Brownian motion: [[KS91, 5.5.13]] Assume Assumption 6.
Fix a number $c\in\mathbb{R}$ and define the scale function

$\displaystyle p(x)$
$\displaystyle:=\int_{c}^{x}\exp\left\\{-2\int_{c}^{\xi}\frac{b(\zeta)d\zeta}{\sigma^{2}(\zeta)}\right\\}d\xi;\hskip
10.0ptx\in\mathbb{R}$

and inverse $q:(p(-\infty),p(\infty))\rightarrow\mathbb{R}$ of $p$. A process
$X=\\{X_{t}\\}_{t\geq 0}$ is a strong solution of equation (29) if and only if
the process $Y:=\\{Y_{t}=p(X_{t})\\}_{t\geq 0}$ is a strong solution of

$\displaystyle Y_{t}=Y_{0}+\int_{0}^{t}\tilde{\sigma}(Y_{s})dW_{s};\hskip
10.0pt0\leq t<\infty,$ (46)

where

$\displaystyle p(-\infty)<Y_{0}<p(\infty)\hskip 10.0pt\hskip 10.0pt\text{a.s.
},$
$\displaystyle\tilde{\sigma}(y)=\begin{cases}p^{\prime}(q(y))\sigma(q(y));&p(\infty)<y<p(\infty),\\\
0;&\text{otherwise}.\end{cases}$

######  Fact 41.

Let $(\Omega,\mathcal{F},\mathbb{P})$ be a probability space.

  1. (1)

In equation (46), the Brownian motion $\\{W_{t}\\}_{t\geq 0}$ is known to be a
_continuous local martingale_. The definition of a continuous local martingale
can be found in 1.5.15 of the reference [KS91]. Furthermore, the stochastic
integral $\\{\int_{0}^{t}\tilde{\sigma}(Y_{s})dW_{s}\\}_{t\geq 0}$ is also a
continuous local martingale, provided that the condition

$\displaystyle\mathbb{P}\left(\omega;\int_{0}^{t}\tilde{\sigma}^{2}(Y_{s}(\omega))ds<\infty\right)=1\quad\text{for
every }t\in[0,\infty)$

is satisfied. This fact is also mentioned in Section 3.2.D of [KS91].

  2. (2)

The stochastic process $\\{\int_{0}^{t}\tilde{\sigma}^{2}(Y_{s})ds\\}_{t\geq
0}$ is indeed referred to as the _quadratic variation_ of the continuous local
martingale $\\{\int_{0}^{t}\tilde{\sigma}(Y_{s})dW_{s}\\}_{t\geq 0}$. The
definition of quadratic variation can be found in 1.5.18 of the reference
[KS91]. This fact is also mentioned in Section 3.2.D of [KS91].

  3. (3)

Let $M:=\\{M_{t}\\}_{t\geq 0}$ be a continuous local martingale starting at
zero and $\langle M\rangle:=\\{\langle M\rangle_{t}\\}_{t\geq 0}$ be the
quadratic variation of $M$. Consider a probability space
$(\hat{\Omega},\hat{\mathcal{F}},\hat{\mathbb{P}})$ in which a Brownian motion
exists. According to the results in 3.4.6 and 3.4.7 of the reference [KS91],
there exists a Brownian motion $\tilde{B}:=\\{\tilde{B}_{t}\\}_{t\geq 0}$
defined on the probability space
$(\tilde{\Omega},\tilde{\mathcal{F}},\tilde{\mathbb{P}})=(\Omega\times\hat{\Omega},\mathcal{F}\otimes\hat{\mathcal{F}},\mathbb{P}\otimes\hat{\mathbb{P}})$
such that

$\displaystyle M_{t}(\omega)=B_{\langle
M\rangle_{t}}(\omega,\tilde{\omega})\quad\text{almost surely
}\tilde{\mathbb{P}}.$

This provides a representation of the continuous local martingale $M$ in terms
of the Brownian motion $\tilde{B}$.

The following lemma gives a representation of SDE (29) by time change of
Brownian motion.

######  Theorem 42.

Suppose that $\sigma:\mathbb{R}\rightarrow\mathbb{R}$ and
$b:\mathbb{R}\rightarrow\mathbb{R}$ satisfies Assumption 6. Then, a unique,
strong solution exists (29). Moreover, there exist

  * •

a probability space $(\hat{\Omega},\hat{\mathcal{F}},\hat{\mathbb{P}})$,

  * •

a Brownian motion $B$ and an nonnegative continuous strictly increasing
process$\\{Z_{t}\\}_{t\geq 0}$ with $Z_{0}=0$ on
$(\tilde{\Omega},\tilde{\mathcal{F}},\tilde{\mathbb{P}}):=(\Omega\times\hat{\Omega},\mathcal{F}\otimes\hat{\mathcal{F}},\mathbb{P}\otimes\hat{\mathbb{P}})$,
and

  * •

a strictly increasing continuous function $p:\mathbb{R}\rightarrow\mathbb{R}$

such that

$\displaystyle
X_{t}(\omega)=p^{-1}(p(\xi)+B_{Z_{t}}(\omega,\hat{\omega}))\hskip 10.0pt0\leq
t<\infty,$ (47)

a.s. $\tilde{\mathbb{P}}$. Here $\xi=X_{0}$ is the constant initial value of
the SDE (29).

######  Proof A.2.

The existence and uniqueness of the solution follow from Proposition A.1.
Since $\sigma$ and $b$ satisfy Assumption 6, we can deduce from Theorem A.1
that there exists a continuous injection $p:\mathbb{R}\rightarrow\mathbb{R}$
and a continuous function $\tilde{\sigma}:\mathbb{R}\rightarrow\mathbb{R}$
such that $\\{Y_{t}(\omega)\\}_{t\geq 0}=\\{p(X_{t}(\omega))\\}_{t\geq 0}$ is
a strong solution of the SDE (46). From the Definition 3.4 of the strong
solution,
$\mathbb{P}[\int_{0}^{t}\tilde{\sigma}^{2}(Y_{s}(\omega))ds<\infty]=1$ for
every $t$. Then, by (i) of Fact 41, we know that $Y_{t}(\omega)-Y_{0}(\omega)$
is a continuous local martingale starting at zero. From (ii) of Fact 41, the
quadratic variation $\langle Y\rangle$ of $Y$ is given by
$\\{\int_{0}^{t}\tilde{\sigma}^{2}(Y_{s})ds\\}_{t\geq 0}$. Moreover, from the
definition $Y_{t}(\omega)=p(X_{t}(\omega))$ and the construction of
$\tilde{\sigma}$ in (46), we have $\tilde{\sigma}^{2}(Y_{t}(\omega))>0$ for
every $t\in[0,\infty)$. Therefore, $t\mapsto\langle Y\rangle_{t}(\omega)$ is
strictly increasing almost surely. Now, by (iii) of Fact 41, there exists a
probability space $(\hat{\Omega},\hat{\mathcal{F}},\hat{\mathbb{P}})$ such
that there exists a Brownian motion $B$ on
$(\tilde{\Omega},\tilde{\mathcal{F}},\tilde{\mathbb{P}})=(\Omega\times\hat{\Omega},\mathcal{F}\otimes\hat{\mathcal{F}},\mathbb{P}\otimes\hat{\mathbb{P}})$
such that

$\displaystyle Y_{t}(\omega)=Y_{0}(\omega)+B_{\langle
Y\rangle_{t}}(\omega,\hat{\omega})\quad\text{almost surely on
}\tilde{\mathbb{P}}.$

We obtain the desired result by setting $Z_{t}:=\langle Y\rangle_{t}$.

######  Proof A.3 (Proof of Lemma 27).

From Theorem 42, we have
$X_{t}(\omega)=p^{-1}(p(\xi)+B_{Z_{t}}(\omega,\hat{\omega}))$ for all
$t\in[0,\infty)$ almost surely in the extended probability space
$(\tilde{\Omega},\tilde{\mathcal{F}},\tilde{\mathbb{P}})=(\Omega\times\hat{\Omega},\mathcal{F}\otimes\hat{\mathcal{F}},\mathbb{P}\otimes\hat{\mathbb{P}})$,