aa short = AA, long = Acceptance Accuracy, long-indefinite = an ,foreign-
plural= adas short = ADAS, long = Advanced Driver-Assistance Systems, short-
indefinite = an, long-indefinite = an ,foreign-plural= acc short = ACC, long =
Adaptive Cruise Control, short-indefinite = an, long-indefinite = an ,foreign-
plural= adc short = ADC, long = Analog to Digital Converter, short-indefinite
= an, long-indefinite = an ,foreign-plural= afr short = , long = Always
Finitely Refutable, short-indefinite = an, long-indefinite = an ,foreign-
plural= afs short = , long = Always Finitely Satisfiable, short-indefinite =
an, long-indefinite = an ,foreign-plural= ai short = AI, long = artificial
intelligence ,foreign-plural= ais short = AIS, long = Active Instance Stack,
long-indefinite = an ,foreign-plural= aml short = AML, long = the ASPEN
Modeling Language ,foreign-plural= anml short = ANML, long = the Action
Notation Modeling Language ,foreign-plural= anmlite short = ANMLite, long =
the Action Notation Modeling Language Light ,foreign-plural= api short = API,
long = Application Programming Interface, short-indefinite = an, long-
indefinite = an ,foreign-plural= atam short = ATAM, long = Architecture
Tradeoff Analysis Method, short-indefinite = an, long-indefinite = an
,foreign-plural= atl short = ATL, long = Allen’s Temporal Logic, short-
indefinite = an, long-indefinite = an ,foreign-plural= bide short = BIDE, long
= BI-Directional Extension ,foreign-plural= bji short = BJI, long = between-
job inter-arrival time ,foreign-plural= can short = CAN, long = Controller
Area Network ,foreign-plural= capec short = CAPEC, long = Common Attack
Pattern Enumeration and Classification ,foreign-plural= cep short = CEP, long
= Complex Event Processing ,foreign-plural= cfc short = CFC, long =
Computation of Fixed-point Complexity ,foreign-plural= cfsm short = CFSM, long
= communicating finite state machine ,foreign-plural= cminwin short = CMINWIN,
long = Number of Minimal Windows of Occurrence ,foreign-plural= cpu short =
CPU, long = Central Processing Unit ,foreign-plural= csp short = CSP, long =
Communicating Sequential Processes ,foreign-plural= csv short = CSV, long =
Comma Separated Value ,foreign-plural= dfa short = DFA, long = Deterministic
Finite Automaton, long-plural-form = Deterministic Finite Automata ,foreign-
plural= dft short = DFT, long = Discrete Fourier Transform ,foreign-plural=
dsl short = DSL, long = domain-specific language ,foreign-plural= dsms short =
DSMS, long = Data Stream Management System ,foreign-plural= dut short = DUT,
long = device-under-test ,foreign-plural= ecu short = ECU, long = Electronic
Control Unit, short-indefinite = an, long-indefinite = an ,foreign-plural= edf
short = EDF, long = Earliest Deadline First ,foreign-plural= egads short =
EGADS, long = Extendible and Generic Anomaly Detection System, short-
indefinite = an, long-indefinite = an ,foreign-plural= epl short = EPL, long =
Event Processing Language, short-indefinite = an, long-indefinite = an
,foreign-plural= esl short = ESL, long = Expressive Stream Language, short-
indefinite = an, long-indefinite = an ,foreign-plural= esql short = ESQL, long
= Event Stream Query Language, short-indefinite = an, long-indefinite = an
,foreign-plural= etm short = ETM, long = Embedded Trace Macrocell, short-
indefinite = an, long-indefinite = an ,foreign-plural= evr short = EVR, long =
EVent Report ,foreign-plural= fa short = FA, long = Finite Automaton, long-
plural-form = Finite Automata, short-indefinite = an ,foreign-plural= fcda
short = FCDA, long = Forward Collision Detection and Avoidance, short-
indefinite = an ,foreign-plural= fifo short = FIFO, long = first-in first-out
,foreign-plural= fltl short = FLTL, long = ltl on Finite Traces, short-
indefinite = an ,foreign-plural= fpga short = FPGA, long = Field Programmable
Gate Array, short-indefinite = an ,foreign-plural= fr short = FR, long =
Finitely Refutable, short-indefinite = an ,foreign-plural= fs short = FS, long
= Finitely Satisfiable, short-indefinite = an ,foreign-plural= fsm short =
FSM, long = finite state machine, short-indefinite = an ,foreign-plural= gcc
short = GCC, long = the GNU Compiler Collection ,foreign-plural= gil short =
GIL, long = Graphical Interval Logic ,foreign-plural= gpl short = GPLv3, long
= Gnu Public License version 3 ,foreign-plural= gps short = GPS, long = Global
Positioning System ,foreign-plural= gui short = GUI, long = Graphical User
Interface ,foreign-plural= gsql short = GSQL, long = Gigascope Query Language
,foreign-plural= hdlc short = HDLC, long = High-level Data Link Control
,foreign-plural= hmm short = HMM, long = Hidden Markov Model ,foreign-plural=
hpc short = HPC, long = High Performance Computing, short-indefinite = an
,foreign-plural= hs short = HS, long = Halpern and Shoham’s modal logic of
intervals, short-indefinite = an ,foreign-plural= ids short = IDS, long =
Intrusion Detection System, short-indefinite = an, long-indefinite = an
,foreign-plural= ifp short = IFP, long = Information Flow Processing, short-
indefinite = an, long-indefinite = an ,foreign-plural= iji short = IJI, long =
intra-job inter-arrival time, short-indefinite = an, long-indefinite = an
,foreign-plural= imu short = IMU, long = Inertial Measurement Unit, short-
indefinite = an, long-indefinite = an ,foreign-plural= ip short = IP, long =
Internet Protocol, short-indefinite = an, long-indefinite = an ,foreign-
plural= isr short = ISR, long = interrupt service routine, short-indefinite =
an, long-indefinite = an ,foreign-plural= itl short = ITL, long = Interval
Temporal Logic, short-indefinite = an, long-indefinite = an ,foreign-plural=
jit short = JIT, long = Just-In-Time ,foreign-plural= jpl short = JPL, long =
Jet Propulsion Laboratory ,foreign-plural= json short = JSON, long =
JavaScript Object Notation ,foreign-plural= jvm short = JVM, long = Java
Virtual Machine ,foreign-plural= knn short = k-NN, long = k-Nearest Neighbors
,foreign-plural= lars short = LARS, long = Laboratory for Reliable Software
,foreign-plural= lanl short = LANL, long = the Los Alamos National Laboratory
,foreign-plural= lansce short = LANSCE, long = Los Alamos Neutron Science
Center ,foreign-plural= lcfsm short = LCFSM, long = lossy communicating finite
state machine, short-indefinite = an ,foreign-plural= ldw short = LDW, long =
Lane Departure Warning, short-indefinite = an ,foreign-plural= lka short =
LKA, long = Lane Keeping Assistance, short-indefinite = an ,foreign-plural=
loda short = LODA, long = Lightweight Online Detector of Anomalies, short-
indefinite = an, long-indefinite = an ,foreign-plural= ltl short = LTL, long =
Linear Temporal Logic, short-indefinite = an ,foreign-plural= ltl3 short =
LTL3, long = Three-value ltl, short-indefinite = an ,foreign-plural= ltl4
short = LTL4, long = four-value ltl, short-indefinite = an ,foreign-plural=
mcu short = MCU, long = Micro-controller Unit, short-indefinite = an ,foreign-
plural= milprit short = MILPRIT, long = Mining Interval Logic Patterns with
Regular expressIons consTraints ,foreign-plural= mitl short = MITL, long =
Metric Interval Temporal Logic, short-indefinite = an ,foreign-plural= msl
short = MSL, long = Mars Science Laboratory, short-indefinite = an ,foreign-
plural= mtl short = MTL, long = Metric Temporal Logic, short-indefinite = an
,foreign-plural= mfotl short = MFOTL, long = Metric First-Order Temporal
Logic, short-indefinite = an ,foreign-plural= nasa short = NASA, long = the
National Aeronautics and Space Administration ,foreign-plural= nba short =
NBA, long = Non-deterministic Büchi Automaton, long-plural-form = Non-
deterministic Büchi Automata, short-indefinite = an ,foreign-plural= nddl
short = NDDL, long = the EUROPA Modeling Language ,foreign-plural= nfa short =
NFA, long = Non-deterministic Finite Automaton, long-plural-form = Non-
deterministic Finite Automata, short-indefinite = an ,foreign-plural= nfr
short = , long = Never Finitely Refutable, short-indefinite = an ,foreign-
plural= nfs short = , long = Never Finitely Satisfiable, short-indefinite = an
,foreign-plural= os short = OS, long = Operating System, short-indefinite = an
,foreign-plural= pc short = PC, long = personal computer ,foreign-plural= pddl
short = PDDL, long = the Planning Domain Definition Language ,foreign-plural=
pid short = PID, long = Proportional-Integral-Derivative ,foreign-plural= pocs
short = POCS, long = projections onto convex sets ,foreign-plural= poset short
= POSET, long = Partially-Ordered Set ,foreign-plural= psdst short = PSDST,
long = Propositional Streaming Data-String Transducer, short-indefinite = a
,foreign-plural= psl short = PSL, long = Property Specification Language
,foreign-plural= ptl short = PTL, long = Propositional Temporal Logic
,foreign-plural= ptp short = PTP, long = Precision Time Protocol ,foreign-
plural= qbf short = QBF, long = Quantified Boolean Formula, long-plural-form =
Quantified Boolean Formulae ,foreign-plural= qea short = QEA, long =
Quantified Event Automata ,foreign-plural= ra short = RA, long = Rejection
Accuracy, short-indefinite = an ,foreign-plural= rems short = REMS, long =
Rover Environmental Monitoring Station ,foreign-plural= resp short = RESP,
long = the REdis Serialization Protocol, short-indefinite = an ,foreign-
plural= rm short = RM, long = Rate Monotonic, short-indefinite = an ,foreign-
plural= rnn short = RNN, long = Recurrent Neural Network, short-indefinite =
an ,foreign-plural= roc short = ROC, long = Receiver Operating Characteristic,
short-indefinite = an ,foreign-plural= ros short = ROS, long = Robot Operating
System ,foreign-plural= rpn short = RPN, long = Reverse Polish Notation,
short-indefinite = an ,foreign-plural= rv short = RV, long = Runtime
Verification, short-indefinite = an ,foreign-plural= rvltl short = RV-LTL,
long = Runtime Verification ltl, short-indefinite = an ,foreign-plural= saam
short = SAAM, long = Software Architecture Analysis Method, short-indefinite =
an ,foreign-plural= sax short = SAX, long = Symbolic Aggregate approXimation
,foreign-plural= sclwnrf short = LANL, long = System Call Logs with Natural
Random Faults ,foreign-plural= sdk short = SDK, long = Software Development
Kit ,foreign-plural= sdl short = SDL, long = Specification and Description
Language, short-indefinite = an ,foreign-plural= sdst short = SDST, long =
Streaming Data-String Transducer, short-indefinite = an ,foreign-plural= sfr
short = , long = Sometimes Finitely Refutable, short-indefinite = an ,foreign-
plural= sfs short = , long = Sometimes Finitely Satisfiable, short-indefinite
= an ,foreign-plural= sft short = SFT, long = Symbolic Finite-state
Transducer, short-indefinite = an ,foreign-plural= smm short = SMM, long =
Symbolic Mealy Machine, short-indefinite = an ,foreign-plural= soc short =
SoC, long = System-on-a-Chip, short-indefinite = an, long-plural-form =
Systems-on-Chips ,foreign-plural= spade short = SPACE, long = Sequential
PAttern Discovery using Equivalence classes ,foreign-plural= spam short =
SPAM, long = Sequential PAttern Mining ,foreign-plural= sql short = SQL, long
= Structured Query Language ,foreign-plural= srv short = SRV, long = Stream
Runtime Verification, short-indefinite = an ,foreign-plural= ssps short =
SSPS, long = Sequential Sense-Process-Send ,foreign-plural= stdev short =
stdev, long = standard deviation ,foreign-plural= stl short = STL, long =
Signal Temporal Logic, short-indefinite = an ,foreign-plural= svpa short =
SVPA, long = Symbolic Visibly Pushdown Automaton, long-plural-form = Symbolic
Visibly Pushdown Automata, short-indefinite = an ,foreign-plural= ta short =
TA, long = Timed Automaton, long-plural-form = Timed Automata ,foreign-plural=
tba short = TBA, long = Timed Büchi Automaton, long-plural-form = Timed Büchi
Automata ,foreign-plural= tltl short = TLTL, long = Timed ltl ,foreign-plural=
tksr short = TKSR, long = Time Series Knowledge Representation ,foreign-
plural= tre short = TRE, long = Timed Regular Expression ,foreign-plural= udp
short = UDP, long = User Datagram Protocol ,foreign-plural= uhml short =
$\mu$HML, long = $\mu$-Hennessy-Milner Logic, short-indefinite = a ,foreign-
plural= uml short = UML, long = Unified Modeling Language ,foreign-plural=
wcet short = WCET, long = Worst-Case Execution Time ,foreign-plural= wsdl
short = WSDL, long = Web Services Description Language ,foreign-plural= xml
short = XML, long = Extensible Markup Language, short-indefinite = an
,foreign-plural=

