Online Monitoring of MTL using Sequential NetworksDogan Ulus

# Online Monitoring of Metric Temporal Logic
using Sequential Networks

Dogan Ulus Boston University, Boston, MA, U.S.A.

###### Abstract

Metric Temporal Logic (MTL) is a popular formalism to specify patterns with
timing constraints over the behavior of cyber-physical systems. In this paper,
I propose sequential networks for online monitoring applications and construct
network-based monitors from the past fragment of MTL over discrete and dense
time behaviors. This class of monitors is more compositional, extensible, and
easily implementable than other monitors based on rewriting and automata. I
first explain the sequential network construction over discrete time behaviors
and then extend it towards dense time by adopting a point-free approach. The
formulation for dense time behaviors and MTL radically differs from the
traditional pointy definitions and, in return, we avoid some longstanding
complications. I argue that the point-free approach is more natural and
practical therefore should be preferred for the dense time. Finally, I present
my implementation together with some experimental results that show the
performance of the network-based monitors compared to similar existing tools.

##  1 Introduction

Monitoring temporal behaviors of systems during their actual execution has
important application areas ranging from runtime verification and anomaly
detection to supervisory control. It is desirable to construct such online
monitors automatically from high-level specifications of temporal patterns.
Originally proposed for formal verification, the formalism of Linear Temporal
Logic (LTL) [17] and its timed extensions such as Metric Temporal Logic (MTL)
[12] are very popular to specify various temporal patterns to be monitored. In
this paper, I propose online monitors based on sequential networks and study
their construction from the past fragment of MTL over discrete and dense time
behaviors.

A sequential network is an abstract machine defined by a finite state space, a
set of update rules for each state variable, and an output function. It
operates by reading a sequence (temporal behavior) left-to right (past-to-
future), updates its state variables according to some certain equations, and
yields an output value at each step. Hence, it is easy to view sequential
networks as an analogue of dynamical systems in theoretical computer science.
Sequential networks are functionally equivalent to finite automata but they
differ in the structure. Such seemingly subtle difference brings significant
advantages for sequential networks in terms of compositionality,
extensibility, and implementability. Therefore, sequential networks constitute
a very solid foundation to meet various types of monitoring needs in practice.

Sequential networks in this paper are directly constructed from the past
fragment of temporal logic specifications. The restriction to the past
temporal operators is twofold: (1) Future-oriented (acausal) monitoring is
inherently more expensive than past-oriented (causal) monitoring. The worst-
case exponential cost of bookkeeping all possibilities in the future cannot be
avoided unless the output at $t$ is delayed by some amount $d$ depending on
the formula. (2) However, the practical value of delaying seems nonexistent
for a truly online/reactive setting as we need an output from the monitor at
the current time $t$ rather than the time $t+d$, which may be too late. This
is especially important when the monitor’s output is used to take a timely
decision as in the supervisory control systems. Moreover, a monitor that
frequently returns _unknown_ or _pending_ as answers is not helpful in such
applications. Therefore, I consider future temporal operators as a costly
feature without much practical benefit in online monitoring applications.

The essence of the sequential network construction from temporal logic
formulas is to associate each subformula with a state variable to store the
relevant information and then manipulate them using a suitable algebra. Here I
will start from the online monitor construction explained in [10] where
authors essentially construct Boolean sequential networks from past LTL
formulas. For monitoring temporal patterns with timing constraints, the
Boolean algebra alone would no longer suffice in sequential networks unlike
the case of untimed patterns. Therefore, sequential networks to monitor MTL
formulas over discrete and dense time behaviors needs to store numerical
timing information. The technique in this paper differs from similar works [4]
as sets of past time points/periods are not explicitly stored from where
timing constraints will be measured. Instead the technique stores and
manipulates sets of future time points/periods affected by temporal operators
based on an observation [13] for offline MTL monitoring. Furthermore I
emphasize sequential networks as the model of computation for monitoring
tasks. This approach provides further connections with the theory of automata
and some related theoretical results. Effectiveness of these techniques then
would come no surprise for anyone despite their simplicity.

The other contribution of this paper is in introducing an alternative (point-
free) dense time formulation for MTL based on time periods rather than time
points. My motivation is that a number of (ancient and modern) complications
arises when we extend the discrete time setting towards the dense time if
dense timeline has been considered to be an infinite collection (continuum) of
time points. It is known that these mathematical complications simply
disappear once the traditional pointy definition of timeline has been
abandoned. Recently a number of works has proposed a point-free approach to
monitor timed regular expressions and interval logic [19, 20], which are based
on time periods by definition. Following these works, the question whether an
inherently pointy temporal logic such as MTL can be defined and monitored
effectively without points becomes interesting. In this paper, a positive
answer is given for this question with necessary foundations to have a natural
and practical dense time monitoring of MTL without longstanding complications
of the continuum and ever-increasing number of patches to fix them.

The structure of the paper is as follows. I first give the necessary
background and definitions in Section 2. Sequential networks constructions
from Past LTL and MTL specifications over discrete time behaviors is explained
with examples in Section 3. This section also serves as a preparation for
dense time constructions given in Section 4. Then a new point-free dense time
setting is formalized at the end of Section 4. My implementation and its
evaluation results are presented in Section 5 before the conclusions.

##  2 Preliminary Definitions

#### Boolean Temporal Behaviors

Let $P=\\{p_{1},\dots,p_{m}\\}$ be a finite set of propositions that
correspond to some qualitative states and activities of some real-time systems
and the environment. We consider such propositions to be observed
incrementally for an indefinite amount of time. Then a Boolean temporal
behavior refers to the history of such observations over either discrete or
dense timeline. More precisely, we first define an alphabet
$\Sigma=\mathbb{B}^{m}$ of observations expressed as Boolean vectors of
dimension $m$ where $\mathbb{B}=\\{\textsc{f},\textsc{t}\\}$. Then discrete
time behaviors are defined to be functions from integers to Boolean vectors
and dense time behaviors from a dense time domain to Boolean vectors.

#### Past Linear-time Temporal Logic

Past Linear-time Temporal Logic (past LTL) extends the propositional logic
with the _previously_ ($\newmoon$) and _since_ ($\mathcal{S}$) operators.
Given a finite set $P$ of atomic propositions, the formulas of past LTL are
built using the following grammar:

$\varphi\ =\ \top\ |\ p\ |\ \neg\,\varphi\ |\ \varphi_{1}\vee\varphi_{2}\ |\
\newmoon\,\varphi\ |\ \varphi_{1}\,\mathcal{S}\,\varphi_{2}$

The satisfaction relation $(w,t)\vdash\varphi$ of past LTL indicates that the
discrete-time behavior $w$ satisfies $\varphi$ at the time point $t$.

$\begin{array}[]{rlcl}(w,t)&\vdash p&\ \leftrightarrow&w_{p}(t)=\top\\\
(w,t)&\vdash\neg\,\varphi&\ \leftrightarrow&(w,t)\nvdash\varphi\\\
(w,t)&\vdash\varphi_{1}\vee\varphi_{2}&\
\leftrightarrow&(w,t)\vdash\varphi_{1}\text{ or }(w,t)\vdash\varphi_{2}\\\
(w,t)&\vdash\newmoon\,\varphi&\ \leftrightarrow&(w,t-1)\vdash\varphi\\\
(w,t)&\vdash\varphi_{1}\ \mathcal{S}\ \varphi_{2}&\ \leftrightarrow&\exists
t^{\prime}\in(0,t].\ (w,t^{\prime})\vdash\varphi_{2}\text{ and }\\\
&&&\quad\forall t^{\prime\prime}\in(t^{\prime},t].\
(w,t^{\prime\prime})\vdash\varphi_{1}\end{array}$

Other popular temporal operators _past eventually_ ($\blacklozenge$) and _past
always_ ($\blacksquare$) can be obtained from the since operator using
equivalences $\blacklozenge\varphi\equiv\top\mathcal{S}\varphi$ and
$\blacksquare\varphi\equiv\neg\blacklozenge\neg\varphi$.

#### Past Metric Temporal Logic

Past Metric Temporal Logic (past MTL) extends propositional logic with a time-
bounded (timed) variant of the _since_ modality, denoted by $\mathcal{S}_{I}$,
such that an interval $I$ of duration values additionally restricts the range
of quantification over time points. Given a finite set $P$ of atomic
propositions, the formulas of past MTL, when interpreted over discrete-time
behaviors, are defined by the following grammar:

$\varphi\ =\ \top\ |\ p\ |\ \neg\,\varphi\ |\ \varphi_{1}\vee\varphi_{2}\ |\
\varphi_{1}\,\mathcal{S}_{I}\,\varphi_{2}$

where $p\in P$. Time-bounded _past eventually_ ($\blacklozenge_{I}$) and _past
always_ ($\blacksquare_{I}$) are derived as usual. For any temporal operator,
I omit the time bound $I$ if $I=[0,\infty)$ and call such a operator untimed.
The traditional satisfaction relation $(w,t)\vdash\varphi$ indicates that the
sequence $w$ satisfies the formula $\varphi$ at time point $t>0$ as follows.

