POLIMON: Checking Temporal Properties over Out-of-order Streams at Runtime
Felix Klaedtke
LaTeX2e




 
  stmryboldUstmrymn 
                                              
 


 
  
  
  
  
 



  calc,shapes,arrows

 










CASE[1]
      
      
      
      
      
      
    
  
  #1

























  





















 
 
 









































































   
                    

 
                  

 
                  


 



Umathb45
Umathbmn
      <5> <6> <7> <8> <9> <10> gen * mathb
      <10.95> mathb10 <12> <14.4> <17.28> <20.74> <24.88> mathb12
      
mathbUmathbmn


⊏3mathb"80
⊑3mathb"84
3mathb"88
































time-stamp
time-stamps
time-stamped
time-stamp-ing



headings





Klaedtke
NEC Laboratories Europe, Heidelberg





: Checking Temporal Properties over Out-of-order Streams at Runtime
    Felix Klaedtke
    —
===================================================================




  This paper presents the monitoring tool  for checking
  system behavior at runtime against specifications expressed as
  formulas in the real-time logic MTL or its extension with the freeze
  quantifier.  The tool's distinguishing feature is that 
  can receive messages describing the system events out of order.
  Furthermore, since  processes received messages
  immediately, it outputs verdicts promptly when a message's described
  system event leads to a violation of the specification.  This makes
  the tool well suited, e.g., for verifying the behavior of
  distributed systems with unreliable channels at runtime.







§ INTRODUCTION



Monitoring system behavior and checking it during runtime is widely
used for a diversity of systems and properties.  An important class of
properties are requirements on the temporal occurrence and
nonoccurrence of system events.  For instance, requests must be served
within a given time period and a failed login must not be directly
followed by another login attempt.  Linear-time temporal logics like
LTL or variants and extensions thereof are well suited to formally
express such requirements and various online algorithms have been
developed for them for the verification of system behavior at runtime,
see,
e.g., <cit.>.


A major challenge in checking system behavior at runtime is when the
system under scrutiny is composed of several interacting, distributed
components <cit.>.
Most of today's IT systems are of this form.  For instance, the
observations of a monitor may only be partial or received out-of-order
because of network latencies or system component failures.  Note that
related challenges arise in stream processing applications where data
must be queried or aggregated in real time, is not necessarily
complete, and may be received in an order different from is
generation <cit.>.






  
Contributions.

In this paper, we present the tool  for monitoring
out-of-order event streams.  Concretely, the tool's objective is to
determine at runtime whether system behavior, as observed and reported
by system components, satisfies or violates a given specification.
 handles specifications expressed as formulas in the
real-time logic MTL and its extension with the freeze quantifier
 (pronounced “MTL freeze”). The freeze quantifier allows
one to bind logical variables to data values occurring in an event.  A
cornerstone of 's underlying monitoring
approach <cit.> is a three-valued
semantics for MTL and  that is well suited to reason in
settings where system components communicate with the monitors over
unreliable channels.  's reported verdicts are sound and
complete with respect to the tool's partial knowledge about the system
behavior.


 operates as follows.  It receives as input timestamped
messages from the system components that describe the system events.
No assumptions are made on the order in which these messages are
received.

For each received message,  updates its state.  This state
comprises an acyclic graph structure for reasoning about the system
behavior, that is, computing verdicts about the monitored
specification's fulfillment.  The graph's nodes store the truth values
of the subformulas for the different times with data values frozen to
logical variables, including the times with no or only partial
knowledge.   refines the graph when receiving information
about a specific point in time in form of events.
In each such update, data values are propagated down to the graph's
leaves and Boolean truth values for subformulas are propagated up
along the graph's edges.  When a Boolean truth value is propagated to
a root node of the graph,  outputs the corresponding
verdict.

 is significantly faster than its
predecessor <cit.>.  The speedup is
rooted in various algorithmic improvements on maintaining the graph
structure.  Furthermore,  utilizes multiple CPU cores by
processing the received messages in a pipeline.   also
supports new features.  For instance,  can export and import
its internal state, which are crucial operations for
migrating monitors.   also implements different approaches
for closing knowledge gaps.







  
Related Tools.