11institutetext:  Aalborg University, Aalborg Denmark
11email<EMAIL_ADDRESS>
# Monitoring Timed Properties (Revisited)††thanks: This paper was partly
sponsored by the S4OS Villum Investigator Grant and DIREC Digital Research
Center Denmark.

Thomas Møller Grosen  Sean Kauffman
Kim Guldstrand Larsen  Martin Zimmermann

###### Abstract

In this paper we revisit monitoring real-time systems with respect to
properties expressed either in Metric Interval Temporal Logic or as Timed
Büchi Automata. We offer efficient symbolic online monitoring algorithms in a
number of settings, exploiting so-called zones well-known from efficient model
checking of Timed Automata. The settings considered include new, much
simplified treatment of time divergence, monitoring under timing uncertainty,
and, extension of monitoring to offer minimum time estimates before conclusive
verdicts can be made.

###### Keywords:

Monitoring Timed Automata Metric Temporal Logic

##  1 Introduction

Runtime monitoring has gained acceptance as a method for formally verifying
the correctness of executing systems. Monitoring means to test a sequence of
observations of a system against a specification, often written in a formal
logic. Monitoring contrasts with static verification methods, like model
checking, in that it is computationally easier due to only testing a single
system execution. Runtime monitoring may also be applied to black-box systems
where details about the environment and design of the monitored system are not
required to be known in advance.

Many systems have so-called “extra-functional” requirements that must be
expressed with respect to time. These systems, generally called real-time
systems, are pervasive in modern life as the controllers of cyber-physical
systems. To express requirements with time components, logics such as mtl and
derivatives like mitl have been developed that extend the more classical ltl
with timing constraints [22, 2]. Finite Automata have also been extended with
time to form Timed Automata [1]. These formalisms allow the expression of
notions such as that “a response should occur within 20 milliseconds of a
request.”

Monitoring timed properties is possible and several solutions have been
proposed, each with their own advantages and drawbacks. In this work, we
introduce an efficient solution to the online monitoring problem for timed
properties under time divergence. Given a property expressed in mitl and a
finite timed sequence, our method determines if the property is guaranteed to
be satisfied or violated by any continuation of that finite sequence.
Additionally, the eventual satisfaction or violation of a property considers
that any future timing constraints will eventually be settled. Note that
online monitoring here contrasts with offline monitoring, where the system is
assumed to have terminated and timed properties are interpreted with finite
semantics. In online monitoring, liveness properties (e.g., “eventually, plaid
shirts will be popular”) cannot be violated since there will always be more
symbols, while they can be violated in offline monitoring, since the entire
sequence is known.

In this paper we revisit the monotoring of real-time properties expressed in
the logic mitl. In particular, we offer efficient symbolic online monitoring
algorithms for a number of settings. The symbolic approach exploits the fact
that properties in mitl may be translated into Timed Büchi Automata (TBA) [9]
under a point-wise semantics. Our symbolic approach exploits so-called
zones111also known as DBMs: Difference Bounded Matrices., which are used for
efficient model checking of Timed Automata [8]. In fact, zones has been
exploited in the tool UPPAAL TRON [23] for on-line testing that the behaviour
of a real-time system conforms to a Timed Automata specification.

In the first setting, we offer a new much simplified way of dealing with time
divergence. Time divergence means that during the infinite behaviour or a
real-time system time progresses beyond any finite bound. Time divergence is
stated as an assumption by most works in the area because it reflects reality.
However, the algorithmic support for time divergence in earlier work seems
somewhat underdeveloped.

To understand how time divergence impacts monitor verdicts, consider the
property “nothing should be observed after an hour”. It should be clear that
time divergence guarantees that no infinite sequence will satisfy this
property. Because we are interested in online monitoring properties over
infinite timed sequences, the language of the property is empty, and its
monitor should evaluate any finite prefix to be in violation of it.
Conversely, a monitor that does not compensate for time divergence will
register an _unknown_ verdict for finite prefixes that do not include
observations past the hour mark.

In a second setting, we extend our algorithmic method for monitoring to the
setting of timing uncertainty, i.e. a setting where the real-valued time-
points of events can only be observed up to a given precision. Finally, in a
third and final setting, we refine the algorithmic monitor to offer guaranteed
minimum time estimates that must pass until a conclusive verdict can be made.

##  2 Related Work

Many techniques to monitor timed properties have focused on monitoring logics
with finite-word semantics. The first work to introduce timed property
monitoring is by Roşu et al. focusing on discrete-time finite-word mtl [31].
Basin et al. proposed algorithms for monitoring real-time finite-word
properties in [5] and compared the differences between different time models.
Ulus et al. described monitoring tre for finite words using a union of two-
dimensional zones [32, 33]

The most closely related work to ours is that by Bauer et al. in which the
authors introduced the classical ltl3 monitor construction and then showed how
a similar construction could be used for tltl [6]. Their method transforms
tltl formula to event-clock automata which are strictly less expressive than
tba, which we support. Their algorithm also differs from ours in being based
on the so-called region automata. Though this construction _do_ provide a
principle monitoring algorithm the performance of zone-based monitoring
algorithms provide an order of magnitude improvement. Finally, their
monitoring algorithm does not readily seem to support time divergence. Two
more recent works have proposed solutions to the problem of monitoring timed
languages specified in mtl. Baldor et al. showed how to construct a monitor
for a dense-time mitl formula by constructing a tree of timed transducers [3].
They showed how subsets of mitl could be used to limit the complexity of their
technique which requires linear space in the size of the input for the full
fragment. Ho et al. split unbounded and bounded parts of a dense-time mitl
formula for monitoring, using traditional ltl monitoring for the unbounded
parts and permitting a simpler construction for the (finite-word) bounded
parts [18]. Unlike the work by Baldor et al., their method is size independent
of the input. However, it does require non-elementary blowup of the formula to
ensure no unbounded operators appear in the context of a bounded operator.
They also monitor bounded parts using a dynamic programming formulation that
relies on a maximum bound for the number of events in a time span. Neither the
solution by Baldor et al. or Ho et al. address time-divergence.

Crucially, none of the previously mentioned works implement their solutions.
On the other hand, some tools have been released for monitoring other timed
logics. Basin et al. implemented MonPoly, which can monitor an expressive
finite-word (safety) fragment of mfotl using discrete time semantics [4].
Bulychev et al. implemented a rewrite-based monitoring algorithm similar to
the one proposed in [31] for Weighted mtl in the Uppaal SMC tool [11]. R2U2 is
a tool for generating monitors for fpga developed by Moosbrugger et al. that
supports finite-word mitl properties [26]. Much more recently, Chattopadhyay
and Mamouras presented a verified monitor for discrete, past-time (finite
word) mitl with quantitative semantics [13]. Some tools also exist to convert
timed logics to automata which we will cover in the next section.

##  3 Preliminaries

We first define some notation used throughout the paper. The set of natural
numbers (including zero) is $\mathbb{N}$. The set of real numbers is
$\mathbb{R}$ and the set of non-negative real numbers is $\mathbb{R}_{\geq
0}$. The set of Boolean values is $\mathbb{B}$ and the three-valued set of
monitor verdicts is $\mathbb{B}_{3}=\\{\top,\textbf{{?}},\bot\\}$. We shall
assume that $\mathbb{B}_{3}$ is equipped with a partial order where
$\textbf{{?}}\sqsubseteq\top$ and $\textbf{{?}}\sqsubseteq\bot$. Given a set
$S$ the set of all its subsets is denoted $2^{S}$. The cross product of two
sets $S$ and $T$ is $S\times T$. Given a sequence $\sigma$, $\sigma_{i}$
denotes the element at the $i$th position of $\sigma$ (where one is the first
position) and $\sigma^{i}$ denotes the suffix of $\sigma$ starting at index
$i$. Given two sequences $s$ and $t$, we write $s\cdot t$ to denote their
concatenation.