$\begin{array}[]{rlcl}(w,t)&\vdash p&\ \leftrightarrow&w_{p}(t)=\top\\\
(w,t)&\vdash\neg\,\varphi&\ \leftrightarrow&(w,t)\nvdash\varphi\\\
(w,t)&\vdash\varphi_{1}\vee\varphi_{2}&\
\leftrightarrow&(w,t)\vdash\varphi_{1}\text{ or }(w,t)\vdash\varphi_{2}\\\
(w,t)&\vdash\varphi_{1}\ \mathcal{S}_{I}\ \varphi_{2}&\
\leftrightarrow&\exists t^{\prime}\in(0,t).\
(w,t^{\prime})\vdash\varphi_{2}\text{ and }\\\ &&&\quad\forall
t^{\prime\prime}\in(t^{\prime},t).\
(w,t^{\prime\prime})\vdash\varphi_{1}\text{ and }\\\ &&&\quad\quad
t-t^{\prime}\in I\\\ \end{array}$

#### Sequential Networks

A sequential network is an abstract machine that computes an output sequence
$Y_{1}Y_{2}\dots Y_{k}\dots$ from an input sequence $X_{1}X_{2}\dots
X_{k}\dots$. At any time step $k$, a sequential network is in a state, denoted
by $V_{k}$, given by the values of its state variables. The network operates
by updating its state $V_{k}$ and yielding the current output $Y_{k}$ with
respect to the previous state $V_{k-1}$ and the current input $X_{k}$. We then
completely characterize a sequential network by the following elements:

  * •

The initial valuation vector $V_{0}$ of $m$ state variables

  * •

Update equations $V_{k}(i)=F_{i}(V_{k-1},X_{k})$ for $i=1,\dots,m$

  * •

The output function $Y(V_{k-1},X_{k})$ of the network

$V_{0}$$V_{1}$$V_{2}$$\dots$$V_{k}$$X_{1}$$X_{2}$$\dots$$X_{k}$$Y_{1}$$Y_{2}$$\dots$$Y_{k}$
Figure 1: Computation in sequential networks.

Figure 1 illustrates the model of computation employed in sequential networks.
Easily seen that we only need to maintain a fixed set of state variables
during a run of the network and the number of updates linearly depends on the
number of state variables and the length of the input. We can usually afford
update functions that are expensive in terms of complexity as long as their
complexities do not depend on the length of the input (or depends on
logarithmically at most). Actual data types of inputs, outputs, and state
variables of the network vary across applications. The simplest class of
sequential networks, in which all data types are Booleans, is called Boolean
sequential networks or digital sequential circuits when realized using Boolean
logic gates and memory elements such as flip-flops. The class of Boolean
sequential networks precisely recognizes regular languages and thus
functionally equivalent to finite automata [6]. However, there are a few key
differences between automata and networks regarding the direction of updates
explained as follows. While the transition function of an automaton computes
the next reachable states from a state (one-to-many), an update rule of a
sequential network computes whether a state is reachable from previous states
(many-to-one). I refer to the study [5] for some theoretical results regarding
this reverse relation between automata and Boolean sequential networks.

Finally, update equations and the output function in sequential networks are
given as functions of previous valuations $V_{k-1}$ of state variables in the
strict sense. However, in this paper, I allow so-called transient state
variables to ease the forthcoming constructions. These transient state
variables store intermediate results of update computations and depend on
current valuations $V_{k}$. If desired, such states can be eliminated by
embedding their update equations into the rest as a small optimization
attempt.

##  3 Discrete Time

In this section, I explain sequential network constructions over the discrete
time behaviors from past LTL and MTL specifications. In discrete setting, a
fixed set of propositions is observed at each discrete time point and we feed
the network with the corresponding Boolean vector. For the case of MTL, we
additionally assume a counter that keeps track of the integer time (sequence
index) and use integers to specify timing constraints accordingly.

###  3.1 Sequential Networks from Past LTL

The monitor construction presented here from past LTL is very similar to the
one in [10] introduced under the broad name of dynamic programming. Here I
show that this algorithm essentially constructs Boolean sequential networks
from past LTL specifications. Although it is mostly a change in terminology, I
emphasize some elements that are trivial for past LTL monitors (such as output
functions) as a preparation for timed generalizations in the following.

Monitor construction from a past LTL formula starts by associating each
subformula with a Boolean state variable initially set to false. Update
equations for the Boolean state variables are defined according to their
operators as given in the list below:

$\begin{array}[]{rcl}V_{k}(p)&=&X_{k}(p)=\begin{cases}1&\text{if }p\text{
holds at }k\\\ 0&\text{otherwise.}\end{cases}\\\ \\\ V_{k}(\neg\varphi)&=&\neg
V_{k}(\varphi)\\\ V_{k}(\varphi_{1}\vee\varphi_{2})&=&V_{k}(\varphi_{1})\vee
V_{k}(\varphi_{2})\\\ V_{k}(\newmoon\,\varphi)&=&V_{k-1}(\varphi)\\\
V_{k}(\varphi_{1}\mathcal{S}\varphi_{2})&=&V_{k}(\varphi_{2})\ \vee\
\big{(}V_{k}(\varphi_{1})\wedge\
V_{k-1}(\varphi_{1}\mathcal{S}\varphi_{2})\big{)}\end{array}$

We then obtain update equations for other temporal operators using their
definitions in terms of the since operator as follows.

$\begin{array}[]{rcl}V_{k}(\blacklozenge\,\varphi)&=&V_{k}(\varphi)\vee
V_{k-1}(\blacklozenge\,\varphi)\\\
V_{k}(\blacksquare\,\varphi)&=&V_{k}(\varphi)\wedge
V_{k-1}(\blacksquare\,\varphi)\end{array}$

The construction is completed by declaring the value of the top variable (the
original formula) as the output of the overall network.

We now illustrate the sequential network construction from past LTL with an
example. Consider a past LTL formula $\varphi=(p\vee q)\ \mathcal{S}\ \neg r$,
which contains three propositions and three subformulas. We then construct a
sequential network from $\varphi$, which has three inputs and three state
variables (all initialized to false) with update equations and output function
listed in Table 1. Letters in the leftmost column of the table denotes
datatype of variables where b stands for Boolean, which is the case for
untimed monitors over discrete time behaviors.

$\begin{array}[]{lrcl}\hline\cr\hline\cr\textsc{b}&V_{k}(\neg r)&=&\neg
X_{k}(r)\\\ \textsc{b}&V_{k}(p\vee q)&=&X_{k}(p)\vee X_{k}(q)\\\
\textsc{b}&V_{k}(\varphi)&=&V_{k}(\neg r)\ \vee\ \Big{(}V_{k}(p\vee q)\wedge
V_{k-1}(\varphi)\Big{)}\\\ \hline\cr\textsc{b}&Y_{k}&=&V_{k}(\varphi)\\\
\hline\cr\hline\cr\end{array}$ Table 1: Boolean sequential network constructed
from the formula $\varphi=(p\vee q)\ \mathcal{S}\ \neg r$.

Note that compositionality is an important feature of network based monitors.
Easily seen, we can construct the same sequential network from previously
constructed monitors of $(p\vee q)$ and $\neg r$. Given two monitors for past
LTL formulas $\varphi_{1}=(p\vee q)$ and $\varphi_{2}=\neg r$, we can obtain a
new monitor for $\varphi_{1}\ \mathcal{S}\ \varphi_{2}$ by joining state
variables from both monitors plus adding a new state variable for the
(topmost) since operator. Then, the outputs of $\varphi_{1}$ and $\varphi_{2}$
monitors become arguments of the update equation of the new state. In other
words, output equations of $\varphi_{1}$ and $\varphi_{2}$ are embedded into
the update equation of $\varphi_{1}\ \mathcal{S}\ \varphi_{2}$ at the
composition. Notice that output equations defined for past LTL are trivial,
which simply yield the value of the corresponding state variable. Therefore a
discussion of output equations can be ignored for past LTL constructions.
However, this is not the case for constructions from MTL as we see in the
following.

###  3.2 Sequential Networks from Past MTL

For monitoring timed specifications such as past MTL, we quantitatively reason
about time distances (durations) between events and states. For example,
consider the evaluation of a MTL formula
$\varphi=\varphi_{1}\mathcal{S}_{[a,b]}\varphi_{2}$ at the current time point
$k$. According to the semantics, we need to check distances between $k$ and
time points where $\varphi_{2}$ hold in the past whether they satisfy the
specified timing constraint $[a,b]$. In other words, actual time points where
$\varphi_{2}$ hold in the past are important for the MTL evaluation and we
need to store relevant time points (thus a set of integers) during monitoring.
Compare this with the untimed case where the existence of such a time point
needs to be stored (thus a Boolean value). Therefore, in the following, I use
state variables that store sets of integers, called timed state variables, to
handle quantitative timing constraints. Unless explicitly stated, I consider
all timed state variables to be initialized to the empty set $\emptyset$. Then
it is sufficient to define update equations and the output function for each
timed temporal operator to manipulate such sets according to the semantics.
Note that Boolean and untimed temporal operators in MTL formulas can be
handled using Boolean state variables as if they are LTL formulas.

#### Timed Past Eventuality Operator

According to (discrete time) MTL semantics, the formula
$\varphi=\blacklozenge_{[a,b]}\ \psi$ holds at a time point $k$ if the
subformula $\psi$ holds for some time points in $[k-b,k-a]$. Equivalently,
whenever the formula $\psi$ holds at a time point $k$, the formula $\varphi$
will be true for all future time points in $[k+a,k+b]$. Using this simple
observation, called forward-shifting in [13], we first define a state variable
$V_{k}(\psi)\subseteq[k,\infty)$ for the formula
$\varphi=\blacklozenge_{[a,b]}\ \psi$ to store a set of integers. Intuitively,
the set $V_{k}(\blacklozenge_{[a,b]})$ corresponds to future time points at
which the formula $\blacklozenge_{[a,b]}$ will be held. Therefore, we first
define the update equation for $V_{k}(\varphi)$ as follows.