Various monitoring tools have been developed within the
runtime-verification community over the last years, for instance,
EAGLE <cit.>, MOP <cit.>,
BeepBeep <cit.>, MONPOLY <cit.>, AMT <cit.>,
Montre <cit.>, and StreamLAB <cit.>, each with
unique features.  Many of these tools handle—as
—spe­ci­fi­ca­tions expressed in some formalism that extends the
linear-time temporal logic LTL.

Metric constraints are, e.g., supported by the tools MONPOLY, AMT,
Montre, and .

EAGLE and  both support the freeze quantifier to reason
about the events' data values.  Freeze quantification in turn is a
weak form of first-order quantification, which is supported by
BeepBeep and MONPOLY.  Note that the MOP framework also supports some
reasoning about data by slicing the traces according to the events'
data values.

There are, however, often subtle differences in the tools' underlying
time models and the semantics of their specification languages.
Concretely, the semantics of 's specification language uses a
three-valued semantics, which conservatively approximates the
classical Boolean semantics.  's unique feature is that it
soundly and completely deals with knowledge gaps.






  
Organization.

The remainder of this paper is structured as follows.  In
Section <ref>, we provide an overview of the tool.  In
Section <ref>, we report on the tool's performance.  Finally,
in Section <ref>, we draw conclusions.




§  IN A NUTSHELL



's input comprises (1) a specification and (2) event streams
from the monitored system components.  See also
Figure <ref>.   processes the incoming events,
which it either receives over a UDP socket or reads from a file,
iteratively and checks them against the specification, which is a
formula in the real-time logic
MTL <cit.>
extended with the freeze quantifier.

 does not require that the events are received in the order
in which they are generated.  Each event is processed immediately,
that is,  interprets the incoming message that describes the
event, updates the monitor state, and outputs the computed verdicts.


We proceed by first illustrating 's usage through a simple
example before we describe the tool's theoretical underpinnings and
its main components, including some details on their implementation.




 §.§ Example


Consider a system in which agents can issue tickets. Issuing a ticket
is represented by an event 𝑡𝑖𝑐𝑘𝑒𝑡(a,n), where a is the
agent who issued the ticket and n is the ticket
identifier. Furthermore, consider the simple specification that an
agent must wait for some time (e.g. 100 milliseconds) before issuing
another ticket.  A formalization in 's specification language
is as follows.

    [             a[agent], n[𝑖𝑑].                  𝑡𝑖𝑐𝑘𝑒𝑡(a,n);                                                          ;                              (0,100𝑚𝑠] m[𝑖𝑑]. 𝑡𝑖𝑐𝑘𝑒𝑡(a,m) ]

The  quantifiers bind the logical variables to the data
values that occur in the events.  The data values are stored in
predefined registers (𝑎𝑔𝑒𝑛𝑡 and 𝑖𝑑 in the above
formula) and each event determines the register values at the event's
occurrence.  Note that the data values from an event bound by the
outer  quantifier in the above formula stem from an event
that is different from the one for the inner  quantifier,
since the metric constraint of the temporal future-time connective
 excludes 0.  Furthermore, note that an event also
determines the interpretation of the predicate symbol
𝑡𝑖𝑐𝑘𝑒𝑡 at the event's occurrence, namely, the singleton
{(a,n)}.

Finally, note that there is an implicit outermost temporal connective
.  For each received event, a reported verdict describes
whether the given specification is violated or satisfied at the
event's time.

 requires that events are timestamped (in Unix time with a
precision up to microseconds).   additionally requires that
each event includes the event's system component and a sequence
  number, i.e., the ith event of the component.   uses
the sequence numbers to determine whether it has received all events
from a component within a given time period.  For instance, when
 is monitoring a single component and it has received events
with the sequence number i and i+2 but no event with the sequence
number i+1, then  knows that there is a knowledge
  gap between the two events with the sequence numbers i and i+2.