A timed word over a finite alphabet $\Sigma$ is a pair $\rho=(\sigma,\tau)$
where $\sigma$ is a non-empty word over $\Sigma$ and and $\tau$ is a sequence
of strictly increasing non-negative real numbers of the same length as
$\sigma$. Timed words may be finite or infinite where the type of finite timed
words is $T\\!\Sigma^{*}$ and the type of infinite timed words is
$T\\!\Sigma^{\omega}$. We also represent a timed word as a sequence of pairs
$(\sigma_{1},\tau_{1}),(\sigma_{2},\tau_{2}),\ldots$. If
$\rho=(\sigma_{1},\tau_{1}),(\sigma_{2},\tau_{2}),\ldots(\sigma_{n},\tau_{n})$
is a finite timed word, we denote by $\tau(\rho)$ the total time duration of
$\rho$, i.e. $\tau_{n}$.

###  mtl

We use the Metric Interval Temporal Logic, mitl, in this work to formalize
examples because we can translate it into the tba that we use in our
monitoring algorithm. Brihaye et al. developed the tool MightyL to translate
mitl formulas to tba in a compositional manner [9]. Some earlier work
implemented algorithms to translate subsets of mitl to tba as well. Li et al.
proposed and implemented Casaal, a tool to construct deterministic
approximations of tba from mtl0,∞ formulas [24, 10]. Geilen and Dams
implemented an algorithm to produce a deterministic ta for dense-time mitl≤ (a
subset of mtl0,∞) using an on-the-fly tableau construction that discretizes
the time domain and only supports an upper bound [17]. Note that some other
works exist that provide algorithms for the translation of mitl or related
logics to tba, but without providing implementations [16, 27].

Let $\Sigma$ be a finite alphabet. The syntax of mitl formula $\varphi$ over
$\Sigma$ is given by the following grammar:

$\varphi\coloncolonequals p\ |\ \neg\varphi\ |\ \varphi\vee\varphi\ |\
X_{I}\varphi\ |\ \varphi\ U_{I}\varphi\ $

where $p\in\Sigma$, and $I$ is a non-singular interval over $\mathbb{R}_{\geq
0}$ with endpoints in ${\mathbb{N}\cup\\{+\infty\\}}$. Note that we often
write $\leavevmode\resizebox{5.55557pt}{0.0pt}{$\sim$}\,n$ for
$I=\\{d\in\mathbb{R}:d\leavevmode\resizebox{5.55557pt}{0.0pt}{$\sim$}n\\}$
where $\leavevmode\resizebox{5.55557pt}{0.0pt}{$\sim$}\in\\{<,\leq,\geq,>\\}$,
and $n\in\mathbb{N}$.

The semantics of mitl is defined over infinite timed words. Given such a timed
word $\rho=(\sigma_{1},\tau_{1}),(\sigma_{2},\tau_{2}),\ldots\in
T\\!\Sigma^{\omega}$, a position $i\geq 1$, and mitl formula $\varphi$, we
inductively define the satisfaction relation $\rho,i\models\varphi$ as
follows:

${\rho,i\models}$ |  ${p}$ | if | ${p=\sigma_{i}}$
---|---|---|---
${\rho,i\models}$ |  ${\neg\varphi}$ | if | ${\rho,i\not\models\varphi}$
${\rho,i\models}$ |  ${\varphi\vee\psi}$ | if | ${\rho,i\models\varphi\textit{ or }\rho,i\models\psi}$
${\rho,i\models}$ |  ${X_{I}\varphi}$ | if | ${\rho,{(i+1)}\models\varphi}\textit{ and }\tau_{i+1}-\tau_{i}\in I$
${\rho,i\models}$ |  ${\varphi\ U_{I}\psi}$ | if | ${\exists k\geq i\raisebox{-1.07639pt}{\scalebox{1.6}{.}}{\ }\rho,k\models\psi,\tau_{k}-\tau_{i-1}\in I\textit{ and }\forall j\raisebox{-1.07639pt}{\scalebox{1.6}{.}}{\ }1\leq j<k\raisebox{-1.07639pt}{\scalebox{1.6}{.}}{\ }\rho,j\models\varphi}$

where $\tau_{0}=0$. We write $\rho\models\varphi$ whenever
$\rho,1\models\varphi$. We also define the standard syntactic sugar:
$\mathit{true}=p\vee\neg p$, $\mathit{false}=\neg\mathit{true}$,
$\varphi\wedge\psi=\neg(\neg\varphi\vee\neg\psi)$,
$\varphi\rightarrow\psi=\neg\varphi\vee\psi$, $F_{I}\varphi=\mathit{true}\
U_{I}\varphi$, and $G_{I}\varphi=\neg F_{I}\neg\varphi$. Given mitl formula
$\varphi$, its language $\mathcal{L}(\varphi)$ is the set of all infinite
timed words that satisfy $\varphi$.

### Timed Automata

tba $\mathcal{A}$ is a six-tuple $(Q,Q_{0},\Sigma,C,\Delta,\mathcal{F})$,
where $\Sigma$ is a finite alphabet, $Q$ is a finite set of locations,
$Q_{0}\subseteq Q$ is a set of initial locations, $C$ is a finite set of
clocks, $\Delta\subseteq Q\times Q\times\Sigma\times 2^{C}\times G(C)$ is a
finite set of transitions with $G(C)$ being the type of constraints over $C$,
and $\mathcal{F}\subseteq Q$ is a set of accepting locations. A transition
$(q,q^{\prime},\alpha,\lambda,g)$ is an edge from $q$ to $q^{\prime}$ on input
symbol $\alpha$ where $\lambda$ is the set of clocks to reset and $g$ is a
clock constraint over $C$. A clock constraint is a conjunction of atomic
constraints of the form $c\sim n$, where $c$ is a clock, $n\in\mathbb{N}$, and
$\sim\ \in\\{<,\leq,=,\geq,>\\}$. A state of tba is a pair $(q,v)$ where $q$
is a location in $Q$ and $v:C\rightarrow\mathbb{R}_{\geq 0}$ is a valuation
mapping clocks to their values. We say that for any $d\in\mathbb{R}_{\geq 0}$,
$v+d$ is the valuation where $d$ is added to all clock values in $v$.

A run of $\mathcal{A}$ from a starting state $(q_{0},v_{0})$ is a sequence of
steps over a timed word $(\sigma,\tau)$ of the form

$(q_{0},v_{0})\overset{(\sigma_{1},t_{1})}{\longrightarrow}(q_{1},v_{1})\overset{(\sigma_{2},t_{2})}{\longrightarrow}(q_{2},v_{2})\overset{(\sigma_{3},t_{3})}{\longrightarrow}\cdots$

where for all $i\geq 1$ there is a transition
$(q_{i-1},q_{i},\sigma_{i},\lambda_{i},g_{i})$ such that $v_{i}(c)=0$ for all
$c$ in $\lambda_{i}$ and $v_{i-1}(c)$ otherwise, and $g$ is satisfied by the
valuation $v_{i-1}+(t_{i}-t_{i-1})$. Given a run $r$, we denote the set of
locations visited infinitely many times by $r$ as $\textit{inf}\,(r)$. A run
$r$ of $\mathcal{A}$ is accepting if
$\textit{inf}\,(r)\cap\mathcal{F}\neq\varnothing{}$. The language of
$\mathcal{A}$ from a starting state $(q,v)$, denoted
$\mathcal{L}(\mathcal{A},(q,v))$, is the set of all timed words with an
accepting run in $\mathcal{A}$ starting from $(q,v)$. We define the language
of $\mathcal{A}$, written $\mathcal{L}(\mathcal{A})$, to be
$\bigcup_{q}\mathcal{L}(\mathcal{A},(q,v_{0}))$, where $q$ ranges over all
locations in $Q_{0}$ and where $v_{0}(c)=0$ for all $c\in C$.

Given two tba $\mathcal{A}=(Q,Q_{0},\Sigma,C,\Delta,\mathcal{F})$ and
$\mathcal{A}^{\prime}=(Q^{\prime},Q^{\prime}_{0},\Sigma,C^{\prime},\Delta^{\prime},\mathcal{F}^{\prime})$,
their intersection is denoted
$\mathcal{A}\otimes\mathcal{A}^{\prime}=(Q^{\otimes},Q_{0}^{\otimes},\Sigma,C^{\otimes},\Delta^{\otimes},\mathcal{F}^{\otimes})$,
where

  * •

$Q_{\otimes}=Q\times Q^{\prime}\times\\{1,2\\}$,

  * •

$Q_{0}^{\otimes}=Q_{0}\times Q^{\prime}_{0}\times\\{1\\}$,

  * •

$C^{\otimes}=C\cup C^{\prime}$ (we assume they are disjoint),

  * •

$\Delta^{\otimes}=\Delta_{1}^{\otimes}\cup\Delta_{2}^{\otimes}$ with

    * $\Delta_{1}^{\otimes}=\\{((q_{1},q^{\prime}_{1},1),(q_{2},q^{\prime}_{2},i),\alpha,\lambda\cup\lambda^{\prime},g\wedge g^{\prime}):(q_{1},q_{2},\alpha,\lambda,g)\in\Delta$ and $(q^{\prime}_{1},q^{\prime}_{2},\alpha,\lambda^{\prime},g^{\prime})\in\Delta^{\prime}$ and $i=2$ if $q_{1}\in\mathcal{F}$ else $i=1\\}$ and

    * $\Delta_{2}^{\otimes}=\\{((q_{1},q^{\prime}_{1},2),(q_{2},q^{\prime}_{2},i),\alpha,\lambda\cup\lambda^{\prime},g\wedge g^{\prime}):(q_{1},q_{2},\alpha,\lambda,g)\in\Delta$ and $(q^{\prime}_{1},q^{\prime}_{2},\alpha,\lambda^{\prime},g^{\prime})\in\Delta^{\prime}$ and $i=1$ if $q^{\prime}_{1}\in\mathcal{F}^{\prime}$ else $i=2\\}$,

  * •

and $\mathcal{F}^{\otimes}=(\mathcal{F}\times
Q^{\prime}\times\\{1\\})\cup(Q\times\mathcal{F}^{\prime}\times\\{2\\})$.

We note that
$\mathcal{L}(\mathcal{A}\otimes\mathcal{A}^{\prime})=\mathcal{L}(\mathcal{A})\cap\mathcal{L}(\mathcal{A}^{\prime})$.

##  4 Monitoring in a Timed Setting

In this section, we describe monitoring and show how it applies in the timed
setting. We first, briefly, introduce monitoring in the untimed case and then
extend it to the timed case.