$\centering
V_{k}(\blacklozenge_{[a,b]}\psi)=\begin{cases}V_{k-1}(\blacklozenge_{[a,b]}\psi)\cup[k+a,k+b]&\text{if
}Y_{k}(\psi)\\\
V_{k-1}(\blacklozenge_{[a,b]}\psi)&\text{otherwise.}\end{cases}\@add@centering$

where the function $Y_{k}(\psi)$ denotes the output equation of the network
constructed for $\psi$. Note that ensuring the condition
$V_{k}\subseteq[k,\infty)$ is important to bound the size of the set
$V_{k}(\varphi)$. Hence, we also apply the intersection
$V_{k}(\varphi)\cap[k,\infty)$ at each update. For brevity, I omit this
intersection operation in all the following update equations.

It is easy to see that the current time point $k$ must be in
$V_{k}(\blacklozenge_{[a,b]}\psi)$ by definition if the formula
$\blacklozenge_{[a,b]}\psi$ holds at $k$. Therefore, I define the output
function $Y_{k}(\blacklozenge_{[a,b]}\psi)$ to be a membership test as
follows.

$\centering Y_{k}(\blacklozenge_{[a,b]}\psi)=k\in
V_{k}(\blacklozenge_{[a,b]}\psi)\@add@centering$

We now illustrate the sequential network construction from a past MTL formula
$\varphi=\blacklozenge_{[1,2]}\blacklozenge_{[1,2]}(p\vee q)$, which possesses
(non-propositional) subformulas $(1):p\vee q$,
$(2):\blacklozenge_{[1,2]}(p\vee q)$, and
$(3):\blacklozenge_{[1,2]}\blacklozenge_{[1,2]}(p\vee q)$. Accordingly we have
three state variables in the network, one Boolean and two timed, as shown in
Table 2 with update equations and the output function. Notice that the output
function $k\in V_{k}(2)$ of $\blacklozenge_{[1,2]}(p\vee q)$ is embedded into
the update equation of $V_{k}(3)$ at the composition.

$\centering\begin{array}[]{lrcl}\hline\cr\hline\cr\textsc{b}&V_{k}(1)&=&X_{k}(p)\vee
X_{k}(q)\\\
\textsc{t}&V_{k}(2)&=&\begin{cases}V_{k-1}(2)\cup[k+1,k+2]&\text{if
}V_{k}(1)\\\ V_{k-1}(2)&\text{otherwise.}\end{cases}\\\
\textsc{t}&V_{k}(3)&=&\begin{cases}V_{k-1}(3)\cup[k+1,k+2]&\text{if }k\in
V_{k}(2)\\\ V_{k-1}(3)&\text{otherwise.}\end{cases}\\\
\hline\cr\textsc{b}&Y_{k}(\varphi)&=&k\in V_{k}(3)\\\
\hline\cr\hline\cr\end{array}\@add@centering$ Table 2: Sequential network
constructed from the formula
$\varphi=\blacklozenge_{[1,2]}\blacklozenge_{[1,2]}(p\vee q)$.
$\begin{array}[]{rcccccccc}\hline\cr\hline\cr k:&0&1&2&3&4&5&6\\\ \hline\cr
p:&&\textsc{t}&\textsc{f}&\textsc{f}&\textsc{f}&\textsc{f}&\textsc{f}\\\
q:&&\textsc{f}&\textsc{f}&\textsc{f}&\textsc{f}&\textsc{t}&\textsc{f}\\\
\hline\cr
V_{\varphi}(1):&\textsc{f}&\textsc{t}&\textsc{f}&\textsc{f}&\textsc{f}&\textsc{t}&\textsc{f}\\\
V_{\varphi}(2):&\emptyset&[2,3]&[2,3]&\\{3\\}&\emptyset&[6,7]&[6,7]\\\
V_{\varphi}(3):&\emptyset&\emptyset&[3,4]&[3,5]&[4,5]&\\{5\\}&[7,8]\\\
\hline\cr
Y_{\varphi}:&&\textsc{f}&\textsc{f}&\textsc{t}&\textsc{t}&\textsc{t}&\textsc{f}\\\
\hline\cr\hline\cr\end{array}$ Table 3: A run of the network in Table 2.

In Table 3, we depict a discrete time behavior from the index $k=0$ to $k=6$
over the propositions $p$ and $q$ by listing on separate lines. The next three
lines below denotes the valuation of state variables and the final line
denotes the output of the sequential network. I note that the formula
$\blacklozenge_{[1,2]}\blacklozenge_{[1,2]}(p\vee q)$ is equivalent to a
simpler formula of $\blacklozenge_{[2,4]}(p\vee q)$. Such equivalences and
rewrites can be used to optimize the sequential network construction but it is
important for us to have a robust construction not depending on these
optimizations.

Finally a key point of the construction is in representing sets of integers by
symbolic means, that is to say, as a union of intervals. By this way, large
numbers (and infinity) that may appear in timing constraints can be handled
efficiently. Set operations between an interval and union of intervals (as we
need in the update equations) and membership tests can be performed in
(amortized) logarithmic time. The worst case space requirement can be observed
for the formula $\blacklozenge_{[b,b]}\psi$ where $b$ is a finite number and
$\psi$ holds at every other time point. In this case, we need to store $b/2$
singleton intervals (time points) in $V_{k}(\blacklozenge_{[b,b]}\psi)$.

#### Timed Past Always Operator

The formula $\varphi=\blacksquare_{[a,b]}\ \psi$ holds at a time point $t$ if
the subformula $\psi$ holds for all time points in $[t-b,t-a]$. We can obtain
the update equation

$V_{k}(\varphi)=\begin{cases}V_{k-1}(\varphi)\cup[k+a,k+b]&\text{if not
}Y_{k}(\psi)\\\ V_{k-1}(\varphi)&\text{otherwise.}\end{cases}$

and the output equation

$Y_{k}(\varphi)=k\notin V_{k}(\varphi)$

from the case of timed past eventuality operator as usual. We illustrate an
example run of the sequential network constructed from the formula
$\varphi=\blacksquare_{[1,2]}\psi$ in Table 4.

$\begin{array}[]{rcccccccc}\hline\cr\hline\cr k:&0&1&2&3&4&5&6\\\ \hline\cr
Y_{\psi}:&&\textsc{f}&\textsc{f}&\textsc{t}&\textsc{t}&\textsc{t}&\textsc{f}\\\
\hline\cr V(\varphi):&\emptyset&[2,3]&[2,4]&[3,4]&\\{4\\}&\emptyset&[7,8]\\\
\hline\cr
Y_{\varphi}:&&\textsc{t}&\textsc{f}&\textsc{f}&\textsc{f}&\textsc{t}&\textsc{t}\\\
\hline\cr\hline\cr\end{array}$ Table 4: A run of the network for
$\varphi=\blacksquare_{[1,2]}\psi$.

Notice that the network yields true for time point $1$ as there is no time
points before time point 1; therefore, it holds vacuously. This is the
standard behavior equivalent to the assumption that $\psi$ holds for all time
point before time point 1. Alternatively, we can invoke strong semantics of
the always operator and assume the formula $\psi$ does not hold before time
point 1. Under strong semantics, we simply set the initial valuation
$V_{0}=[0,b]$ where $b$ is the upper time bound $b$ for the operator.

#### Timed Since Operator

The formula $\psi_{1}\mathcal{S}_{[a,b]}\psi_{2}$ holds at a time point $t$ if
$\psi_{2}$ held at time point $t^{\prime}$ in the past between time points
$t-b$ and $t-a$, and $\psi_{1}$ has held continuously from $t^{\prime}$ to
$t$. Intuitively speaking, we can see these semantics as a conjunction of the
case of timed past eventuality as we forward-shift time points at which
$\varphi_{2}$ hold and the case where $\varphi_{1}$ continuously holds. It
means that we can store time point $V_{k}$ as if timed past eventuality while
$\varphi_{1}$ is holding. On the other hand, time points in the set $V_{k}$
becomes invalid whenever $\varphi_{1}$ ceases to hold therefore we need to
clear $V_{k}$. Based on these observations, I define the update equation of
the sequential network constructed for the formula
$\varphi=\psi_{1}\mathcal{S}_{[a,b]}\psi_{2}$ as follows.

$V_{k}(\varphi)=\begin{cases}V_{k-1}(\varphi)\cup[k+a,k+b]&\text{if
}Y_{k}(\psi_{1})\wedge Y_{k}(\psi_{2})\\\ [k+a,k+b]&\text{if }\neg
Y_{k}(\psi_{1})\wedge Y_{k}(\psi_{2})\\\ V_{k-1}(\varphi)&\text{if
}Y_{k}(\psi_{1})\wedge\neg Y_{k}(\psi_{2})\\\
\emptyset&\text{otherwise.}\end{cases}$

The output equation is similarly defined.

$Y_{k}(\varphi)=k\in V_{k}(\varphi)$

The Table 5 illustrates a run of the sequential network constructed from the
formula $\varphi=p\ \mathcal{S}_{[2,3]}\ q$.

$\begin{array}[]{rcccccccc}\hline\cr\hline\cr k:&0&1&2&3&4&5&6\\\ \hline\cr
p:&&\textsc{f}&\textsc{f}&\textsc{t}&\textsc{t}&\textsc{t}&\textsc{t}\\\
q:&&\textsc{f}&\textsc{t}&\textsc{f}&\textsc{f}&\textsc{t}&\textsc{f}\\\
\hline\cr
V(\varphi):&\emptyset&\emptyset&[4,5]&[4,5]&[4,5]&\\{5\\}\cup[7,8]&[7,8]\\\
\hline\cr
Y(\varphi):&&\textsc{f}&\textsc{f}&\textsc{f}&\textsc{t}&\textsc{t}&\textsc{f}\\\
\hline\cr\hline\cr\end{array}$ Table 5: A run of the sequential network
constructed for the MTL formula $p\ \mathcal{S}_{[2,3]}\ q$ over discrete time
behaviors of propositions $p$ and $q$.