For our example, assume that  is monitoring the single
component 𝚜𝚢𝚜𝚌𝚘𝚖𝚙 and receiving the following events from
it.

    [   1548694551.904@[𝚜𝚢𝚜𝚌𝚘𝚖𝚙] (1): 𝑡𝑖𝑐𝑘𝑒𝑡(𝚊𝚕𝚒𝚌𝚎,34);      1548694551.996@[𝚜𝚢𝚜𝚌𝚘𝚖𝚙] (2): 𝑡𝑖𝑐𝑘𝑒𝑡(𝚋𝚘𝚋,8); 1548694552.059@[𝚜𝚢𝚜𝚌𝚘𝚖𝚙] (3): 𝑡𝑖𝑐𝑘𝑒𝑡(𝚌𝚑𝚊𝚛𝚕𝚒𝚎,52);     1548694552.084@[𝚜𝚢𝚜𝚌𝚘𝚖𝚙] (5): 𝑡𝑖𝑐𝑘𝑒𝑡(𝚋𝚘𝚋,11);  1548694552.407@[𝚜𝚢𝚜𝚌𝚘𝚖𝚙] (6): 𝑡𝑖𝑐𝑘𝑒𝑡(𝚌𝚑𝚊𝚛𝚕𝚒𝚎,1); 1548694552.071@[𝚜𝚢𝚜𝚌𝚘𝚖𝚙] (4): 𝑡𝑖𝑐𝑘𝑒𝑡(𝚌𝚑𝚊𝚛𝚕𝚒𝚎,99) ]

Note that the events are received in the order of their timestamps,
except the event with the sequence number 4 is received out of
order.  The delay of receiving this event might, e.g., be caused by
network latencies.  processes the events in the order it
receives them.

 does not output any verdict after receiving the first two
events.  When processing the third event,  outputs the
verdict

    𝑡𝑟𝑢𝑒@1548694551.904
       .

The reason is that enough time has elapsed for 𝚊𝚕𝚒𝚌𝚎 to
issue another ticket.  This inference is sound since no events are
missing up to the third event and the time difference between the
first event and the third event is larger than 100 milliseconds.

The next verdict  outputs is when processing the second
event with agent 𝚋𝚘𝚋:

    𝑓𝑎𝑙𝑠𝑒@1548694551.996
       .

Note that although there is a knowledge gap (the event with the
sequence number 4 is missing), outputting this verdict is sound,
since no matter how this gap is filled, the second event with
agent 𝚋𝚘𝚋 causes a violation of the specification for the
first event with agent 𝚋𝚘𝚋.

When receiving the second last event,  outputs the verdict

    𝑡𝑟𝑢𝑒@1548694552.084

but not the verdict 𝑡𝑟𝑢𝑒@1548694552.059.  Outputting the
latter verdict would not be sound because of the knowledge gap between
the events with sequence numbers 3 and 5.  In fact, the event,
which arrives late, causes a violation.  Finally, when receiving this
last event,  outputs the following two verdicts.

    [  𝑡𝑟𝑢𝑒@1548694552.071; 𝑓𝑎𝑙𝑠𝑒@1548694552.059 ]


We have used  in checking the interactions of components in
software-defined networks (SDN controllers, network applications, and
switches).  In particular,  receives events describing the
actions performed by the various network components, and checks in
real time, e.g., whether certain deadlines are met.  In case of
violations, components can be 




 §.§ Foundations


's theoretical underpinnings, which we summarize in the
following, are described in detail
in <cit.>.

Specifications are given as formulas in the real-time logics MTL or
.  's core syntax is given by the grammar

    [                                                       φ                                                     ::= |    p(x_1,…,x_n)  | ϕ |ϕ  ϕ | x_1[r_1],…,x_n[r_n]. ϕ |;                                                                                                                                             I ϕ | I ϕ |ϕ  I ϕ |ϕ  I ϕ , ]

where the x_is range over variable names, p ranges over the
predicate symbols, the r_is over register names, and I ranges over
intervals, e.g., [0,*) is the unbounded left-closed interval with
left bound 0.   supports various standard syntactic sugar,
which it unfolds.  For instance, ϕ  ψ abbreviates
( ϕ)  ψ and ϕ abbreviates
[0,*) ϕ.   also supports rigid predicates
like the ordering on integers, which we omit here for the sake of
brevity.