Traditionally in rv, properties are specified using a temporal logic such as
ltl and a monitor is constructed from those properties. A monitor is a kind of
program that takes a finite word as an input and returns a _verdict_ depending
on the relationship between the input and the property from which the monitor
is constructed. Verdicts are usually of the form _accept_ ($\top$), _reject_
($\bot$), or _unknown_ (?), although larger verdict domains exist to provide
more information.

In online monitoring (our interest), the properties specify behaviors over
infinite sequences of symbols, or words, while the monitor must interpret
those specifications over an ever-growing finite prefix of such an infinite
word. The most prevalent solution to this problem is to use a monitor
semantics where acceptance or rejection means that the finite word
_determines_ the property and no future suffix can alter the verdict. In the
case where the finite prefix does not determine the property, the monitor
outputs an _unknown_ verdict and continues.

Monitoring languages of timed infinite words works in much the same way as in
the untimed setting. A finite prefix of an infinite timed word is checked to
see if it determines the property. If all possible infinite extensions of the
prefix result in a word that is included in the monitored property, then the
monitor returns the $\top$ verdict. If no possible infinite extensions lead to
a word that is included in the monitored property, then the monitor returns
the $\bot$ verdict. If extensions exist that could lead to either outcome,
then the monitor returns ? and continues monitoring.

######  Definition 1 (Monitor verdicts for timed languages).

Given a language of infinite timed words $\phi\subseteq T\\!\Sigma^{\omega}$
and a finite timed word $\rho\in T\\!\Sigma^{*}$, the function
$\mathcal{V}:2^{T\\!\Sigma^{\omega}}\rightarrow
T\\!\Sigma^{*}\rightarrow\mathbb{B}_{3}$ evaluates to a verdict with the
following definition:

$\mathcal{V}(\phi)(\rho)=\left.\begin{cases}\top&\text{if
}\rho\cdot\mu\in\phi\ $ for all $\mu\in T\\!\Sigma^{\omega},\\\ \bot&\text{if
}\rho\cdot\mu\notin\phi\ $ for all $\mu\in T\\!\Sigma^{\omega},\\\
\textbf{{?}}&\text{otherwise}.\end{cases}\right.$

######  Example 1.

Consider the bounded response property “whenever $a$ is observed, $b$ should
be observed within 30 time units” that is specified by the mitl formula
$\varphi=G(a\rightarrow F_{\leq 30}b)$ where $\Sigma=\\{a,b,c\\}$. This
property corresponds to the tba shown in Figure 1. This type of time-bounded
leadsto property is very common for real-time systems [25]. It states that
some trigger $a$ is followed by a reaction $b$ before the deadline elapses.
Note we draw the “sink” state $q_{3}$ here for illustrative purposes as we
will return to this example later in the paper, but it can be omitted without
changing the language of the automaton.

$q_{1}$$q_{2}$$q_{3}$$b,c$$a$$x\colonequals 0$$a,c$$x\leq 30$$b$$x\leq
30$$a,b,c$$x>30$$a,b,c$ Figure 1: tba corresponding to $G(a\rightarrow F_{\leq
30}b)$

Now consider the finite timed prefix $\rho_{\text{ok}}=(a,10),(b,20)$. The
verdict in this case is
$\mathcal{V}(\mathcal{L}(\varphi))(\rho_{\text{ok}})=\textbf{{?}}$, since
there are infinite extensions of the prefix that satisfy the property and
those that violate it. For example, if the pattern of $\rho_{\text{ok}}$ was
repeated infinitely many times, the resulting infinite timed word
$\rho_{\text{ok}}^{\omega}=((a,10\cdot i),(b,20\cdot i))^{i\geq 1}$ would
satisfy $\varphi$. Now suppose the prefix $\rho_{\text{bad}}=(a,10),(b,50)$.
In this case, the prefix only has infinite extensions that violate the
property, so $\mathcal{V}(\mathcal{L}(\varphi))(\rho_{\text{bad}})=\bot$.

This property demonstrates a way in which timed monitoring differs from the
untimed setting. If we remove the time constraint and consider the (unbounded)
response property $G(a\rightarrow Fb)$, no finite prefix could ever determine
the property and so the only possible verdict would be ?. This is a classic
example of what is called an _unmonitorable_ property [29, 7, 21].

##  5 Time Divergence

Note that Definition 1 does not take time divergence into account, i.e., a
verdict can be based on convergent extensions of a given prefix. As we will
see in Example 2, this leads to invalid verdicts. In this section, we consider
the monitoring problem in the presence of time divergence and show how it
affects the verdicts from monitors for timed languages. Time divergence
entails that time will always progress beyond any given time-bound.

We begin by defining the type of infinite time divergent words. These are the
only timed words that will occur in practice, since time always diverges.
Mathematically, however, the type $T\\!\Sigma^{\omega}$ includes words that
are not time divergent, e.g.,
$(\alpha,\frac{1}{2}),(\alpha,\frac{3}{4}),(\alpha,\frac{7}{8}),\ldots$. The
definition states that time divergent words are those where the time sequence
is unbounded. Note that we do not consider _finite_ timed words either
divergent or convergent even though their time sequences technically converge.

######  Definition 2.

The set of all time divergent words
$T\\!\\!\vbox{\hbox{{\tiny{D}}}}\Sigma^{\omega}\subseteq T\\!\Sigma^{\omega}$
is the set of all timed words
$(\sigma_{1},\tau_{1}),(\sigma_{2},\tau_{2})\ldots$ such that
$\lim_{i\to\infty}\tau_{i}=+\infty$.

We now use the set of time divergent words to define a verdict function that
accounts for time divergence. Crucially, the properties that we monitor may
include non-time divergent words. In that case, the verdict returned by the
evaluation function under time divergence $\mathcal{V}_{D}$ may differ from
the verdict returned by $\mathcal{V}$.

######  Definition 3 (Monitor verdicts under time divergence).

Given a language of infinite timed words $\phi\subseteq T\\!\Sigma^{\omega}$
and a finite timed word $\rho\in T\\!\Sigma^{*}$, the function
$\mathcal{V}_{D}:2^{T\\!\Sigma^{\omega}}\rightarrow
T\\!\Sigma^{*}\rightarrow\mathbb{B}_{3}$ evaluates to a verdict with the
following definition:

$\mathcal{V}_{D}(\phi)(\rho)=\left.\begin{cases}\top&\text{if
}\rho\cdot\mu\in\phi\ $ for all $\mu\in
T\\!\\!\vbox{\hbox{{\tiny{D}}}}\Sigma^{\omega},\\\ \bot&\text{if
}\rho\cdot\mu\notin\phi\ $ for all $\mu\in
T\\!\\!\vbox{\hbox{{\tiny{D}}}}\Sigma^{\omega},\\\
\textbf{{?}}&\text{otherwise}.\end{cases}\right.$

######  Example 2.

Consider the property “the system will continue past 20 time units”
represented by the mitl formula $\varphi=F_{\geq 20}a$, where
$\Sigma=\\{a\\}$. This property corresponds to the tba shown in Figure 2.

$q_{1}$$q_{2}$$a$$a$$x\geq 20$$a$ Figure 2: tba corresponding to $F_{\geq
20}a$

If this property is monitored, the verdict may change depending on whether
time divergence is accounted for. Under time divergence, this property is
clearly a tautology since all infinite time divergent words must eventually
reach time 20 and location $q_{2}$. However, if time divergence is not assumed
as in Definition 1, then it is possible for an infinite timed word to never
pass time 20 and therefore stay in location $q_{1}$.

Suppose, for example, the finite timed prefix $\rho=(a,10)$. Since $\varphi$
is a tautology under time divergence,
$\mathcal{V}_{D}(\mathcal{L}(\varphi))(\rho)=\top$. However,
$\mathcal{V}(\mathcal{L}(\varphi))(\rho)=\textbf{{?}}$, since
$T\\!\Sigma^{\omega}$ contains time-convergent suffixes to $\rho$ that are in
not in the language of $\varphi$.

To ensure that verdicts are correct for all properties, we monitor an
intersection of the given automata with a special tba that only accepts time
divergent words. This tba, which we will call $\mathcal{A}_{\textit{D}}$, is
shown in Figure 3. The automaton must visit the left location infinitely often
to accept and it can only visit this state once time has passed a threshold of
one time unit. Note that the exact threshold is arbitrary and could be any
number; the purpose is ensure that the language of the automaton is exactly
the language of time divergent words.

$A$$B$$\Sigma$$z\colonequals 0$$\Sigma$$z\geq 1$$\Sigma$$z<1$ Figure 3: tba
$\mathcal{A}_{\textit{D}}$ to model divergence

######  Theorem 5.1.

The language of $\mathcal{A}_{\textit{D}}$ is exactly the set of all time
divergent words.

######  Example 3.

We now consider the complement property to Example 2 that is accepted by the
mitl formula $\overline{\varphi}=G_{\geq 20}\mathit{false}$. Note that, since
we use symbols in our mitl formulas and not propositions, we cannot write
$\neg a$ here but must use its complement $\Sigma\setminus\\{a\\}=\varnothing$
which is equivalent to $\mathit{false}$ in our mitl syntax. The tba for
$\overline{\varphi}$ is shown in Figure 4.

$\overline{q_{1}}$$a$$y<20$ Figure 4: tba corresponding to $G_{\geq
20}\mathit{false}$

Now we want to intersect this tba with $\mathcal{A}_{\textit{D}}$ to restrict
its language to only time divergent words. The result of this operation is
shown in Figure 5. Note that we are intentionally showing a trivial example to
simplify the presentation; a two state automaton like that in Figure 1
intersected with $\mathcal{A}_{\textit{D}}$ has eight locations and, in that
case, 23 transitions.

$B_{1}$$A_{1}$$A_{2}$$B_{2}$$a$$y<20$$z\colonequals 0$$a$$y<20$$z\colonequals
0$$a$$y<20$$a$$y<20,z\geq 1$$a$$y<20$ Figure 5: tba corresponding to $G_{\geq
20}\mathit{false}$ intersected with $\mathcal{A}_{\textit{D}}$

In this tba, an accepting run must visit location $A_{2}$ infinitely many
times. However, it should be clear that this is not possible, since the run
must include fewer than 20 combinations of the transition from $B_{1}$ to
$B_{2}$ (which resets the $z$ clock) and the transition from $B_{2}$ to
$A_{2}$, which requires that it passes 1. The reason is that the latter
transition also requires the clock $y$ to stay below 20 and $y$ is never
reset. The result is that the automaton has an empty language.

