Online Monitoring of Metric Temporal Logic using Sequential Networks

TL;DR

This paper introduces a scalable online monitoring framework for Metric Temporal Logic (MTL) using sequential networks, enabling efficient real-time verification of temporal properties in cyber-physical systems.

Contribution

It presents a novel method to construct sequential networks from MTL specifications, improving efficiency and scalability for online monitoring of discrete and dense time behaviors.

Findings

Demonstrates performance improvements over existing methods.

Shows scalability in handling complex MTL specifications.

Validates effectiveness through extensive testing and comparison.

Abstract

Metric Temporal Logic (MTL) is a popular formalism to specify temporal patterns with timing constraints over the behavior of cyber-physical systems with application areas ranging in property-based testing, robotics, optimization, and learning. This paper focuses on the unified construction of sequential networks from MTL specifications over discrete and dense time behaviors to provide an efficient and scalable online monitoring framework. Our core technique, future temporal marking, utilizes interval-based symbolic representations of future discrete and dense timelines. Building upon this, we develop efficient update and output functions for sequential network nodes for timed temporal operations. Finally, we extensively test and compare our proposed technique with existing approaches and runtime verification tools. Results highlight the performance and scalability advantages of our monitoring approach and sequential networks.

Tables

Table 1. Table 1: Boolean sequential network constructed from the formula φ = ( p ∨ q ) ​ 𝒮 ​ ¬ r 𝜑 𝑝 𝑞 𝒮 𝑟 \varphi=(p\vee q)\ \mathcal{S}\ \neg r .

Table 2. Table 2: Sequential network constructed from the formula φ = ◆ [ 1 , 2 ] ​ ◆ [ 1 , 2 ] ​ ( p ∨ q ) 𝜑 subscript ◆ 1 2 subscript ◆ 1 2 𝑝 𝑞 \varphi=\blacklozenge_{[1,2]}\blacklozenge_{[1,2]}(p\vee q) .

Table 3. Table 3: A run of the network in Table  2 .

Table 4. Table 4: A run of the network for φ = ■ [ 1 , 2 ] ​ ψ 𝜑 subscript ■ 1 2 𝜓 \varphi=\blacksquare_{[1,2]}\psi .

Table 5. Table 5: A run of the sequential network constructed for the MTL formula p ​ 𝒮 [ 2 , 3 ] ​ q 𝑝 subscript 𝒮 2 3 𝑞 p\ \mathcal{S}_{[2,3]}\ q over discrete time behaviors of propositions p 𝑝 p and q 𝑞 q .

Table 6. Table 6: A run of the network constructed for the formula ψ = φ 1 ​ 𝒮 ( 18 , 24 ) ​ φ 2 𝜓 subscript 𝜑 1 subscript 𝒮 18 24 subscript 𝜑 2 \psi=\varphi_{1}\ \mathcal{S}_{(18,24)}\ \varphi_{2} over dense time behaviors of φ 1 subscript 𝜑 1 \varphi_{1} and φ 2 subscript 𝜑 2 \varphi_{2} .

Table 7. Table 7: Comparing the performance of tools for three temporal properties with varying timing parameters over discrete time behaviors of length 1 million.

	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 8. Table 8: Speed of dense monitors relative to discrete monitors under different maximum chunk sizes.

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

Equations

$$\phi =\top |p|\neg \phi |{\phi }_1\vee {\phi }_2|\text{newmoon}\phi |{\phi }_1\mathcal{S}{\phi }_2$$

$$\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}$$

$$\phi =\top |p|\neg \phi |{\phi }_1\vee {\phi }_2|{\phi }_1{\mathcal{S}}_I{\phi }_2$$

$$\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}$$

$$\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}$$

$$\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}$$