The semantics of the specification language follows intuitively the
classical point-based semantics for
MTL <cit.>.
However, for dealing with knowledge gaps, the semantics is not defined
over timed words but over so-called
observations <cit.>. Observations
are finite words in which knowledge gaps are made explicit.
Furthermore, the semantics is defined over three truth values ,
, and , which are interpreted as in strong Kleene
logic, namely, they are partially ordered ( is less than
 and , which are incomparable) and  stands for
true,  for false, and  for unknown.  The semantics
conservatively approximates the classical Boolean semantics.  We refer
to <cit.> for details.


The reason of using a nonstandard semantics is for providing both
soundness and completeness guarantees of the verdicts in the presence
of knowledge gaps.  Intuitively speaking, soundness means that
 only outputs a verdict when this verdict remains valid no
matter how gaps are filled later, and completeness means that
 outputs a verdict as soon as possible based on the already
received events.  We note that there is always at least one knowledge
gap, even when events are received inorder, namely, a  does
not know what events occur after the event with the largest timestamp.


 makes the following system assumptions.  First, a system's
behavior is described completely through infinitely many events. Note
that  does not require to receive all of them in the
limit. Second, the monitored system components are fixed and known to
.  Third, components do not send bogus events.

's underlying time model is based on wall-clock time.
 requires that the events' timestamps are unique and the
events are linearly ordered by their timestamps.  Note that this is a
strong requirement, since in particular for distributed systems,
events can actually only be partially ordered by logical clocks.  If
events are, however, only partially ordered, the reasoning becomes
significantly more difficult since a finite partially ordered trace
can have exponentially many interleavings.  Furthermore, we argue that
when events are generated at the speed of microseconds, existing
protocols like the Network Time Protocol (NTP) work well in practice
to synchronize clocks between distributed components.  This
justification becomes however questionable when events are generated
at a very high speed, e.g., in the low microsecond range or even in
the nanosecond range.




 §.§ Implementation Details



 is a command-line tool and written in the programming
language Go (<www.golang.org>).[ has not been
  opensourced.  However, for nonprofit use, it can be obtained freely
  under a source code license agreement from NEC Laboratories Europe
  GmbH.]  In the following, we provide an overview of its
implementation.

 processes incoming events in a pipeline, where the pipeline
stages are executed as separate goroutines.  See
Figure <ref>.

The first stage, the receiver, parses the incoming events.

The second stage, the interpreter, extracts the
event's data values, and determines the interpretation of the
predicate symbols at the events' time point via regular-expression
matching.

The third stage, the timeliner, determines based on the
events' sequence numbers the time periods for which all events have
been received.

The fourth stage, the monitor, computes the verdicts.

Finally, the fifth stage, the outputter, reports the verdicts.


 supports different implementations of these stages, e.g.,
receivers and outputters for different input and output formats.
 currently also comprises two monitors: one for MTL and one
for .  Furthermore,  implements multiple
timeliners: one in which events must be received inorder and two for
receiving events out of order.  The first one uses sequence numbers to
determine whether there are gaps between messages and the second one
uses watermark messages <cit.> to close gaps between
messages.  Watermark messages are control messages that are inserted
into the pipeline.  Another type of control messages that can be
inserted into the pipeline are messages for outputting the internal
states of the timeliner and the monitor.  The outputter is responsible
for writing the state as a JSON object into a file.



's key data structure is an acyclic graph that represents the
intermediate specification's fulfillment with respect to the partial
knowledge about the system behavior.  This graph can be understood as
a combinational circuit, which is refined for each received event.
Such a refinement comprises the steps of (1) splitting gates, (2) the
downward propagation of data values, which may create new gates, and
(3) the upward propagation of Boolean truth values.

The gates are arranged along three axes: The x-axis is the temporal
dimension, the y-axis the formula structure, and the z-axis the data
dimension (which is trivial for propositional formulas).  Each
variable assignment corresponds to a plane along the z-axis.