##  6 Symbolic Method for Monitoring

In this section, we describe an algorithm to monitor languages of infinite
timed words that correctly accounts for time divergence. Our algorithm is
loosely based on the classical construction for monitoring ltl3 by Bauer et
al. [6], but with alterations to address the many differences between the
timed and untimed domains.

Our solution requires that properties are specified as two tba - one for the
property and one for its complement. Although non-deterministic tba are not
closed under complementation, we consider this requirement to not be too much
of a limitation. This is because we expect a property to be expressed by a
user in mitl, which, along with its negation, can be converted to tbas using
one of the methods described in Section 3.

Before we address the monitoring algorithm, we first introduce the notions of
states of tba with a non-empty language and state estimates. Given tba
$\mathcal{A}$, a state $(q,v)$ has a non-empty language when it has an
accepting run starting in $(q,v)$.

######  Definition 4.

Given tba $\mathcal{A}=(Q,Q_{0},\Sigma,C,\Delta,\mathcal{F})$, the set of
states with non-empty language is $S_{\mathcal{A}}^{\textit{ne}}=\\{(q,v):q\in
Q,v\in C\rightarrow\mathbb{R}_{\geq
0}\raisebox{-1.07639pt}{\scalebox{1.6}{.}}{\
}\mathcal{L}(\mathcal{A},(q,v))\neq\varnothing\\}$.

In the following definition, we write
$(q_{0},v_{0})\xrightarrow{\rho}_{\mathcal{A}}(q,v)$ to denote a run that
takes $\mathcal{A}$ from $(q_{0},v_{0})$ to $(q,v)$ processing the input
$\rho$.

######  Definition 5.

Given tba $\mathcal{A}$ and a finite timed word $\rho\in T\\!\Sigma^{*}$, the
set of possible states a run over $\rho$ starting from initial states of
$\mathcal{A}$ can end in is given by
$\mathcal{T}_{\mathcal{A}}(\rho)=\\{(q,v):(q_{0},v_{0})\xrightarrow{\rho}_{\mathcal{A}}(q,v)\text{
where }(q_{0},v_{0})\text{ is }\text{an }\text{initial }\text{state of
}\mathcal{A}\\}$. We call this the state estimate of $\mathcal{A}$ over
$\rho$.

Note that the state estimate $\mathcal{T}_{\mathcal{A}}(\rho)$ is always a
finite set of states of $\mathcal{A}$.

We can now define a function to compute a monitor verdict using Definitions 4
and 5. To determine a verdict for a language $\phi\subseteq
T\\!\Sigma^{\omega}$, the function requires both tba $\mathcal{A}$ such that
$\mathcal{L}(\mathcal{A})=\phi$ and its complement, $\overline{\mathcal{A}}$.
Definition 6 states that a finite timed word $\rho\in T\\!\Sigma^{*}$
positively (negatively) determines the property under time divergence if the
states of $\overline{\mathcal{A}}\otimes\mathcal{A}_{\textit{D}}$
($\mathcal{A}\otimes\mathcal{A}_{\textit{D}}$) with non-empty languages are
disjoint from the state estimate of
$\overline{\mathcal{A}}\otimes\mathcal{A}_{\textit{D}}$
($\mathcal{A}\otimes\mathcal{A}_{\textit{D}}$) over $\rho$.

######  Definition 6 (Monitoring tba under time divergence).

Given tba $\mathcal{A}$, its complement $\overline{\mathcal{A}}$
($\mathcal{L}(\overline{\mathcal{A}})=T\\!\Sigma^{\omega}\setminus\mathcal{L}(\mathcal{A})$),
the automaton $\mathcal{A}_{\textit{D}}$ such that
$\mathcal{L}(\mathcal{A}_{\textit{D}})=T\\!\\!\vbox{\hbox{{\tiny{D}}}}\Sigma^{\omega}$,
and a finite timed word $\rho\in T\\!\Sigma^{*}$,
${\mathcal{M}:\mathbb{A}\times\mathbb{A}\rightarrow
T\\!\Sigma^{*}\rightarrow\mathbb{B}_{3}}$ computes a verdict with the
following definition.

$\mathcal{M}(\mathcal{A},\overline{\mathcal{A}})(\rho)=\left.\begin{cases}\top&\text{if
}\mathcal{T}_{\overline{\mathcal{A}}\otimes\mathcal{A}_{\textit{D}}}(\rho)\cap
S_{\overline{\mathcal{A}}\otimes\mathcal{A}_{\textit{D}}}^{\textit{ne}}=\varnothing\\\
\bot&\text{if
}\mathcal{T}_{\mathcal{A}\otimes\mathcal{A}_{\textit{D}}}(\rho)\cap
S_{\mathcal{A}\otimes\mathcal{A}_{\textit{D}}}^{\textit{ne}}=\varnothing\\\
\textbf{{?}}&\text{otherwise}\end{cases}\right.$

######  Theorem 6.1.

$\mathcal{M}(\mathcal{A},\overline{\mathcal{A}})(\rho)=\mathcal{V}_{D}(\mathcal{L}(\mathcal{A}))(\rho)$
for all $\rho\in T\\!\Sigma^{*}$.

So far, this construction is very similar to the the classical procedure for
monitoring ltl3 with the addition of $\mathcal{A}_{\textit{D}}$ to account for
time divergence. However, the set of states with non-empty languages of tba is
likely to be infinite, and its state estimate over a symbolic trace (see
Section 7) may be as well. We now present a symbolic online algorithm to
compute these infinite sets and their intersections in an efficient manner.

### Monitoring Algorithm

We assume that the language we will monitor $\phi$ and its complement
$\overline{\phi}$ are given as tba $\mathcal{A}_{\phi}$ and
$\mathcal{A}_{\overline{\phi}}$, where $\mathcal{L}(\mathcal{A}_{\phi})=\phi$
and $\mathcal{L}(\mathcal{A}_{\overline{\phi}})=\overline{\phi}$. We begin by
computing the intersection of both automata with $\mathcal{A}_{\textit{D}}$
(we hereafter refer to these intersection automata as $\mathcal{A}$ and
$\overline{\mathcal{A}}$). We continue by finding the states of the automata
with non-empty languages, also called the non-empty states from Definition 4.
We then compute the intersection of the non-empty states with the state
estimate (from Definition 5) of $\mathcal{A}$ and $\overline{\mathcal{A}}$
over $\rho$. If one of the intersections is empty, then we can output $\top$
or $\bot$, otherwise, we output ?.

We can calculate the set $S_{\mathcal{A}}^{\textit{ne}}$ as a fixpoint using a
backwards reachability algorithm. In order to practically work with the states
of tba we use a symbolic representation of the clock valuations, namely zones.
A symbolic state $(q,Z)$ is a pair of a location and a zone. A zone is a
finite conjunction of lower and upper bound integer constraints on clocks and
clock differences, and may be efficiently represented using so-called
Difference Bounded Matrices (DBMs) [8]. We say that $(q,v)\in(q,Z)$ or $v\in
Z$ iff $v\models Z$, such that the clock values in $v$ satisfies all
constraints in $Z$. Similarly we say that $v(x)\models Z$ if the value $v(x)$
satisfies the bounds on $x$ in $Z$. We now define several zone operations,
that we will need.

######  Definition 7.

Given two zones $Z$ and $Z^{\prime}$ over a set $C$ of clocks, a set of clocks
$\lambda\subseteq C$, a positive real number $t$ and an interval
$I=[t_{1},t_{2}]$ between to positive real numbers, we define the following
operations on zones:

  * •

$\textit{free}_{\lambda}(Z)=\\{v:\forall x\in
C\raisebox{-1.07639pt}{\scalebox{1.6}{.}}{\ }v(x)\models Z\textit{ if
}x\notin\lambda\\}$

  * •

$Z_{\textit{free}}=\textit{free}_{C}(Z)$

  * •

$Z[\lambda]=\\{v:\exists v^{\prime}\in Z\>\forall x\in
C\raisebox{-1.07639pt}{\scalebox{1.6}{.}}{\ }v(x)=0\textit{ if
}x\in\lambda\textit{ otherwise }v(x)=v^{\prime}(x)\\}$

  * •

$Z^{\nearrow}=\\{v:\exists v^{\prime}\in
Z\raisebox{-1.07639pt}{\scalebox{1.6}{.}}{\ }v=v^{\prime}+d\textit{ for some
}d\in\mathbb{R}_{\geq 0}\\}$

  * •

$Z^{\searrow}=\\{v:\exists v^{\prime}\in
Z\raisebox{-1.07639pt}{\scalebox{1.6}{.}}{\ }v=v^{\prime}-d\textit{ for some
}d\in\mathbb{R}_{\geq 0}\\}$

  * •

$Z^{\nearrow_{I}}=\\{v:\exists v^{\prime}\in Z\>\forall x\in
C\raisebox{-1.07639pt}{\scalebox{1.6}{.}}{\ }v^{\prime}(x)+t_{1}\leq v(x)\leq
v^{\prime}(x)+t_{2}\\}$

  * •

$Z\land Z^{\prime}=\\{v:v\models Z\textit{ and }v\models Z^{\prime}\\}$

  * •

$Z_{0}=\\{v:\forall x\in C\raisebox{-1.07639pt}{\scalebox{1.6}{.}}{\
}v(x)=0\\}$

All of the above operations on zones may be efficiently implemented using the
DBM data-structure [8]. We now proceed to develop the online zone-based
procedure we use to monitor real-time properties specified by TBAs.

$Pred_{\mathcal{A}}(q,Z)$ (described in Algorithm 1) is the set of symbolic
states that can, by a single transition and delay, backwards reach the state
$(q,Z)$ of $\mathcal{A}$.

Algorithm 1 Find the predecessors (single transition) of a state

tba $\mathcal{A}=(Q,Q_{0},\Sigma,C,\Delta,\mathcal{F})$ and a symbolic state
$(q,Z)$

$\textit{Pred}_{\mathcal{A}}(q,Z)$

$\textit{Predecessors}\leftarrow\varnothing$

for $(q^{\prime},q,\alpha,\lambda,g)\in\Delta$ do

$Z^{\prime}=\textit{free}_{\lambda}(Z^{\searrow}\wedge\\{x=0:x\in\lambda\\}\wedge
g)$

$\textit{Predecessors}\leftarrow\textit{Predecessors}\cup\\{(q^{\prime},Z^{\prime})\\}$

end for

return Predecessors

$\textit{Reach}_{\mathcal{A}}(S)$ (described in Algorithm 2) is the set of
symbolic states that can, by at least one transition, reach a state in $S$.