##  4 Dense Time without Points

In this section, I explain sequential network constructions from past MTL
specifications over dense time behaviors. Under the hood, I propose an
alternative (point-free) dense-time formulation for MTL based on time periods
to replace the traditional formulation based on time points. My goal has been
to avoid longstanding complications of the traditional pointy model of time
and consequently obtain a more natural and practical MTL monitoring solution
over dense time behaviors without sacrificing formality.

Traditionally, dense timeline has been viewed as an infinite collection
(continuum) of time points having zero duration. This view is so rooted that
the resulting complications as well as patches to fix them are now thought to
be the fate of dense timeline. Here I focus on two of them we have been
experiencing in contemporary timed systems research. First, by the very
definition of the continuum, it is _possible_ to have a dense time behavior
that switches infinite number times in a finite amount of time. Since this is
very problematic in computer science regarding computability and complexity,
virtually all practical works assume a (finite variability) condition that
bounds the number of switchings or events in a finite amount of time. Here it
is beneficial to question why we have started with a clearly non-physical
assumption at the first place and then patched it with a physical restriction
everywhere else. I think, if such a non-physical assumption is an idealization
of physics (which is perfectly fine), then it simply should help solve our
problems rather than create them. At this point, readers are encouraged to
revise ancient complications [7] as well.

On the other hand, the second complication I want to show is much more
annoying. Consider an (untimed) MTL formula $\varphi=\psi_{1}\ \mathcal{S}\
\psi_{2}$ and its evaluation over pointy dense time behaviors of $\psi_{1}$
and $\psi_{2}$ depicted on the left and right of Figure 2. Although $\psi_{2}$
behaviors of both sides are the same everywhere except a single point, we
obtain a different result when monitoring the formula $\psi_{1}\ \mathcal{S}\
\psi_{2}$ according to the semantics of MTL. In other words, on the right of
the figure, the formula $\psi_{2}$ held _precisely zero duration more_ by
including the time point at the boundary and consequently the outcome of
monitoring has significantly altered. I argue that such an outcome totally
defies the quantitative reasoning we try to have about time by distinguishing
cases when there is no measurable difference even mathematically.

Note that it is also possible to patch this particular bug by restricting
pointy behaviors to be left-continuous functions, that is to say, functions
with no jumps when the limit point is approached from the left. Under the
finite variability condition and left-continuity, the behavior can be then
partitioned into a finite number of left-open and right-closed intervals. This
solution would work in practice but see that this is yet another patch for the
pointy model enforced externally. Patching after patching is never considered
to be a good sign for such a fundamental theory after all. Besides notice that
all these practical patches make the pointy model less pointy by introducing
certain aspects of the point-free model such as finiteness and uniform parts
of non-zero duration. Therefore I can say that the point-free model I am
proposing here naturally emerges from the practice. Now let us move to the
point-free proposal.

$\varphi_{1}$$\varphi_{2}$$\varphi_{1}\mathcal{S}\varphi_{2}$ |  |  $\varphi_{1}$$\varphi_{2}$$\varphi_{1}\mathcal{S}\varphi_{2}$
---|---|---
Figure 2: The outcome of monitoring $\varphi_{1}\mathcal{S}\varphi_{2}$
changes due to the formula $\varphi_{2}$ holds zero duration more on the
right.

A point-free approach for time starts from an undivided timeline as a whole
and assumes that it is the observer who divide it into parts during the
observation. Since we cannot observe physical processes with an infinite
precision and divide the dense timeline infinitely many times, we can only
have a finite number of parts having non-zero durations (time periods). Such a
view of time gives us a mathematical way to avoid Zeno’s paradoxes [7] as well
as our aforementioned complications. I, therefore, consider dense timeline to
be a finite sequence of time periods rather than an infinite collection of
time points in the following.

#### Point-free Behaviors

When we are describing temporal behaviors, it is natural to say, for example,
that a proposition $p$ is true for 4 seconds, then false for 2 seconds, then
true for 2 seconds, and then false for 1 seconds. Equivalently, we can say the
proposition is true from 0 to 4, false from 4 to 6, true from 6 to 8, and
false from 8 to 9 assuming a beginning time zero. As time progress, we can
observe further, divide the rest of the timeline, and say $p$ is false from 9
to 11, and continue. These descriptions do not explicitly refer to values of
individual time points but time periods. By point-free behaviors, I mean such
finite sequences of time periods furnished with observation values.

Formally a point-free dense-time Boolean behavior $w$ on a time period
$(t_{0},t_{n})$ is defined to be a finite sequence such that

$w=(t_{0},t_{1},b_{1}),(t_{1},t_{2},b_{2}),\dots,(t_{n-1},t_{n},b_{n})$

where $b_{k}$ is a Boolean value and $t_{k-1}<t_{k}$ for $k\in 1\dots n$. We
then write the example proposition $p$ as follows.

$p=(0,4,\textsc{t}),(4,6,\textsc{f}),(6,8,\textsc{t}),(8,9,\textsc{f})$

Notice that such representation is far from unique as we can divide any time
period arbitrarily and obtain equivalent behaviors. For example, the behavior
$p^{\prime}$ below is simply equivalent to the behavior $p$.

$p^{\prime}=(0,2.5,\textsc{t}),(2.5,4,\textsc{t}),(4,6,\textsc{f}),(6,8,\textsc{t}),(8,9,\textsc{f})$

More often we use the other direction and merge _stuttering_ periods, that is
successive time periods that have the same value, into one.

By the span of a behavior I mean the total time period it occupies on the
timeline. For example, the behavior $p$ has a span of $(0,9)$. Once the span
of a behavior is clear in the context, I drop periods of false from its
representation and write periods of true in a set. For example, we can
represent the behavior $p$ as a set $\\{(0,4),(6,8)\\}$ with a span of
$(0,9)$.

One practical benefit of the point-free approach is that we now have a single
type of time periods in sequences. Compare it with the fact that pointy
behaviors (partitioned into a finite sequence of intervals under the finite
variability condition) require four types of intervals (open, closed, and
half-opens) in sequences, which means more resources and effort for
implementation and testing.

#### Boolean Operations

I first explain Boolean operations over point-free behaviors. For example,
consider two point-free behaviors of propositions $p_{1}$ and $p_{2}$ spanning
over a time period $(0,20)$.

$\begin{array}[]{rcl}p&=&\\{(2,4),(7,10),(11,17)\\}\\\
q&=&\\{(3,8),(14,15)\\}\end{array}$

Informally speaking, a Boolean operation over point-free behaviors amounts to
synchronizing two behaviors (by dividing them accordingly), apply the usual
Boolean operation over values, and merge stuttering periods. The following
illustrates the results of some Boolean operations over behaviors $p$ and $q$.

$\begin{array}[]{rcl}\sim p&=&\\{(0,2),(4,7),(10,11),(17,20)\\}\\\ p\sqcap
q&=&\\{(3,4),(7,8),(14,15)\\}\\\ p\sqcup q&=&\\{(2,10),(11,17)\\}\end{array}$

where operators $\sim$, $\sqcap$, and $\sqcup$ denote negation, conjunction,
and disjunction over point-free behaviors, respectively. Notice that we
compute the negation of a behavior with respect to its span unless specified
otherwise. These operations are very intuitive and I later formalize them in
the corresponding section.

For online monitoring, I assume we receive dense time behaviors one chunk at a
step, which is called the current chunk or $k$th chunk referring to the number
of steps so far. It does not mean that values of every proposition (and
formula) are necessarily constant in a chunk. The reason for this is that I
would like to stay faithful to the segmentation of the timeline given by the
input behavior for the output behavior. Then, in general, constant chunks
cannot be obtained in the presence of timed subformulas.

Next, similar to discrete time networks, I define state variables $V_{k}$ and
store point-free behaviors in state variables corresponding to subformulas of
the original formula. For the case of Boolean operators, update equations are
straightforward:

$\begin{array}[]{rcl}V_{k}(p)&=&p_{k}\\\ V_{k}(\neg\psi)&=&\sim V_{k}(\psi)\\\
V_{k}(\psi_{1}\wedge\psi_{2})&=&V_{k}(\psi_{1})\sqcap V_{k}(\psi_{2})\\\
V_{k}(\psi_{1}\vee\psi_{2})&=&V_{k}(\psi_{1})\sqcup V_{k}(\psi_{2})\\\
\end{array}$

where $p_{k}$ is the $k$th chunk of the behavior $p$ and all the valuations of
state variables for Boolean operators span over the $k$th chunk. Output
functions $Y_{k}(\varphi)=V_{k}(\varphi)$ are then trivially defined to be
equal to corresponding state variable.

#### Timed Since Operation