Figure <ref> illustrates this graph-based data
structure for (0,3] p by showing (a) the initial graph
that comprises a node for each subformula for the interval
[0,∞), and (b) the split when receiving an event with the
timestamp τ; Boolean values have not been propagated.

Note that in Figure <ref>(b) the initial knowledge
gap [0,∞) is split into a left and a right knowledge gap,
[0,τ) and (τ,∞), respectively. Furthermore, a time
point for the received event is added. The new intervals and the time
point inherit the nodes of the ancestor interval and the nodes' edges
are adjusted according to the semantics of the temporal connective and
its metric constraint.  The dashed edges are implicit. They are
derived by following the solid edges and the nodes' horizontal
successors or predecessors.  This small detail is actually critical
for 's performance (see Section <ref>): each node has
a single outgoing edge and splits are therefore more local.

After a split, Boolean truth values are propagated up along the edges.
There are several subtle cases for the propagation.  For instance, in
Figure <ref>(b), the propagation of a Boolean truth
value of the proposition p at time τ can only be carried out
when the metric constraint is valid, i.e., if τ≤3.




§ EXPERIMENTAL EVALUATION



In this section, we report on 's performance.  For the
experiments, we used a computer with an Intel Xeon 3.3 GHz CPU (four
physical cores).   was compiled with the Go compiler
version 1.13.x.

In a first set of experiments, we used the Timescale benchmark
suite <cit.>, which includes log generators for 20 temporal
parameterized propositional patterns with metric constraints.  We also
evaluated 's performance on out-of-order event streams that we
obtained from the ordered logs generated by Timescales by adding
artificial “arrival delays” to each event's timestamp.

The plots in Figure <ref> show 's running times
for a few Timescales patterns on ordered and out-of-order event
streams with different metric constraints.  For comparison, the plot
on the left-hand side of Figure <ref> includes the
running times of the MONPOLY tool.  Our results for the other
Timescales patterns are similar.

Overall, 's performance is competitive to MONPOLY's
performance on ordered logs.  Note that some patterns cannot be
handled by MONPOLY because of the tool imposes the syntactic
restriction that temporal future-time connectives must not be
unbounded.  Handling out-of-order event streams does not significantly
increase running times.  The reason is that most updates on the graph
structure are local and thus involve only a few nodes. Recall from
Section <ref> that each node has only a single
outgoing edge, which needs to be updated; the implicit edges in
contrast often follow from the single outgoing edge without further
computations.  We also measured the tools' memory usage.  In general,
memory usage is low for both tools.  's memory usage usually
increases slowly with the “out-of-orderness” in event streams.



In a second set of experiments, we used MTL and  formulas
expressing policies for handling suspicious financial transactions.
The formulas are similar to the ones used in previous evaluations of
monitoring
tools <cit.>.

We again generated event streams synthetically for different event rates
(i.e., events per second) and, similar as in the Timescales
experiments, we obtained out-of-order streams by adding artificial
arrival delays to each event's timestamp taken.  The delays were taken
from a normal distribution for different standard deviations.


The plots in Figure <ref> show the running times for the
formulas in Figure <ref>.  Note that the formulas vary in
their temporal and their data “complexity.”  For MTL, the running
times grow linearly with the event rate and the impact of receiving
events out of order is almost negligible.  This is in contrast to
, where running times grow nonlinearly and the impact on
out-of-order events can be significant.  As in the Timescales
experiments memory usage increases for out-of-order events.  However,
the increase is often moderate (usually  consumes less than
256 MB of RAM), except for the  out-of-order cases (P3)
and (P4) in which the running times also increase significantly.

For putting 's performance in relation, we also ran MONPOLY on
corresponding specifications over the ordered event streams.  For MTL,
 and MONPOLY show similar performance.  For ,
MONPOLY is in general significantly faster. (P3) is an exception as it
does not have an equivalent counterpart that can be handled by MONPOLY
and even for a variant of it, 


Figure <ref> provides detailed views on individual
 runs.  The plots on the left-hand side are for the MTL