Algorithm 2 Compute the states that can reach the given states with at least
one transition

tba $\mathcal{A}$ and a set of symbolic states $S$

$\textit{Reach}_{\mathcal{A}}(S)$

$\textit{Waiting}\leftarrow\varnothing$

$\textit{Passed}\leftarrow\varnothing$

for $s\in S$ do

$\textit{Waiting}\leftarrow\textit{Waiting}\cup\textit{Pred}_{\mathcal{A}}(s)$

end for

while $\textit{Waiting}\neq\varnothing$ do

select and remove $s$ from Waiting

$\textit{Waiting}\leftarrow\textit{Waiting}\cup\textit{Pred}_{\mathcal{A}}(s)$

$\textit{Passed}\leftarrow\textit{Passed}\cup\\{s\\}$

end while

return $Passed$

Algorithm 3 Calculate the set of states that can infinitely often reach a
location in $Q$

tba $\mathcal{A}$ and a set of locations $Q^{\prime}$

$\textit{Reach}_{\mathcal{A}}^{\infty}(Q^{\prime})$

$S_{Q^{\prime}}\leftarrow\varnothing$

for $q\in Q^{\prime}$ do

$S_{Q^{\prime}}\leftarrow S_{Q^{\prime}}\cup\\{(q,Z_{\textit{free}})\\}$

end for

$S_{a}\leftarrow S_{Q^{\prime}}$

$S_{b}\leftarrow\varnothing$

while $S_{a}\neq S_{b}$ do

$S_{b}\leftarrow S_{a}$

$S_{a}\leftarrow\textit{Reach}_{\mathcal{A}}(S_{a}\cap S_{Q^{\prime}})$

end while

return $S_{a}$

$\textit{Reach}_{\mathcal{A}}^{\infty}(Q^{\prime})$ (described in Algorithm 3)
is the set of states that can infinitely many times reach a location in
$Q^{\prime}$. We can use this to calculate the set of states, from which there
is a possible accepting run: Given tba $\mathcal{A}$ we write
$\textit{Reach}_{\mathcal{A}}^{\infty}$ as a shorthand for
$\textit{Reach}_{\mathcal{A}}^{\infty}(\mathcal{F})$, where $\mathcal{F}$ is
the set of accepting locations of $\mathcal{A}$.

######  Theorem 6.2.

Given tba $\mathcal{A}$. Then
$\textit{Reach}_{\mathcal{A}}^{\infty}=S_{\mathcal{A}}^{\textit{ne}}$.

Using this fixpoint, we can do online monitoring given $\mathcal{A}$ and
$\overline{\mathcal{A}}$ by storing the state estimate given by a finite timed
word over $\mathcal{A}$ and $\overline{\mathcal{A}}$, while continuously
checking if the state estimates still overlap with
$S_{\mathcal{A}}^{\textit{ne}}$ and $S_{\overline{\mathcal{A}}}^{\textit{ne}}$
respectively. If both state estimates still have non-empty languages, then the
verdict is ?, but if all the states in the state estimate of $\mathcal{A}$
have empty languages, then the verdict is $\bot$ ($\top$ for
$\overline{\mathcal{A}}$).

Algorithm 4 Get the set of possible successor states from $S$ after an input
$(\alpha,t)$

tba $\mathcal{A}=(Q,Q_{0},\Sigma,C,\Delta,\mathcal{F})$, a set of symbolic
states $S$ and a timed input $(\alpha,t)\in\Sigma\times\mathbb{R}_{\geq 0}$

$\textit{Succ}_{\mathcal{A}}^{S}(\alpha,t)$

$\textit{Successors}\leftarrow\varnothing$

for $(q,Z)\in S$ do

for $(q,q^{\prime},\alpha,\lambda,g)\in\Delta$ do

if $Z^{\nearrow_{[t,t]}}\models g$ then

$\textit{Successors}\leftarrow\textit{Successors}\cup\\{(q^{\prime},(Z^{\nearrow_{[t,t]}}\land
g)[\lambda])\\}$

end if

end for

end for

return Successors

Given the procedure $\textit{Succ}_{\mathcal{A}}$ described in Algorithm 4 we
can compute the state estimate of $\mathcal{A}$ over a finite timed word
$\rho\in T\\!\Sigma^{*}$ of length $n$ iteratively. If $S_{0}$ is the set of
initial states then
$S_{n}=\textit{Succ}_{\mathcal{A}}^{S_{n-1}}(\alpha_{n},t_{n})=\mathcal{T}_{\mathcal{A}}(\rho)$
is the state estimate after $\rho$.

Algorithm 5 Online monitoring procedure given $\mathcal{A}_{\phi}$ and
$\mathcal{A}_{\overline{\phi}}$. Gives a verdict $\top$, $\bot$ or ? after
each input

$\textit{time}\leftarrow 0$

$\mathcal{A}\leftarrow\mathcal{A}_{\phi}\otimes\mathcal{A}_{\textit{D}}$

$\overline{\mathcal{A}}\leftarrow\mathcal{A}_{\overline{\phi}}\otimes\mathcal{A}_{\textit{D}}$

$S\leftarrow\\{(q,Z_{0}):q\textit{ is an initial location of }\mathcal{A}\\}$

$\overline{S}\leftarrow\\{(q,Z_{0}):q\textit{ is an initial location of
}\overline{\mathcal{A}}\\}$

loop

Receive new input: $(\alpha,t)\in\Sigma\times\mathbb{R}_{\geq 0}$

$S\leftarrow\textit{Succ}_{\mathcal{A}}^{S}(\alpha,t-\textit{time})$ // Update
state estimate

$\overline{S}\leftarrow\textit{Succ}_{\overline{\mathcal{A}}}^{\overline{S}}(\alpha,t-\textit{time})$

$\textit{time}\leftarrow t$

if $S\cap\textit{Reach}_{\mathcal{A}}^{\infty}=\emptyset$ then

output $\bot$

else if
$\overline{S}\cap\textit{Reach}_{\overline{\mathcal{A}}}^{\infty}=\emptyset$
then

output $\top$

else

output ?

end if

end loop

An overview of the online monitoring procedure (see Algorithm 5) with
$\mathcal{A}_{\phi}$ and $\mathcal{A}_{\overline{\phi}}$ is as follows. First
we define $\mathcal{A}$ and $\overline{\mathcal{A}}$ as the intersection of
each input automata with $\mathcal{A}_{\textit{D}}$. We then use the backwards
reachability algorithm to compute the set of states that have a non-empty
language (in each tba). While continuously receiving inputs, we compute the
symbolic successor states from the initial states. After each input, we check
if there is an overlap between the states with a non-empty language, and the
state estimates and output a verdict. The verdict is either $\top$ or $\bot$
when one of the state estimates falls outside the set of states with a non-
empty language and ? otherwise.

(a) State space of $\mathcal{A}$

(b) State spaces of $\overline{\mathcal{A}}$

Figure 6: Illustration of the state spaces in Algorithm 5 given a timed word
$\rho$. The grey areas are the states with a non-empty language
$\textit{Reach}_{\mathcal{A}}^{\infty}$ and
$\textit{Reach}_{\overline{\mathcal{A}}}^{\infty}$. The black areas are the
state-estimates after $\rho$, i.e. $\mathcal{T}_{\mathcal{A}}(\rho)$ and
$\mathcal{T}_{\overline{\mathcal{A}}}(\rho)$.

Figure 6 shows an example of the state space, with the non-empty states marked
as grey and the current state estimates marked as black. In this example the
verdict would be ?, since both state estimates overlap with the set of states
with a non-empty language.

######  Example 4.

Consider the mitl formula $\varphi=G(a\rightarrow F_{\leq 30}b)$ from Example
1. We are given the tba $\mathcal{A}$ in Figure 1 and its complement
$\overline{\mathcal{A}}$, the tba for $\overline{\varphi}=F(a\wedge G_{\leq
30}\neg b)$ shown in Figure 7. As before, we draw the sink state
$\overline{q_{4}}$ here for illustrative purposes. If we were to monitor
$\mathcal{L}(\varphi)$, the first step would be to take the intersections
$\mathcal{A}\otimes\mathcal{A}_{\textit{D}}$ and
$\overline{\mathcal{A}}\otimes\mathcal{A}_{\textit{D}}$, but we skip that here
because of the size of the resulting automata.

$\overline{q_{1}}$$\overline{q_{2}}$$\overline{q_{3}}$$\overline{q_{4}}$$a,b,c$$a$$y\colonequals
0$$a,c$$a,b,c$$y>30$$a,b,c$$b$$y\leq 30$$a,b,c$ Figure 7: tba corresponding to
$F(a\wedge G_{\leq 30}\neg b)$

Now suppose the finite prefix $\rho_{\text{ok}}=(a,10),(b,20)$ as seen in
Example 1. We compute the state estimate for $\mathcal{A}$ as
$\mathcal{T}_{\mathcal{A}}(\rho_{\text{ok}})=\\{\ (q_{1},\\{x=10\\})\ \\}$ and
for $\overline{\mathcal{A}}$ as
$\mathcal{T}_{\overline{\mathcal{A}}}(\rho_{\text{ok}})=\\{\
(\overline{q_{1}},\\{y=20\\}),(\overline{q_{4}},\\{y=10\\})\ \\}$ where
$\\{c=v\\}$ represents the symbolic constraints on the clocks of the tba.
Although the algorithm uses a symbolic representation for the state estimates,
for a concrete input the clock constraints are equalities. Note that, for
$\overline{\mathcal{A}}$, there are two possible states for $\rho_{\text{ok}}$
since $\overline{\mathcal{A}}$ is non-deterministic. For the other Example 1
prefix, $\rho_{\text{bad}}=(a,10),(b,50)$,
$\mathcal{T}_{\mathcal{A}}(\rho_{\text{bad}})=\\{\ (q_{3},\\{x=40\\})\ \\}$
and $\mathcal{T}_{\overline{\mathcal{A}}}(\rho_{\text{bad}})=\\{\
(\overline{q_{1}},\\{y=50\\}),(\overline{q_{3}},\\{y=40\\})\ \\}$.

##  7 Time Uncertainty

So far, we have assumed that we can measure the real-valued time-points
$\tau_{i}$ appearing in a finite timed word with arbitrary mathematical
precision. Given that our monitor has to be implemented as an algorithm, this
cannot necessarily be achieved. To ensure implementability, we rather assume
that the time-points are observed with a certain precision. More precisely, we
assume that we observe some integer-bounded interval $I_{i}$ containing
$\tau_{i}$, e.g. $[\lfloor\tau\rfloor,\lceil\tau\rceil]$. In related settings,
concrete timing information may be missing for many reasons, particularly when
monitoring distributed systems [19, 30, 28]. The problem we consider is also
closely related to the robustness of ta [15] as well as work on monitoring
over unreliable channels [20, 21].