In the case of the timed since, it is more convenient to compute the operation
sequentially over time periods where both values of operands are constant. To
this end, I locally introduce a secondary (and local) index $l$ that indicates
the position of a time period in a chunk, in which the values of operands are
necessarily constant. Suppose we are processing the $k$th chunk that consists
of $n$ constant-valued time periods for the operands $Y_{k}(\varphi_{1})$ and
$Y_{k}(\varphi_{2})$ of the since operation for the formula
$\varphi_{1}\mathcal{S}_{(a,b)}\varphi_{2}$. Note that the number $n$ is
specific to this chunk and this formula and we do not use it to divide the
timeline for other operations in the network. I denote by $V_{k,l}$ the
valuation of $l$-th constant time period for the both operand in the $k$th
chunk and similarly by $Y_{k,l}$ the output of thereof for $l=1\dots n$. Then
I give update equations for the timed since operator
$\psi=\varphi_{1}\mathcal{S}_{(a,b)}\varphi_{2}$ as follows.

$V_{k,l}(\psi)=\begin{cases}V_{k,l-1}(\psi)\ \sqcup&\text{if
}y_{k,l}(\varphi_{1})\wedge y_{k,l}(\varphi_{2})\\\ \quad(t+a,\
t^{\prime}+b)\\\ (t^{\prime}+a,\ t^{\prime}+b)&\text{if }\neg
y_{k,l}(\varphi_{1})\wedge y_{k,l}(\varphi_{2})\\\ V_{k,l-1}(\psi)&\text{if
}y_{k,l}(\varphi_{1})\wedge\neg y_{k,l}(\varphi_{2})\\\
\emptyset&\text{otherwise.}\end{cases}$

where $y_{k,l}(\varphi)$ is the Boolean value for the constant time period
$Y_{k,l}(\varphi)$ and $V_{k,n}=V_{k+1,0}$. The output of each local step
equals to the conjunction of the valuation and the current local step as
follows.

$Y_{k,l}(\varphi)=V_{k,l}\ \sqcap\ \text{Span}(k,l)$

We then collectively yield the outcome $Y_{k}(\varphi)$ of the whole chunk $k$
as the disjunction of the outputs of local steps.

$Y_{k}(\varphi)=Y_{k,1}\sqcup Y_{k,2}\sqcup\dots\sqcup Y_{k,n}$

Yielding a collective output as above eliminates the fragmentation created by
the local synchronization and allows us to continue the computation toward
upper nodes seamlessly.

$\begin{array}[]{rcccccc}\hline\cr\hline\cr k:&\phantom{m}&1&2&3&4\\\
\hline\cr\\\ \text{Current:}\\\
\text{period}:&&(0,30)&(30,47)&(47,75)&(75,99)\\\ \\\ \hline\cr\\\
\varphi_{1}:&&\\{(7,30)\\}&\\{(30,35),(39,47)\\}&\\{(47,49),(63,75)\\}&\\{(75,99)\\}\\\
\varphi_{2}:&&\\{(3,8)\\}&\\{(38,39)\\}&\\{(70,75)\\}&\\{(75,89)\\}\\\ \\\
\hline\cr\\\ ||\phantom{|}:&&\begin{array}[]{rcc}&\varphi_{1}&\varphi_{2}\\\
(0,3):&\textsc{f}&\textsc{f}\\\ (3,7):&\textsc{f}&\textsc{t}\\\
(7,8):&\textsc{t}&\textsc{t}\\\
(7,30):&\textsc{t}&\textsc{f}\end{array}&\begin{array}[]{rcc}&\varphi_{1}&\varphi_{2}\\\
(30,35):&\textsc{t}&\textsc{f}\\\ (35,38):&\textsc{f}&\textsc{f}\\\
(38,39):&\textsc{f}&\textsc{t}\\\
(39,47):&\textsc{t}&\textsc{f}\end{array}&\begin{array}[]{rcc}&\varphi_{1}&\varphi_{2}\\\
(47,49):&\textsc{t}&\textsc{f}\\\ (49,63):&\textsc{f}&\textsc{f}\\\
(63,70):&\textsc{t}&\textsc{f}\\\
(70,75):&\textsc{t}&\textsc{t}\end{array}&\begin{array}[]{rcc}&\varphi_{1}&\varphi_{2}\\\
(75,89):&\textsc{t}&\textsc{t}\\\ (89,99):&\textsc{t}&\textsc{f}\end{array}\\\
\\\ \hline\cr\\\ V_{\psi}:&&\begin{array}[]{rc}1:&\emptyset\\\
2:&\\{(25,31)\\}\\\ 3:&\\{(25,32)\\}\\\
4:&\\{(25,32)\\}\end{array}&\begin{array}[]{rc}1:&\\{(30,32)\\}\\\
2:&\emptyset\\\ 3:&\\{(57,63)\\}\\\
4:&\\{(57,63)\\}\end{array}&\begin{array}[]{rc}1:&\emptyset\\\ 2:&\emptyset\\\
3:&\emptyset\\\
4:&\\{(88,99)\\}\end{array}&\begin{array}[]{rc}1:&\\{(88,113)\\}\\\
2:&\\{(89,113)\\}\end{array}\\\ \\\ \hline\cr\\\
Y_{\psi}:&&\\{(25,30)\\}&\\{(30,32)\\}&\emptyset&\\{(88,99)\\}\\\ \\\
\hline\cr\hline\cr\end{array}$ Table 6: A run of the network constructed for
the formula $\psi=\varphi_{1}\ \mathcal{S}_{(18,24)}\ \varphi_{2}$ over dense
time behaviors of $\varphi_{1}$ and $\varphi_{2}$.

In Table 6 we illustrate all these concepts and operations over dense time
behaviors of subformulas $\varphi_{1}$ and $\varphi_{2}$. Input behaviors in
the example are incrementally given in the form of 4 chunks and we locally
synchronize them before the timed since operation. This process may lead to
further divisions on the timeline in which both behaviors hold constant as
shown in the row denoted by $||$. For this example, chunks are divided into
four except the latest one, which is divided into two. Then we apply the
update rule in a sequential manner inside chunks and collectively yield the
output of each chunk before moving to the next chunk.

#### Logical Characterization of Point-free Operations

The traditional semantics of MTL over dense time is pointy, that is to say, it
assigns a truth value to each time point on the timeline for a given formula
and behavior. My goal here is to develop an alternative point-free semantics
for MTL by formalizing Boolean and temporal operations over point-free
behaviors intuitively explained in the previous sections. To this end, I
redefine MTL as a temporal logic of time periods, which rather assigns a truth
value to each _time period_ in a two dimensional temporal structure for given
a formula and a point-free behavior.

I start from a whole timeline, typically $(0,\infty)$, and denote the set of
all time periods over the timeline by $\Omega$. For convenience, I assume the
bounds of time periods and timing constraints are given as rational numbers in
the following. The set of all periods on which a proposition $p$ holds is
called the valuation set $\mathcal{V}(p)\subseteq\Omega$ of the proposition
$p$. Intuitively, if a proposition $p$ holds over a time period, then $p$
necessarily holds for every for all sub-periods thereof. This property is
called homogeneity and captured by the formula

(hom) $(t,t^{\prime})\in\mathcal{V}(p)\longleftrightarrow\forall
t<r<r^{\prime}<t^{\prime}.\ (r,r^{\prime})\in\mathcal{V}(p)$

For example, consider a point-free behavior $p=\\{(2,4),(6,9)\\}$, which means
the proposition $p$ holds from 2 to 4 and 6 to 9. Then this behavior formally
represents a valuation set $\mathcal{V}(p)=\\{(r,r^{\prime})\ |\ 2\leq
r<r^{\prime}\leq 4\text{ or }6\leq r<r^{\prime}\leq 9\\}$ that contains every
time period the proposition $p$ holds. In the following, I use point-free
behaviors and homogeneous valuation sets interchangeably.

Similar to other temporal formalisms, I formalize MTL inside a two dimensional
temporal structure $(\Omega,\mathcal{V})$ where $\Omega$ is the set of all
time periods and a valuation function $\mathcal{V}:P\rightarrow 2^{\Omega}$
from a set $P$ of propositions to their valuation sets. We say a temporal
structure is homogeneous if all propositions are homogeneous as we have in
this paper. Then the point-free semantics of MTL is defined as follows.

######  Definition 4.1 (Point-free Semantics of MTL).

The point-free satisfaction relation $\vDash$ of a past metric temporal logic
formula $\varphi$ in a homogeneous temporal structure $(\Omega,\mathcal{V})$,
relative to a time period $(t,t^{\prime})\in\Omega$ is defined as follows:

$\begin{array}[]{rlcl}(t,t^{\prime})&\vDash p&\
\leftrightarrow&(t,t^{\prime})\in\mathcal{V}(p)\\\
(t,t^{\prime})&\vDash\neg\,\varphi&\ \leftrightarrow&\forall
t<r<r^{\prime}<t.\ (r,r^{\prime})\nvDash\varphi\\\
(t,t^{\prime})&\vDash\varphi_{1}\wedge\varphi_{2}&\
\leftrightarrow&(t,t^{\prime})\vDash\varphi_{1}\text{ and
}(t,t^{\prime})\vDash\varphi_{2}\\\ (t,t^{\prime})&\vDash\varphi_{1}\
\mathcal{S}_{(a,b)}\ \varphi_{2}&\ \leftrightarrow&\forall
t<t^{\prime\prime}<t^{\prime}.\ \exists r<r^{\prime}<t^{\prime\prime}.\\\
&&&\quad(r,r^{\prime})\vDash\varphi_{2}\text{ and}\\\
&&&\quad(r^{\prime},t^{\prime\prime})\vDash\varphi_{1}\text{ and}\\\ &&&\quad
a<t^{\prime\prime}-r^{\prime}<b\\\ \end{array}$