formula (Q4) and the ones on the right-hand side are for the
 formula (P4).  Runs for the other formulas (P1)–(P3)
and (Q1)–(Q3) have similar characteristics.


The upper plots ((a) and (b)) show the running times of 's
pipeline stages for each event.  For MTL, the stages have similar
running times and each stage is usually executed in a fraction of a
millisecond.  The outliers are mainly caused by Go's garbage
collector.  For , the monitor stage dominates the running
times.

The middle plots ((c) and (d)) provide another view on the running
times of the pipeline stages. Namely, they show the percentages of a
stage that executed below a time for an event.  Observe that in the
MTL case almost every event is processed under 10μ𝑠 by
all stages, which is in contrast to the  case, where the
monitor stage takes around 1𝑚𝑠 for most events, whereas the
other stages take no longer than 10μ𝑠.  We also remark
that  in particular benefits in the MTL case from the
multiple CPU cores since the stages run concurrently with a similar
throughput.

The lower plots ((e) and (f)) show the sizes of the data structure.
For , the number of nodes in the data structure is
considerable larger than for MTL, which originates from the different
data values.  Observe that although the events are received out of
order, the size of the data structure stays in a certain bound.  This
bound increases when more events are received out of order and thus
more knowledge gaps are closed later.

Overall,  outperforms its predecessor prototype. It is often
five to ten times faster, sometimes even more,
cf. <cit.>. The implemented algorithms
also scale better, in particular, when events are received out of
order.




§ CONCLUSION





The  tool processes out-of-order event streams in real time,
promptly reports verdicts, and provides both soundness and
completeness guarantees.  The underlying monitoring approach and hence
also the tool make the tradeoff of requiring a linear order on system
events by their wall-clock timestamps instead of a partial order on
the events provided by logical clocks.

For MTL specifications,  handles out-of-order streams
efficiently and its performance is competitive with other monitoring
tools on ordered event streams.  For the setting with data values,
however, the tool's throughput for more complex specifications could
become a bottleneck.  Future work will address this limitation by
further improving the algorithms and their implementation.

1cm




  
Acknowledgments.

This work is co-funded by the European Union through the EU H2020
research and innovation programme SPIRS project with Grant Agreement
number 952622.  Views and opinions expressed are however those of the
author(s) only and do not necessarily reflect those of the European
Union.  Neither the European Union nor the granting authority can be
held responsible for them.

10

AlurHenzinger:realtimelogics_survey
R. Alur and T. A. Henzinger.
Logics and models of real time: A survey.
In Proceedings of the 1991 REX Workshop on Real Time: Theory in
  Practice, volume 600 of Lect. Notes Comput. Sci., pages 74–106.
  Springer, 1992.

Barringer_etal:eagle
H. Barringer, A. Goldberg, K. Havelund, and K. Sen.
Rule-based runtime verification.
In Proceedings of the 5th International Conference on
  Verification, Model Checking and Abstract Interpretation (VMCAI), volume
  2937 of Lect. Notes Comput. Sci., pages 44–57. Springer, 2004.

monpoly
D. Basin, M. Harvan, F. Klaedtke, and E. Zălinescu.
MONPOLY: Monitoring usage-control policies.
In Proceedings of the 2nd International Conference on Runtime
  Verification (RV), volume 7186 of Lect. Notes Comput. Sci.,
  pages 360–364. Springer, 2012.

Basin_etal:rv_mfotl
D. Basin, F. Klaedtke, S. Müller, and E. Zălinescu.
Monitoring metric first-order temporal properties.
J. ACM, 62(2), 2015.

Basin_etal:outoforder_journal
D. Basin, F. Klaedtke, and E. Zălinescu.
Runtime verification over out-of-order streams.
ACM Trans. Comput. Log., 21(1), 2020.

Bauer_etal:rv_tltl
A. Bauer, M. Leucker, and C. Schallhart.
Runtime verification for LTL and TLTL.
ACM Trans. Softw. Eng. Meth., 20(4), 2011.