We assume that during monitoring, we observe a _symbolic_ timed word of the
form $\rho_{s}=(\sigma,\upsilon)$, where $\sigma$ is a finite word over the
symbol alphabet $\Sigma$ and $\upsilon$ is a sequence of time intervals
$I_{1},I_{2},\ldots,I_{n}$ of the same length as $\sigma$. Each time interval
$I_{i}$ is a pair of natural numbers $[l_{i},u_{i}]$ ($l_{i}<u_{i}$)
representing a lower and upper bound of the real-valued time-point, when the
symbol $\sigma_{i}$ occurred. The set of finite symbolic timed words is
denoted $T\\!\\!\vbox{\hbox{{\tiny{S}}}}\Sigma^{*}$. We limit bounds in
symbolic timed words to natural numbers which is equivalent to supporting
rationals with a fixed granularity.

Semantically a symbolic timed word
$\rho_{s}=(\sigma,I_{1},I_{2},\ldots,I_{n})$ covers all timed words
$(\sigma,\tau)$ where $\tau_{i}\in I_{i}$. We write $\rho\sqsubseteq\rho_{s}$.
Also, whenever $\rho_{s}=(\sigma,I_{1},I_{2},\ldots,I_{n})$ and
$\rho^{\prime}_{s}=(\sigma,J_{1},J_{2},\ldots,J_{n})$ are two symbolic timed
words, we write $\rho_{s}\sqsubseteq\rho^{\prime}_{s}$ if $I_{i}\subseteq
J_{i}$ for all $i=1\ldots n$.

Now monitoring a language of timed infinite words in the setting of timing
uncertainty refines timed monitoring in the following way. Given a finite
symbolic prefix, it is checked whether all concrete realization of this prefix
determine the property. That is whether all possible infinite extensions of
such a concrete realization is included in the monitored property. More
formally:

######  Definition 8 (Monitoring with timing uncertainty).

Given a language of infinite timed words $\phi\subseteq T\\!\Sigma^{\omega}$
and a finite symbolic timed word $\rho_{s}\in
T\\!\\!\vbox{\hbox{{\tiny{S}}}}\Sigma^{*}$, the function
$\mathcal{V}_{U}:2^{T\\!\Sigma^{\omega}}\rightarrow
T\\!\\!\vbox{\hbox{{\tiny{S}}}}\Sigma^{*}\rightarrow\mathbb{B}_{3}$ evaluates
to a verdict with the following definition:

$\mathcal{V}_{U}(\phi)(\rho_{s})=\left.\begin{cases}\top&\text{if
}\rho\cdot\mu\in\phi\ $ for all $\rho\sqsubseteq\rho_{s}$ and all $\mu\in
T\\!\\!\vbox{\hbox{{\tiny{D}}}}\Sigma^{\omega},\\\ \bot&\text{if
}\rho\cdot\mu\notin\phi\ $ for all $\rho\sqsubseteq\rho_{s}$ and all $\mu\in
T\\!\\!\vbox{\hbox{{\tiny{D}}}}\Sigma^{\omega},\\\
\textbf{{?}}&\text{otherwise}.\end{cases}\right.$

We note that if $\rho_{s}\sqsubseteq\rho^{\prime}_{s}$ then
$\mathcal{V}_{U}(\phi)(\rho_{s})\sqsubseteq\mathcal{V}_{U}(\phi)(\rho^{\prime}_{s})$.

######  Example 5.

Consider the mitl property $F_{[5,6]}a$, and the concrete timed word
$\rho=(b,1.2),(a,5.4),(c,7.3)$. Assume that we observe time-points as integer-
bounded intervals of length 1 respectively 2 reflected by the following two
symbolic timed words $\rho_{s}^{1}=(b,[1,2]),(a,[5,6]),(c,[7,8])$ and
$\rho_{s}^{2}=(b,[1,3]),(a,[5,7]),\\\ (c,[7,9])$. Now
$\mathcal{V}(F_{[5,6]})a)(\rho)=\top$ and
$\mathcal{V}_{U}(F_{[5,6]})a)(\rho_{s}^{1})=\top$ whereas
$\mathcal{V}_{U}(F_{[5,6]})a)(\rho_{s}^{2})=\bot$.

To obtain a monitoring algorithm for monitoring under timing uncertainty it
merely requires that the symbolic successor computation of Algorithm 4 is
extended to pairs $(\alpha,I)$ where $I$ is an integer-bounded interval. Thus
Algorithm 5 can easily be extended to support time uncertainty.

##  8 Time Predictive Monitoring

In the timed setting studied in this paper, we want to refine the rather
uninformative verdict ? that occurs during monitoring to provide guaranteed
minimum times before a positive or negative verdict can be made.

######  Example 6.

Consider the mitl property $F_{[20,40]}b$. Monitoring the finite timed word
$\rho=(a,5.1),(c,21.0),(c,30.4),(b,35.1),(a,40.2)$ will result in three ?
verdicts followed by the verdict $\top$ when $(b,35.1)$ is read. However, we
may offer significantly more information, e.g. when reading $(a,5.1)$ it is
clear that at least $14.9$ time-units must elapse before we can claim that the
property holds, and at least $34.9$ time-units must elaps before we can claim
that it does not hold.

######  Definition 9 (Time Predictive Monitor Verdicts).

Given a language of infinite timed words $\phi\subseteq T\\!\Sigma^{\omega}$
and a finite timed word $\rho\in T\\!\Sigma^{*}$, the function
$\mathcal{V}_{T}:2^{T\\!\Sigma^{\omega}}\rightarrow
T\\!\Sigma^{*}\rightarrow\mathbb{R}_{\geq 0}^{2}$ evaluates to the verdict
$\mathcal{V}_{T}(\phi)(\rho)=(D^{\rho}_{\phi},D^{\rho}_{\overline{\phi}})$,
where:

$\displaystyle D^{\rho}_{\phi}$
$\displaystyle=\inf\big{\\{}\tau(\rho^{\prime}):\rho^{\prime}\in
T\\!\Sigma^{*}\text{ such that }\forall\mu\in
T\\!\\!\vbox{\hbox{{\tiny{D}}}}\Sigma^{\omega}\raisebox{-1.07639pt}{\scalebox{1.6}{.}}{\
}\rho\cdot\rho^{\prime}\cdot\mu\in\phi\big{\\}}$ $\displaystyle
D^{\rho}_{\overline{\phi}}$
$\displaystyle=\inf\big{\\{}\tau(\rho^{\prime}):\rho^{\prime}\in
T\\!\Sigma^{*}\text{ such that }\forall\mu\in
T\\!\\!\vbox{\hbox{{\tiny{D}}}}\Sigma^{\omega}\raisebox{-1.07639pt}{\scalebox{1.6}{.}}{\
}\rho\cdot\rho^{\prime}\cdot\mu\not\in\phi\big{\\}}$

where $\tau(\rho^{\prime})$ denotes the time duration of $\rho^{\prime}$.

(a) State space of $\mathcal{A}$

(b) State space of $\overline{\mathcal{A}}$

Figure 8: Illustration of the state spaces while monitoring given the inputs
$\mathcal{A}$ and $\overline{\mathcal{A}}$ and a timed word $\rho$. This
figure is a refinement of Figure 6. In particular the states with a non-empty
language, e.g. $\textit{Reach}_{\mathcal{A}}^{\infty}$, has been divided into
two subsets: the set of states that can reach outside
$\textit{Reach}_{\mathcal{A}}^{\infty}$ (darker grey indicating larger infimum
reachability time) and the states that cannot (darkest grey). The black areas
are the state-estimates after $\rho$, i.e. $\mathcal{T}_{\mathcal{A}}(\rho)$
and $\mathcal{T}_{\overline{\mathcal{A}}}(\rho)$.

The intuition behind Definition 9 is illustrated in Figure 8. We note that
when $\mathcal{V}(\phi)(\rho)=\top$ then
$\mathcal{V}_{T}(\phi)(\rho)=(0,+\infty)$. Dually, when
$\mathcal{V}(\phi)(\rho)=\bot$ then $\mathcal{V}_{T}(\phi)(\rho)=(+\infty,0)$.
We note however, that the opposite implications do not hold. As an example
consider the property $F_{\geq 5}b$ and the finite timed word $\rho=(c,6)$.
Then clearly $\mathcal{V}_{T}(\phi)(\rho)=(0,+\infty)$ but
$\mathcal{V}(\phi)(\rho)\not=\top$.

To make steps toward a time predicting monitoring algorithm, we assume that
the property $\phi$ (as well as $\overline{\phi}$) can be captured by a TBA
$\mathcal{A}$. During monitoring, we constantly check whether the state
estimate $\mathcal{T}_{\mathcal{A}}(\rho)$ of the current prefix word $\rho$
intersects the set of states with non-empty language, i.e.
$\textit{Reach}_{\mathcal{A}}^{\infty}$. Now
$R_{\mathcal{A}}=\textit{Reach}_{\mathcal{A}}(\overline{\textit{Reach}_{\mathcal{A}}^{\infty}})$
describes the set of states that can reach a state with an empty language. By
extending the TBA $\mathcal{A}$ with a fresh clock $z$, the extended set
$R_{\mathcal{A}}^{z}=\textit{Reach}_{\mathcal{A}^{z}}(\overline{\textit{Reach}_{\mathcal{A}^{z}}^{\infty}}\wedge(z=0))$
captures in a symbolic way the time required to reach a state with an empty
language222Similar to a method in [12] for time-optimal strategies.. In
particular $d_{\mathcal{A}}(q,v)=\inf\\{v_{z}:(q,v,v_{z})\in
R_{\mathcal{A}}^{z}\\}$ is the infimum reachability time for a state $(q,v)\in
R_{\mathcal{A}}$. For $S$ a set of states, we define $d_{\mathcal{A}}(S)$ to
be the supremum of $d_{\mathcal{A}}(q,v)$ over all $(q,v)\in S$. Now we claim
the following Theorem, pointing to an effective way of providing guaranteed
minimum time predictions of positive and negative verdicts during monitoring.

######  Theorem 8.1.

Let $\phi\subseteq T\\!\Sigma^{\omega}$ be a language of infinite timed words.
Assume that $\phi$ is accepted by a TBA $\mathcal{A}_{\phi}$ and the
complement $\overline{\phi}$ is accepted by a TBA
$\mathcal{A}_{\overline{\phi}}$. Then the following holds:

$d_{\mathcal{A}_{\phi}}(\mathcal{T}_{\mathcal{A}_{\phi}}(\rho))\leq
D^{\rho}_{\phi}\,\,\,\,\textit{ and
}\,\,\,\,d_{\mathcal{A}_{\overline{\phi}}}(\mathcal{T}_{\mathcal{A}_{\overline{\phi}}}(\rho))\leq
D^{\rho}_{\overline{\phi}}$

Moreover, if $\mathcal{A}_{\phi}$ ($\mathcal{A}_{\overline{\phi}}$) is
deterministic the first (second) inequality is an equality.

##  9 Conclusion

In this work, we have revisited the online monitoring problem for timed
properties. We presented an efficient online monitoring algorithm for
languages of infinite timed words. We require the language and its complement
to be expressed as tba, a requirement that is, for example, satisfied for
languages specified in the logic mitl. Hence our method is applicable in many
realistic scenarios.

We showed how to account for time divergence which prior work did not readily
seem to support. We also introduced two extensions to our method: support for
time uncertainty in the time sequence observed by the monitor, and time
predictions that refine the unknown verdict. By supporting time uncertainty in
the observed input, we account for real-world systems where the real-valued
time-points of events can only be observed up to a given precision. This
limits the soundness of verdicts from monitors that support only concrete
timed traces. Time predictions refine the mostly unhelpful unknown verdict to
provide extra information on the possible time-to-failure of the monitored
system. For nondeterministic tba we show how to compute an under-approximation
which is exact in the case of deterministic automata. In the future, we will
investigate the existence of an exact algorithm for the general case.

While our work was designed to facilitate implementation, this has not yet
been completed. Our planned implementation will be distributed in the form of
a C++ library with facilities to read tba in the UPPAAL xml format [23] that
is output by tools like Casaal [24] and MightyL [9]. We also plan to integrate
the tool into UPPAAL SMC [14] to replace the current rewrite-based Weighted
mtl implementation [11].

Further improvements to our monitoring algorithm include improved support for
uncertainties in the input and additional analysis of timed properties. One
direction in which we plan to extend the work is to support unobservable
symbols in the monitor alphabet. This can be logically extended to consider
arbitrary mutations to an input sequence modeled in the form of ta. We also
plan to provide a method to compute the monitorability of a timed property.

## References

  * [1] Alur, R., Dill, D.L.: A theory of timed automata. Theoretical Computer Science 126(2), 183–235 (1994). https://doi.org/10.1016/0304-3975(94)90010-8
  * [2] Alur, R., Feder, T., Henzinger, T.A.: The benefits of relaxing punctuality. Journal of the ACM 43(1) (01 1996)
  * [3] Baldor, K., Niu, J.: Monitoring dense-time, continuous-semantics, metric temporal logic. In: Runtime Verification. pp. 245–259. Springer Berlin Heidelberg (2013). 10.1007/978-3-642-35632-2_24
  * [4] Basin, D., Klaedtke, F., Müller, S., Pfitzmann, B.: Runtime monitoring of metric first-order temporal properties. In: IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science. LIPIcs, vol. 2, pp. 49–60. Schloss Dagstuhl (2008). 10.4230/LIPIcs.FSTTCS.2008.1740
  * [5] Basin, D., Klaedtke, F., Zălinescu, E.: Algorithms for monitoring real-time properties. In: RV. pp. 260–275. Springer (2012). 10.1007/978-3-642-29860-8_20
  * [6] Bauer, A., Leucker, M., Schallhart, C.: Monitoring of real-time properties. In: Arun-Kumar, S., Garg, N. (eds.) FSTTCS 2006: Foundations of Software Technology and Theoretical Computer Science. pp. 260–272. Springer, Berlin, Heidelberg (2006). 10.1007/11944836_25
  * [7] Bauer, A., Leucker, M., Schallhart, C.: Runtime verification for LTL and TLTL. ACM Transactions on Software Engineering and Methodology (TOSEM) 20(4), 14:1–14:64 (9 2011). 10.1145/2000799.2000800
  * [8] Bengtsson, J., Yi, W.: Timed automata: Semantics, algorithms and tools. In: Lectures on Concurrency and Petri Nets, Advances in Petri Nets. LNCS, vol. 3098, pp. 87–124. Springer (2003). 10.1007/978-3-540-27755-2_3
  * [9] Brihaye, T., Geeraerts, G., Ho, H.M., Monmege, B.: MightyL: A compositional translation from MITL to timed automata. In: Computer Aided Verification. pp. 421–440. Springer (2017). 10.1007/978-3-319-63387-9_21
  * [10] Bulychev, P., David, A., Guldstrand Larsen, K., Legay, A., Li, G., Bøgsted Poulsen, D., Stainer, A.: Monitor-based statistical model checking for weighted metric temporal logic. In: Logic for Programming, Artificial Intelligence, and Reasoning. pp. 168–182. Springer (2012). 10.1007/978-3-642-28717-6_15
  * [11] Bulychev, P., David, A., Larsen, K.G., Legay, A., Li, G., Poulsen, D.B.: Rewrite-based statistical model checking of WMTL. In: Runtime Verification. pp. 260–275. Springer (2013). 10.1007/978-3-642-35632-2_25
  * [12] Cassez, F., David, A., Fleury, E., Larsen, K.G., Lime, D.: Efficient on-the-fly algorithms for the analysis of timed games. In: CONCUR 2005 - Concurrency Theory. LNCS, vol. 3653, pp. 66–80. Springer (2005). 10.1007/11539452_9
  * [13] Chattopadhyay, A., Mamouras, K.: A verified online monitor for metric temporal logic with quantitative semantics. In: Runtime Verification. pp. 383–403. Springer (2020). 10.1007/978-3-030-60508-7_21
  * [14] David, A., Larsen, K.G., Legay, A., Mikučionis, M., Wang, Z.: Time for statistical model checking of real-time systems. In: Computer Aided Verification. pp. 349–355. Springer (2011)
  * [15] De Wulf, M., Doyen, L., Markey, N., Raskin, J.F.: Robust safety of timed automata. Formal Methods in System Design 33(1), 45–84 (Dec 2008). 10.1007/s10703-008-0056-7
  * [16] Finkbeiner, B., Kuhtz, L.: Monitor circuits for LTL with bounded and unbounded future. In: Runtime Verification. pp. 60–75. Springer (2009). 10.1007/978-3-642-04694-0_5
  * [17] Geilen, M., Dams, D.: An on-the-fly tableau construction for a real-time temporal logic. In: Formal Techniques in Real-Time and Fault-Tolerant Systems. pp. 276–290. Springer (2000). 10.1007/3-540-45352-0_23
  * [18] Ho, H.M., Ouaknine, J., Worrell, J.: Online monitoring of metric temporal logic. In: Runtime Verification. pp. 178–192. Springer (2014). 10.1007/978-3-319-11164-3_15
  * [19] Jahanian, F., Rajkumar, R., Raju, S.C.V.: Runtime monitoring of timing constraints in distributed real-time systems. Real-Time Systems 7(3), 247–273 (Nov 1994). 10.1007/BF01088521
  * [20] Kauffman, S., Havelund, K., Fischmeister, S.: Monitorability over unreliable channels. In: International Conference on Runtime Verification (RV’19). LNCS, vol. 11757, pp. 256–272. Springer (2019). 10.1007/978-3-030-32079-9_15
  * [21] Kauffman, S., Havelund, K., Fischmeister, S.: What can we monitor over unreliable channels? International Journal on Software Tools for Technology Transfer 23, 579–600 (06 2021). 10.1007/s10009-021-00625-z
  * [22] Koymans, R.: Specifying real-time properties with metric temporal logic. Real-Time Systems 2(4), 255–299 (Nov 1990). 10.1007/BF01995674
  * [23] Larsen, K.G., Mikucionis, M., Nielsen, B.: Online testing of real-time systems using Uppaal. In: Formal Approaches to Software Testing. LNCS, vol. 3395, pp. 79–94. Springer (2004). 10.1007/978-3-540-31848-4_6
  * [24] Li, G., Jensen, P.G., Larsen, K.G., Legay, A., Poulsen, D.B.: Practical controller synthesis for mtl0,∞. In: Int. SPIN Symposium on Model Checking of Software. pp. 102–111. SPIN 2017, ACM (2017). 10.1145/3092282.3092303
  * [25] Lindahl, M., Pettersson, P., Yi, W.: Formal design and analysis of a gear controller. In: Steffen, B. (ed.) Tools and Algorithms for Construction and Analysis of Systems (TACAS). LNCS, vol. 1384, pp. 281–297. Springer (1998). 10.1007/BFb0054178
  * [26] Moosbrugger, P., Rozier, K.Y., Schumann, J.: R2u2: monitoring and diagnosis of security threats for unmanned aerial systems. Formal Methods in System Design 51(1), 31–61 (Aug 2017). 10.1007/s10703-017-0275-x
  * [27] Ničković, D., Piterman, N.: From mtl to deterministic timed automata. In: Formal Modeling and Analysis of Timed Systems. pp. 152–167. Springer Berlin Heidelberg (2010). 10.1007/978-3-642-15297-9_13
  * [28] Pike, L.: A note on inconsistent axioms in Rushby’s "Systematic formal verification for fault-tolerant time-triggered algorithms". IEEE Transactions on Software Engineering 32(5), 347–348 (May 2006)
  * [29] Pnueli, A., Zaks, A.: PSL model checking and run-time verification via testers. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM 2006: Formal Methods. pp. 573–586. Springer, Berlin, Heidelberg (2006). 10.1007/11813040_38
  * [30] Rushby, J.: Systematic formal verification for fault-tolerant time-triggered algorithms. IEEE Transactions on Software Engineering 25(5), 651–660 (1999). 10.1109/32.815324
  * [31] Thati, P., Roşu, G.: Monitoring algorithms for metric temporal logic specifications. Electronic Notes in Theoretical Computer Science 113, 145–162 (2005). 10.1016/j.entcs.2004.01.029, proceedings of the Fourth Workshop on Runtime Verification (RV 2004)
  * [32] Ulus, D., Ferrère, T., Asarin, E., Maler, O.: Timed pattern matching. In: Formal Modeling and Analysis of Timed Systems. pp. 222–236. Springer (2014). 10.1007/978-3-319-10512-3_16
  * [33] Ulus, D., Ferrère, T., Asarin, E., Maler, O.: Online timed pattern matching using derivatives. In: Tools and Algorithms for the Construction and Analysis of Systems. pp. 736–751. Springer (2016). 10.1007/978-3-662-49674-9_47