It is clear how to extend these definitions to the other Boolean operators
$\vee$ and $\rightarrow$ using their definition in terms of $\wedge$ and
$\neg$ as well as to other past temporal operators $\blacklozenge_{(a,b)}$ and
$\blacksquare_{(a,b)}$ using their definition in terms of
$\mathcal{S}_{(a,b)}$. Using these definitions, I extend the valuation
function $\mathcal{V}$ from propositions to past MTL formulas such that
$\mathcal{V}(\varphi)=\\{(t,t^{\prime})\ |\ (t,t^{\prime})\vDash\varphi\\}$.
Then we have that the homogeneity property is preserved for valuation sets of
formulas.

######  Proposition 4.2.

For any past MTL formula $\varphi$ and point-free dense-time behavior $w$, the
valuation set $\mathcal{V}(\varphi)$ is homogeneous.

We now explain the point-free semantics with examples. For example, consider
the disjunction of two behaviors $p=\\{(3,4)\\}$ and $q=\\{(4,6)\\}$. We first
calculate the negated sets $\mathcal{V}(\neg p)=\\{(r,r^{\prime})\ |\ 0\leq
r<r^{\prime}\leq 3\text{ or }4\leq r<r^{\prime}\\}$ and $\mathcal{V}(\neg
q)=\\{(r,r^{\prime})\ |\ 0\leq r<r^{\prime}\leq 4\text{ or }6\leq
r<r^{\prime}\\}$ according to the point-free semantics. Then we apply the set
intersection to get $\mathcal{V}(\neg p\wedge\neg q)=\\{(r,r^{\prime})\ |\
0\leq r<r^{\prime}\leq 3\text{ or }6\leq r<r^{\prime}\\}$ and finally obtain
$\mathcal{V}(p\vee q)=\\{(r,r^{\prime})\ |\ 3\leq r<r^{\prime}\leq 6\\}$ by
negating again, which is equivalent to the desired behavior $p\vee
q=\\{(3,6)\\}$. Note that this calculation is for illustration purposes as we
already mentioned more efficient algorithms to concretely perform Boolean
operations over point-free behaviors. The point-free version of the since
operator holds on a time period $(t,t^{\prime})$ if there exists a time period
ending at $r^{\prime}$ that satisfies $\varphi_{2}$ and a time period that
satisfies $\varphi_{1}$ on $(r^{\prime},t^{\prime\prime})$ for all
$t<t^{\prime\prime}<t^{\prime}$. By the homogeneity property, $\varphi_{1}$
holds for all time periods $(r^{\prime},r^{\prime\prime})$ for
$r^{\prime}<r^{\prime\prime}<t^{\prime\prime}$; therefore, the semantics
fulfills the intuitive meaning of the Since operation.

In the following, we will study the relation between the traditional pointy
semantics and the point-free semantics. The foremost connection is that an MTL
formula $\varphi$ holds on a time period $(t,t^{\prime})$ if $\varphi$ holds
for all time points in $(t,t^{\prime})$ expressed as

(cont) $\forall t<t^{\prime\prime}<t^{\prime}.\ t^{\prime\prime}\vdash\varphi\
\rightarrow\ (t,t^{\prime})\vDash\varphi$

Observe that all four types of continuous intervals, namely $[t,t^{\prime}]$,
$[t,t^{\prime})$, $(t,t^{\prime}]$, and $(t,t^{\prime})$, are mapped to the
same time period $(t,t^{\prime})$. Then we can reduce any pointy dense time
behavior into a point-free one using this mapping. Clearly the implication
cont does not hold in the other direction as the point-free semantics ignores
(the value of singular) points, in particular, boundary points and removable
discontinuities.

It is observed that the pointy model of time becomes more well-behaving under
finite variability and left continuity restrictions. The finite variability is
a common restriction that limits the discussion to finitely representable
behaviors. The left continuity restriction over Boolean behaviors is captured
by the identity

(lc) $t^{\prime}\vdash\varphi\leftrightarrow\exists t<t^{\prime}.\ \forall
t<t^{\prime\prime}<t^{\prime}.\ t^{\prime\prime}\vdash\varphi$

that says that, for every time point $t^{\prime}$, there exist a time point
$t<t^{\prime}$ in the past and the value of all points in between are equal to
the value of $t^{\prime}$. Recall that the original assumption of the pointy
model is that every point is an isolated (individual) member of the timeline.
However, by assuming left continuity, we would actually contradict with the
pointy foundations and accept that (the satisfaction of) a time point is not
that isolated but depends on its (immediate) past. Therefore, we see this
restriction applied more in engineering and physics (with its classical
definition with limits) than computer science and mathematical literature.

The following result shows that this practice (restricting the point model
under variability and continuity) makes the pointy model essentially point-
free.

######  Theorem 4.3.

The pointy semantics ($\vdash_{\textsc{fv},\textsc{lc}}$) under finite
variability (fv) and left continuity (lc) conditions is equivalent to the
flattening of the point-free semantics ($\vDash$) onto the second (end)
component such that

$t^{\prime}\vdash_{\textsc{fv},\textsc{lc}}\ \varphi\ \ \leftrightarrow\ \
\exists t<t^{\prime}.\ (t,t^{\prime})\vDash\varphi$

######  Proof 4.4.

By induction on the formula structure and directly for each case. See Appendix
B.

In other words, we can obtain homogeneous point-free valuations from a
sequence of left-open and right closed intervals (as left continuity enforces)
and reconstruct them by projecting homogeneous valuations onto the second
axis.

Finally note that these results in this section can be easily extended to
include future temporal logic by using symmetric definitions (the until
instead of the since, right-continuity instead of left-continuity, etc.) if
desired.

##  5 Implementation and Evaluation

We have implemented my approach using code generation technique similar to
other works [10, 9]. For a given past MTL formula, the monitor construction
algorithm traverses the syntax tree of the formula and generates corresponding
state variables, updates equations, and the output function in a target
programming language, here C++, for each subformula. Since these are valid C++
statements, we encapsulate them in an ordinary C++ class having two methods,
namely update and output. The generated class corresponds to the sequential
network based monitor and it is the final output of my implementation. Note
that we employ Interval Container Library (ICL) distributed as a part of Boost
C++ Libraries for operations on sets of time periods in updates equations and
output functions. The next thing is to write a main application code that
instantiates the generated (monitor) class and repeatedly call its update and
output methods while reading the input. This part is currently not automated
but we provide an example main application file to read Comma Separated Values
(CSV) files, feed the monitor incrementally, and print the output. The monitor
class and the rest of application are then compiled using the standard g++
compiler with -O2 optimizations. In the following, we perform all tests on a
laptop with a 2.50GHz Intel Core i5-7200 processor and 8GB memory.

We first compare the discrete-time monitors, generated by my implementation
called Reelay, with two publicly available monitoring tools, namely MonPoly
and Aerial, that support online past MTL monitoring. Both tools use an event
(sample) based time model, which is equivalent to discrete model if we have an
event (sample) for each discrete point (See [4] for the details and
comparison). We check in the tests whether tools scale for large timing
constraints since we usually have to reason about slow and fast changing
processes together and the monitoring process should not be affected by
changing the base time unit (e.g. from seconds to milliseconds). We start the
comparison by a property

$\textsc{qpr}(a,b)=\blacksquare\big{(}(r\wedge\neg q\wedge\blacklozenge
q)\rightarrow(p\ \mathcal{S}_{[a,b]}\ q)\big{)}$

that intuitively says the proposition $p$ always holds between (the last
occurrence of) $q$ and $r$ for a duration in $[a,b]$. We depict the comparison
results in Table 7 where we see that MonPoly and Reelay can handle large
timing constraints very well whereas Aerial does not scale. In this case, we
are about 15 times faster than MonPoly but such difference is in the margin of
the implementation details including the choice of programming language (Ocaml
for MonPoly) and my explicit compilation strategy.

The second property $\textsc{pandq}(a,b)=p\ \mathcal{S}_{[a,b]}\ q$ checks a
specific condition such that the subformula $q$ occurs frequently
(continuously at the extreme) and the upper bound $b$ is large. For example,
we encounter such a scenario when a safety controller monitors a system under
oversampling and timing constraints are usually much larger than the sampling
period. We are then testing tools over an extreme input where $\varphi_{1}$
and $\varphi_{2}$ hold continuously. From Table 7, we see that this case
breaks MonPoly’s algorithm as it explicitly stores all occurrences of
$\varphi_{2}$ in the past time window bounded by $b$. On the other hand, the
monitor perform well and require a constant time as the time bound $b$ is
getting larger.

| Aerial | MonPoly | Reelay
---|---|---|---
qpr(3,6) | 1.613 | 1.857 | 0.121
qpr(30,60) | 5.761 | 1.734 | 0.106
qpr(300,600) | 69.29 | 1.734 | 0.102
pandq(1,6) | 1.353 | 2.725 | 0.363
pandq(1,60) | 5.553 | 7.426 | 0.364
pandq(1,600) | 65.72 | 61.59 | 0.364
delay(6) | 1.397 | 2.256 | 0.347
delay(60) | 5.488 | 4.186 | 1.553
delay(600) | 63.665 | 25.972 | 13.176
Table 7: Comparing the performance of tools for three temporal properties with
varying timing parameters over discrete time behaviors of length 1 million.

Next we try to break our monitors as well. As mentioned in Section 3, we have
a very specific worst-case condition that involves (1) a formula $p\
\mathcal{S}_{[a,b]}\ q$ with a very narrow and large timing constraint such
that $b-a\ll b$, and (2) an input behavior of $q$ with frequent short pulses.
This scenario is captured by our third property $\textsc{delay}(b)=p\
\mathcal{S}_{[a,b]}\ q$ over $p$ holds continuously and $q$ holds every other
time point. It is seen from Table 7 the monitoring time is linearly increasing
with respect to $b$ since we need to store $b/2$ number of (disjoint) periods
in the set $V_{k}$. For other cases, in particular for formulas with wider
timing bounds, the algorithm mostly needs to store large overlapping time
periods so we are able to merge them and keep the effective size of the set
small. Note that this scenario is also hard for Aerial and MonPoly.