flink
P. Carbone, A. Katsifodimos, S. Ewen, V. Markl, S. Haridi, and K. Tzoumas.
Apache Flink™: Stream and batch processing in a single
  engine.
IEEE Data Eng. Bull., 38(4):28–38, 2015.

ColomboFalcone:global_clock
C. Colombo and Y. Falcone.
Organising LTL monitors over distributed systems with a global
  clock.
Form. Methods Syst. Des., 49(1):109–158, 2016.

streamlab
P. Faymonville, B. Finkbeiner, M. Schledjweski, M. Schwenger, M. Stenger,
  L. Tentrup, and H. Torfah.
StreamLAB: Stream-based monitoring of cyber-physical systems.
In Proceedings of the 31st International Conference on Computer
  Aided Verification (CAV), volume 11651 of Lect. Notes Comput.
  Sci., pages 421–431. Springer, 2019.

beepbeep
S. Hallé and R. Villemaire.
Browser-based enforcement of interface contracts in web applications
  with BeepBeep.
In Proceedings of the 21st International Conference on Computer
  Aided Verification (CAV), volume 5643 of Lect. Notes Comput.
  Sci., pages 648–653. Springer, 2009.

Havelund_Rosu:monitoring_safty
K. Havelund and G. Roşu.
Efficient monitoring of safety properties.
Int. J. Softw. Tools Technol. Trans., 6(2):158–173,
  2004.

Koymans:realtime_properties
R. Koymans.
Specifying real-time properties with metric temporal logic.
Real-Time Syst., 2(4):255–299, 1990.

Meredith_etal:mop
P. O. Meredith, D. Jin, D. Griffith, F. Chen, and G. Rosu.
An overview of the MOP runtime verification framework.
Int. J. Softw. Tools Technol. Trans., 14(3):249–289,
  2012.

amt2
D. Nickovic, O. Lebeltel, O. Maler, T. Ferrère, and D. Ulus.
AMT 2.0: Qualitative and quantitative trace analysis with extended
  signal temporal logic.
In Proceedings of the 24th International Conference on Tools and
  Algorithms for the Construction and Analysis of Systems (TACAS), volume
  10806 of Lect. Notes Comput. Sci., pages 303–319. Springer,
  2018.

amt
D. Nickovic and O. Maler.
AMT: A property-based monitoring tool for analog systems.
In Proceedings of the 5th International Conference on Formal
  Modeling amd Analysis of Timed Systems (FORMATS), volume 4763 of Lect. Notes Comput. Sci., pages 304–319. Springer, 2007.

Rosu_Chen:slicing
G. Roşu and F. Chen.
Semantics and algorithms for parametric monitoring.
Log. Methods Comput. Sci., 8(1), 2012.

Scheffel_Schmitz:asynchronous_distributed_rv
T. Scheffel and M. Schmitz.
Three-valued asynchronous distributed runtime verification.
In Proceedings of the 12th ACM/IEEE International Conference on
  Formal Methods and Models for Codesign (MEMCODE), pages 52–61. IEEE
  Computer Society, 2014.

Sen_etal:decentralized_disitributed_monitoring
K. Sen, A. Vardhan, G. Agha, and G. Rosu.
Efficient decentralized monitoring of safety in distributed systems.
In Proceedings of the 26th International Conference on Software
  Engineering (ICSE), pages 418–427. IEEE Computer Society, 2004.

Stonebraker_etal:requirements
M. Stonebraker, U. Cetintemel, and S. Zdonik.
The 8 requiremens of real-time stream processing.
SIGMOD Record, 34(4):42–47, 2005.

montre
D. Ulus.
Montre: A tool for monitoring timed regular expressions.
In Proceedings of the 29th International Conference on Computer
  Aided Verification (CAV), volume 10426 of Lect. Notes Comput.
  Sci., pages 329–335. Springer, 2017.

timescales
D. Ulus.
Timescales: A benchmark generator for MTL monitoring tools.
In Proceedings of the 19th Conference on Runtime Verification
  (RV), volume 11757 of Lect. Notes Comput. Sci., pages 402–412.
  Springer, 2019.