$$\text{centering}{V}_k({⧫}_{[a,b]}\psi )=\{\begin{array}{ll}{V}_{k-1}({⧫}_{[a,b]}\psi )\cup [k+a,k+b]& \text{if }{Y}_k(\psi )\\ V_{k-1}({⧫}_{[a,b]}\psi )& \text{otherwise.}\end{array}\text{@add@centering}$$

$$\text{centering}{Y}_k({⧫}_{[a,b]}\psi )=k\in V_k({⧫}_{[a,b]}\psi )\text{@add@centering}$$

$$V_k(\phi )=\{\begin{array}{ll}{V}_{k-1}(\phi )\cup [k+a,k+b]& \text{if not }{Y}_k(\psi )\\ V_{k-1}(\phi )& \text{otherwise.}\end{array}$$

$$Y_k(\phi )=k\notin V_k(\phi )$$

$$V_k(\phi )=\{\begin{array}{ll}{V}_{k-1}(\phi )\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}(\phi )& \text{if }{Y}_k({\psi }_1)\wedge \neg Y_k({\psi }_2)\\ \varnothing & \text{otherwise.}\end{array}$$

$$Y_k(\phi )=k\in V_k(\phi )$$

$$w=(t_0,t_1,b_1),(t_1,t_2,b_2),\dots ,(t_{n-1},t_n,b_n)$$

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

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

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

$$\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}$$

$$\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}$$

$$V_{k,l}(\psi )=\{\begin{array}{ll}{V}_{k,l-1}(\psi )\bigsqcup & \text{if }{y}_{k,l}({\phi }_1)\wedge y_{k,l}({\phi }_2)\\ (t+a,t^{\prime }+b)& \\ (t^{\prime }+a,t^{\prime }+b)& \text{if }\neg y_{k,l}({\phi }_1)\wedge y_{k,l}({\phi }_2)\\ V_{k,l-1}(\psi )& \text{if }{y}_{k,l}({\phi }_1)\wedge \neg y_{k,l}({\phi }_2)\\ \varnothing & \text{otherwise.}\end{array}$$

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

$$Y_k(\phi )=Y_{k,1}\bigsqcup Y_{k,2}\bigsqcup \cdots \bigsqcup Y_{k,n}$$

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

$$\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}$$

$$\forall t<t^{\prime \prime }<t^{\prime }.t^{\prime \prime }⊢\phi \to (t,t^{\prime })\models \phi$$

$$t^{\prime }⊢\phi \leftrightarrow \exists t<t^{\prime }.\forall t<t^{\prime \prime }<t^{\prime }.t^{\prime \prime }⊢\phi$$

$$t^{\prime }{⊢}_{\text{textsc}fv,\text{textsc}lc}\phi \leftrightarrow \exists t<t^{\prime }.(t,t^{\prime })\models \phi$$

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

$$\phi =p|\overline{\phi }|{\phi }_1\cap {\phi }_2|⟨X{⟩}_{(a,b)}\phi$$

$$\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}$$

$$\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}$$

Full text

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:

[TABLE]

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

[TABLE]

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:

[TABLE]

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.

[TABLE]

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

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:

[TABLE]

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

[TABLE]

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.

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.

[TABLE]

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.

[TABLE]

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.

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

[TABLE]

and the output equation

[TABLE]

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.

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.

[TABLE]

The output equation is similarly defined.

[TABLE]

The Table 5 illustrates a run of the sequential network constructed from the formula $\varphi=p\ \mathcal{S}_{[2,3]}\ 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.

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

[TABLE]

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.

[TABLE]

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$.

[TABLE]

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)$.

[TABLE]

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$.

[TABLE]

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:

[TABLE]

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.

[TABLE]

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.

[TABLE]

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

[TABLE]

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.

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

[TABLE]

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:

[TABLE]

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

[TABLE]

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

[TABLE]

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

[TABLE]

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

[TABLE]

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.

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.

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.

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:

[TABLE]

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:

[TABLE]

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

[TABLE]

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

[TABLE]

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

[TABLE]

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:

[TABLE]

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:

[TABLE]

Hence, we obtain ($\leftrightarrow$).