Max. Length of Chunk ($\Delta$) | 10 | 100 | 1000
---|---|---|---
qpr(300,600) | 0.50x | 1.22x | 1.43x
pandq(1,600) | 2.39x | 5.55x | 6.50x
delay(600) | 0.18x | 0.18x | 0.18x
Table 8: Speed of dense monitors relative to discrete monitors under different
maximum chunk sizes.

Finally we test the dense time monitors in comparison with the discrete as
there is no publicly available tool for dense/continuous semantics to my
knowledge (despite some algorithms exist [4, 13]). Recall that we usually
observe continuous processes via fixed-step oversampling, which may lead to
long discrete behaviors with long stutters. Using discrete monitors is of
course a source of inefficiency in this case and dense time monitors can
process such chunks of stuttering periods at one step. In my experiments, we
cap the maximum length $\Delta$ of chunks. This means that a step of the dense
monitor would change between 1 and $\Delta$ time units depending on the length
of stuttering periods (whereas it is always 1 for the discrete). Other
advantages of dense monitors include that they can work with rational (or
floating) numbers and variable-step (asynchronous) sampling schemes.

There is an overhead of dense monitors (due to heavier Boolean operations and
synchronization of behaviors) but we illustrate in Table 8 that it pays off
while we are processing long stuttering behaviors. For example, we see the
dense monitor of pandq(1,600) is two times slower than the discrete one with
$\Delta=10$. However, it processes $22\%$ faster than the discrete for
$\Delta=100$, and $43\%$ faster for $\Delta=1000$. We also report that two
monitors have almost the same speed when the cap is 35 for this particular
example. It suggests that dense monitors can become more effective starting
from stuttering lengths as low as 35 —an oversampling ratio of 256 is common
in digital signal processing. The other two properties, pandq(1,600) and
delay(600), are outliers as the input behavior for the former always stutters
and for the latter never does. Then we first see the speed of monitoring for
pandq(1,600) is approaching to the speed of reading the CSV file. Second, the
overhead of dense monitors is visible in the case of delay(600) as there is no
stutters a dense monitor can exploit. Therefore, we conclude that discrete
monitors should be preferred for rapidly changing processes and dense time
monitors for slowly changing processes.

##  6 Related Work

The pioneering work [10] for monitoring proposes a simple technique to
construct online monitors from past LTL specifications. This construction has
been extended for timed and quantitative (data) properties in several
subsequent works [18, 3, 4, 9]. In terms of tools and implementation, this
branch (network-based monitors) is quite fruitful perhaps because of its
simplicity. Other approaches for online MTL monitoring include automata based
[14, 11], tester based [15], and the incremental marking procedures [13]. To
my knowledge, no implementations are available for these automata and tester
based monitors. The implementation of the incremental algorithm has been
reported to work only with an external simulator in [13] and is not available
in the current version [16].

From a semantic point of view, dense time monitoring algorithms are divided
into sample or event based [18, 3, 11] and interval based continuous [14, 15,
13] semantics. An extensive comparison of two sorts can be found in [4] with a
conclusion that interval-based semantics are more natural and sample-based are
more efficient. In this paper, I propose a point-free semantics for MTL as the
third sort with a claim that it is both natural and efficient. Finally, there
are other formalisms that can be regarded as point-free. These are timed
regular expressions under so-called signal semantics [2] and interval temporal
logics under strict semantics [8, 20], which excludes punctual intervals. I
use similar definitions and techniques with these works in my formalization
and a brief review of interval logics is included in Appendix A.

##  7 Conclusions

I have described how to construct online monitors based on sequential networks
from past metric temporal logic (MTL) specifications over discrete and dense
time behaviors. The proposed construction and monitors are simple,
compositional, extensible, and easily implementable. These properties are
especially important when online monitors are deployed in real-time systems
and used actively in a larger (control) system. My experiments demonstrated
that the proposed monitors can handle large time constraints over long
sequences more efficiently than similar existing tools. Contrary to the
commonly-held opinion that dense time is much harder to handle than discrete
time, the proposed dense time monitors are no more complicated than the
discrete time monitors. It is even showed that dense time monitors perform
better for so-called stuttering behaviors, which are usually obtained in
monitoring continuous processes and systems via sampling.

The theoretical contribution of this paper is the introduction of a point-free
semantics for MTL obtained by discarding durationless time points from the
formulation. In that I was mainly concerned with the physical grounding and
practicality, which the traditional pointy time model fails to provide.
Therefore, my focus in the paper was in showing the mathematical and practical
benefits of having a point-free model for dense time monitoring solutions. I
can easily say that, together with sequential networks, the simplicity of the
dense time monitors is due to such point-free model of time. I believe that
the point-free approach can be also beneficial in other research areas in
timed systems including verification and synthesis.

## Acknowledgments

This article is dedicated to the memory of Oded Maler. I am indebted to him
for many enlightening discussions and suggestions over the years of my
doctoral studies.

## References

  * [1] J. F. Allen, Maintaining knowledge about temporal intervals, Communications of the ACM, 26 (1983), pp. 832–843.
  * [2] E. Asarin, P. Caspi, and O. Maler, Timed regular expressions, Journal of the ACM, 49 (2002), pp. 172–206.
  * [3] D. Basin, F. Klaedtke, S. Müller, and E. Zălinescu, Monitoring metric first-order temporal properties, Journal of the ACM, 62 (2015), p. 15.
  * [4] D. Basin, F. Klaedtke, and E. Zălinescu, Algorithms for monitoring real-time properties, Acta Informatica, 55 (2018), pp. 309–338.
  * [5] J. A. Brzozowski and E. Leiss, On equations for regular languages, finite automata, and sequential networks, Theoretical Computer Science, 10 (1980), pp. 19–35.
  * [6] I. M. Copi, C. C. Elgot, and J. B. Wright, Realization of events by logical nets, Journal of the ACM, 5 (1958), pp. 181–196.
  * [7] B. Dowden, Zeno’s paradoxes, in The Internet Encyclopedia of Philosophy, ISSN 2161-0002.  Last Accessed: December 2018.
  * [8] J. Y. Halpern and Y. Shoham, A propositional modal logic of time intervals, Journal of the ACM, 38 (1991), pp. 935–962.
  * [9] K. Havelund, D. Peled, and D. Ulus, First-order temporal logic monitoring with BDDs, in Proceedings of the Conference on Formal Methods in Computer-Aided Design (FMCAD), 2017.
  * [10] K. Havelund and G. Roşu, Efficient monitoring of safety properties, International Journal on Software Tools for Technology Transfer, 6 (2004), pp. 158–173.
  * [11] H.-M. Ho, J. Ouaknine, and J. Worrell, Online monitoring of metric temporal logic, in International Conference on Runtime Verification, Springer, 2014, pp. 178–192.
  * [12] R. Koymans, Specifying real-time properties with metric temporal logic, Real-Time Systems, 2 (1990), pp. 255–299.
  * [13] O. Maler and D. Ničković, Monitoring properties of analog and mixed-signal circuits, International Journal on Software Tools for Technology Transfer, 15 (2013), pp. 247–268.
  * [14] O. Maler, D. Ničković, and A. Pnueli, Real time temporal logic: Past, present, future, in International Conference on Formal Modeling and Analysis of Timed Systems, Springer, 2005, pp. 2–16.
  * [15] O. Maler, D. Ničković, and A. Pnueli, From MITL to timed automata, in International Conference on Formal Modeling and Analysis of Timed Systems, Springer, 2006, pp. 274–289.
  * [16] D. Ničković, O. Lebeltel, O. Maler, T. Ferrère, and D. Ulus, AMT2.0: Qualitative and quantitative trace analysis with extended signal temporal logic, in Proceedings of the Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2018.
  * [17] A. Pnueli, The temporal logic of programs, in Proceedings of the Symposium on Foundations of Computer Science (FOCS), 1977, pp. 46–57.
  * [18] P. Thati and G. Roşu, Monitoring algorithms for metric temporal logic specifications, Electronic Notes in Theoretical Computer Science, 113 (2005), pp. 145–162.
  * [19] D. Ulus, T. Ferrère, E. Asarin, and O. Maler, Timed pattern matching, in Proceedings of the Conference on Formal Modeling and Analysis of Timed Systems (FORMATS), 2014, pp. 222–236.
  * [20] D. Ulus and O. Maler, Specifying timed patterns using temporal logic, in Proceedings of the Conference on Hybrid Systems: Computation and Control (HSCC), 2018.
  * [21] Y. Venema, Expressiveness and completeness of an interval tense logic, Notre Dame Journal of Formal Logic, 31 (1990), pp. 529–547.

##  Appendix A Temporal Logics of Time Periods

In this section we give the overview of temporal logics based on time periods
(rather than time points) and period-based temporal modalities used in these
logics. We then reveal their connection with our point-free semantics and, in
particular, we give equivalent definitions of the point-free MTL operators in
terms of period-based temporal modalities.

Considering time periods as primitive entities, Allen introduced thirteen
basic relations between two time periods to represent high-level temporal
knowledge in [1]. The set of so-called Allen’s relations between time periods
consists of relations _met-by_ ($A$), _begins_ ($B$), _ends_ ($E$), _during_
($D$), _overlaps_ ($O$), and _later_ ($L$) as well as their inverses and the
equality ($=$). Halpern and Shoham applied modal logic approach over time
periods in [8] and proposed a temporal logic (HS-logic) that features a
temporal modality for each relation above. It is shown that six certain
temporal modalities of the HS-logic can express others under strict semantics,
which excludes points. Other properties of HS-logic can be found in [21]. The
metric extension of hs logic, called Metric Compass Logic (MCL), is introduced
in [20] by the following grammar:

$\varphi\ =\ p\ |\ \overline{\varphi}\ |\ \varphi_{1}\cap\ \varphi_{2}\ |\
\langle X\rangle_{(a,b)}\ \varphi$

where $p\in P$ is a proposition,
$X\in\\{A,\overline{A},B,\overline{B},E,\overline{E}\\}$ is a relation between
time periods, and $(a,b)$ is a timing constraint for the modality. The
existential temporal modality $\langle X\rangle_{(a,b)}\ \varphi$ is the dual
of an universal temporal modality $[X]_{(a,b)}\ \varphi=\overline{\langle
X\rangle_{(a,b)}\ \overline{\varphi}}$ as usual. The satisfaction relation
$\vDash$ of an MCL formula $\varphi$ in a temporal structure
$(\Omega,\mathcal{V})$, relative to a time period $(t,t^{\prime})\in\Omega$ is
defined as follows:

$\begin{array}[]{rlcl}(t,t^{\prime})&\vDash p&\
\leftrightarrow&(t,t^{\prime})\in\mathcal{V}(p)\\\
(t,t^{\prime})&\vDash\overline{\varphi}&\
\leftrightarrow&(t,t^{\prime})\nvDash\varphi\\\
(t,t^{\prime})&\vDash\varphi_{1}\cap\varphi_{2}&\
\leftrightarrow&(t,t^{\prime})\vDash\varphi_{1}\text{ and
}(t,t^{\prime})\vDash\varphi_{2}\\\ \\\ (t,t^{\prime})&\vDash\langle
B\rangle_{(a,b)}\ \varphi&\ \leftrightarrow&\exists
t<t^{\prime\prime}<t^{\prime}.\ (t,t^{\prime\prime})\vDash\varphi\\\
&&&\quad\text{ and }a<t^{\prime}-t^{\prime\prime}<b\\\
(t,t^{\prime})&\vDash\langle\overline{B}\rangle_{(a,b)}\ \varphi&\
\leftrightarrow&\exists t^{\prime\prime}>t^{\prime}.\
(t,t^{\prime\prime})\vDash\varphi\\\ &&&\quad\text{ and
}a<t^{\prime\prime}-t^{\prime}<b\\\ (t,t^{\prime})&\vDash\langle
E\rangle_{(a,b)}\ \varphi&\ \leftrightarrow&\exists
t<t^{\prime\prime}<t^{\prime}.\ (t^{\prime\prime},t^{\prime})\vDash\varphi\\\
&&&\quad\text{ and }a<t^{\prime\prime}-t<b\\\
(t,t^{\prime})&\vDash\langle\overline{E}\rangle_{(a,b)}\ \varphi&\
\leftrightarrow&\exists t^{\prime\prime}<t.\
(t^{\prime\prime},t^{\prime})\vDash\varphi\\\ &&&\quad\text{ and
}a<t-t^{\prime\prime}<b\\\ (t,t^{\prime})&\vDash\langle A\rangle_{(a,b)}\
\varphi&\ \leftrightarrow&\exists t^{\prime\prime}>t^{\prime}.\
(t^{\prime},t^{\prime\prime})\vDash\varphi\\\ &&&\quad\text{ and
}a<t^{\prime\prime}-t^{\prime}<b\\\
(t,t^{\prime})&\vDash\langle\overline{A}\rangle_{(a,b)}\ \varphi&\
\leftrightarrow&\exists t^{\prime\prime}<t.\
(t^{\prime\prime},t)\vDash\varphi\\\ &&&\quad\text{ and
}a<t-t^{\prime\prime}<b\\\ \end{array}$

The following defines point-free MTL operators introduced in this paper using
MCL operators given in this section. Given the formulas $\varphi_{1}$ and
$\varphi_{2}$ satisfy the homogeneity, it is easy to check the equivalences

$\begin{array}[]{rcl}\neg\varphi_{1}&\equiv&[B][E]\ \overline{\varphi_{1}}\
\equiv\ [E][B]\ \overline{\varphi_{1}}\\\ \varphi_{1}\ \wedge\
\varphi_{2}&\equiv&\varphi_{1}\ \cap\ \varphi_{2}\\\ \varphi_{1}\
\mathcal{S}_{(a,b)}\ \varphi_{2}&\equiv&[B]\langle
E\cup\overline{E}\rangle\Big{(}\varphi_{1}\cap\langle\overline{A}\rangle_{(a,b)}\
\varphi_{2}\Big{)}\\\ \end{array}$

where $\langle E\cup\overline{E}\rangle\ \varphi\equiv\langle E\rangle\
\varphi\cup\langle\overline{E}\rangle\ \varphi$ .

##  Appendix B Proof of Theorem 4.3

Provided the left continuity condition (lc) such that

$t^{\prime}\vdash\varphi\leftrightarrow\exists t<t^{\prime}.\ \forall
t<t^{\prime\prime}<t^{\prime}.\ t^{\prime\prime}\vdash\varphi$

and finite variability (fv), the proof first proceeds by the induction of the
formula structure. The base case of propositions and Boolean operations are
straightforward. We prove

$t^{\prime}\vdash_{\textsc{fv},\textsc{lc}}\ \varphi_{1}\ \mathcal{S}\
\varphi_{2}\ \ \leftrightarrow\ \ \exists t<t^{\prime}.\
(t,t^{\prime})\vDash\varphi_{1}\ \mathcal{S}\ \varphi_{2}$

For the direction ($\rightarrow$), assume that the formula $\varphi_{1}\
\mathcal{S}\ \varphi_{2}$ holds at a time point $t^{\prime}$, then we directly
have the following steps:

$\begin{array}[]{rlr}(1)&\exists t<t^{\prime}.\ \forall
t<t^{\prime\prime}<t^{\prime}.\ t^{\prime\prime}\vdash\varphi_{1}\
\mathcal{S}\ \varphi_{2}&(\textsc{lc})\\\ (2)&\exists t<t^{\prime}.\ \forall
t^{\prime}<t^{\prime\prime}<t^{\prime}.&(\mathcal{S})\\\ &\quad\exists
r^{\prime}<t^{\prime\prime}.\ r^{\prime}\vdash\varphi_{2}\text{ and }\forall
r^{\prime}<r^{\prime\prime}<t^{\prime\prime}.\
r^{\prime\prime}\vdash\varphi_{1}\\\ (3)&\exists t<t^{\prime}.\ \forall
t^{\prime}<t^{\prime\prime}<t^{\prime}.&(\vDash)\\\ &\quad\exists
r^{\prime}<t^{\prime\prime}.\ \exists r<r^{\prime}.\
(r,r^{\prime})\vDash\varphi_{2}\text{ and
}(r^{\prime},t^{\prime\prime})\vDash\varphi_{1}\\\ (4)&\exists t<t^{\prime}.\
(t,t^{\prime})\vDash\varphi_{1}\ \mathcal{S}\ \varphi_{2}&(\mathcal{S})\\\
\end{array}$

For the other direction ($\leftarrow$), assume that the formula $\varphi_{1}\
\mathcal{S}\ \varphi_{2}$ holds on a a time period $(t,t^{\prime})$, then we
directly have the following steps:

$\begin{array}[]{rlr}(1)&\exists t<t^{\prime}.\ \forall
t<t^{\prime\prime}<t^{\prime}.\ \exists
r<r^{\prime}<t^{\prime\prime}.&(\mathcal{S})\\\
&\quad(r,r^{\prime})\vDash\varphi_{2}\text{ and
}(r^{\prime},t^{\prime\prime})\vDash\varphi_{1}\\\ (2)&\exists t<t^{\prime}.\
\forall t<t^{\prime\prime}<t^{\prime}.\ \exists
r<r^{\prime}<t^{\prime\prime}.&(\textsc{hom})\\\
&\quad(r,r^{\prime})\vDash\varphi_{2}\text{ and }\\\ &\quad\forall
r^{\prime}<r^{\prime\prime}<r^{\prime\prime\prime}<t^{\prime\prime}.\
(r^{\prime\prime},r^{\prime\prime\prime})\vDash\varphi_{1}\\\ (3)&\exists
t<t^{\prime}.\ \forall t<t^{\prime\prime}<t^{\prime}.\ \exists
r^{\prime}<t^{\prime\prime}.&\\\ &\quad\exists r<r^{\prime}.\
(r,r^{\prime})\vDash\varphi_{2}\text{ and }\\\ &\quad\forall
r^{\prime}<r^{\prime\prime\prime}<t^{\prime\prime}.\ \exists
r^{\prime\prime}.\
(r^{\prime\prime},r^{\prime\prime\prime})\vDash\varphi_{1}\\\ (4)&\exists
t<t^{\prime}.\ \forall t<t^{\prime\prime}<t^{\prime}.\
t^{\prime\prime}\vdash\varphi_{1}\ \mathcal{S}\ \varphi_{2}&(\mathcal{S})\\\
(5)&t^{\prime}\vdash\varphi_{1}\ \mathcal{S}\ \varphi_{2}&(\textsc{lc})\\\
\end{array}$

Hence, we obtain ($\leftrightarrow$).