Online Causation Monitoring of
Signal Temporal Logic⋆
Zhenya Zhang1

CAV

Artifact
Evaluation

Available, Jie An2

, Paolo Arcaini2, and Ichiro Hasuo2

CAV

1

Kyushu University, Fukuoka, Japanzhang@ait.kyushu-u.ac.jp
2
National Institute of Informatics, Tokyo, Japan{jiean,arcaini,hasuo}@nii.ac.jp

Artifact
Evaluation

Reusable

Abstract. Online monitoring is an effective validation approach for hybrid systems, that, at runtime, checks whether the (partial) signals of asystem satisfy a specification in, e.g., Signal Temporal Logic (STL). The
classic STL monitoring is performed by computing a robustness intervalthat specifies, at each instant, how far the monitored signals are fromviolating and satisfying the specification. However, since a robustness interval monotonically shrinks during monitoring, classic online monitors
may fail in reporting new violations or in precisely describing the systemevolution at the current instant. In this paper, we tackle these issues byconsidering the causation of violation or satisfaction, instead of directly
using the robustness. We first introduce a Boolean causation monitor
that decides whether each instant is relevant to the violation or satisfaction of the specification. We then extend this monitor to a quantitative
causation monitor that tells how far an instant is from being relevantto the violation or satisfaction. We further show that classic monitors
can be derived from our proposed ones. Experimental results show thatthe two proposed monitors are able to provide more detailed information
about system evolution, without requiring a significantly higher monitoring cost.
Keywords: online monitoring, Signal Temporal Logic, monotonicity

1

Introduction

Safety-critical systems require strong correctness guarantees. Due to the complexity of these systems, offline verification may not be able to guarantee their
total correctness, as it is often very difficult to assess all possible system behaviors. To mitigate this issue, runtime verification [4,29,36] has been proposed as a⋆Z. Zhang is supported by JSPS KAKENHI Grant No. JP23K16865 and No.
JP23H03372. J. An, P. Arcaini, and I. Hasuo are supported by ERATO HASUOMetamathematics for Systems Design Project (No. JPMJER1603), JST, Funding
Reference number 10.13039/501100009024 ERATO. P.Arcaini is also supported byEngineerable AI Techniques for Practical Applications of High-Quality Machine
Learning-based Systems Project (Grant Number JPMJMI20B8), JST-Mirai.

2

Z. Zhang, J. An, P. Arcaini, I. Hasuo

complementary technique that analyzes the system execution at runtime. Online
monitoring is such an approach that checks whether the system execution (e.g.,given in terms of signals) satisfies or violates a system specification specified ina temporal logic [28, 34], e.g., Signal Temporal Logic (STL) [30].
Quantitative online monitoring is based on the STL robust semantics [17,21]
that not only tells whether a signal satisfies or violates a specification φ (i.e., theclassic Boolean satisfaction relation), but also assigns a value in R ∪ {∞, −∞}(i.e., robustness) that indicates how robustly φ is satisfied or violated. However,differently from offline assessment of STL formulas, an online monitor needs toreason on partial signals and, so, the assessment of the robustness should be
adapted. We consider an established approach [12] employed by classic online
monitors (ClaM in the following). It consists in computing, instead of a single
robustness value, a robustness interval ; at each monitoring step, ClaM identifies
U
an upper bound [R] telling the maximal reachable robustness of any possible
suffix signal (i.e., any continuation of the system evolution), and a lower boundLU[R] telling the minimal reachable robustness. If, at some instant, [R] becomesLnegative, the specification is violated; if [R] becomes positive, the specification
is satisfied. In the other cases, the specification validity is unknown.
Consider a simple example in Fig. 1.
   
It shows the monitoring of the speed of a       vehicle (in the upper plot); the specifica
tion requires the speed to be always below  
10. The lower plot reports how the upUL    ClaM
per bound [R] and the lower bound [R]of the reachable robustness change over  time. We observe that the initial value of  
U
3[R] is around 8 and gradually decreases.
 
The monitor allows to detect that the
specification is violated at time b = 20
Fig. 1: ClaM – Robustness upper andwhen the speed becomes higher than 10,
lower bounds of of 2[0,100] (v < 10)Uand therefore [R] goes below 0. AfterU
that, the violation severity progressively gets worse till time b = 30, when [R]becomes −5. After that point, the monitor does not provide any additional usefulU
information about the system evolution, as [R] remains stuck at −5. However,
if we observe the signal of the speed after b = 30, we notice that (i) the severityof the violation is mitigated, and the “1st violation episode” ends at time b = 35;
however, the monitor ClaM does not report this type of information; (ii) a “2ndviolation episode” occurs in the time interval [40, 45]; the monitor ClaM does notdistinguish the new violation.
The reason for the issues reported in the example is that the upper andlower bounds are monotonically decreasing and increasing; this has the consequence that the robustness interval at a given step is “masked” by the history
3

The value of lower bound [R]L is not shown in the figure, as not relevant. In theexample, it remains constant before b = 100, and the value is usually set either
according to domain knowledge about system signals, or to −∞ otherwise.

Online Causation Monitoring of STL

3

of previous robustness intervals, and, e.g., it is not possible to detect mitigationof the violation severity. Moreover, as an extreme consequence, as soon as themonitor ClaM assesses the violation of the specification (i.e., the upper boundUL[R] becomes negative), or its satisfaction (i.e., the lower bound [R] becomes
positive), the Boolean status of the monitor does not change anymore. Suchcharacteristic directly derives from the STL semantics and it is known as themonotonicity [9–11] of classic online monitors. Monotonicity has been recognized
as a problem of these monitors in the literature [10,37,40], since it does not allow
to detect specific types of information that are “masked”. We informally define
two types of information masking that can occur because of monotonicity:
evolution masking : the monitor may not properly report the evolution of thesystem execution, e.g., mitigation of violation severity may not be detected;
violation masking : as a special case of evolution masking, the first violation
episode during the system execution “masks” the following ones.
The information not reported by ClaM because of information masking, isvery useful in several contexts. First of all, in some systems, the first violation of
the specification does not mean that the system is not operating anymore, andone may want to continue monitoring and detect all the succeeding violations;this is the case, e.g., of the monitoring approach reported by Selyunin et al. [37] inwhich all the violations of the SENT protocol must be detected. Moreover, having
a precise description of the system evolution is important for the usefulness ofthe monitoring; for example, the monitoring of the speed in Fig. 1 could be used
in a vehicle for checking the speed and notifying the driver whenever the speed
is approaching the critical limit; if the monitor is not able to precisely capture
the severity of violation, it cannot be used for this type of application.
Some works [10,37,40] try to mitigate the monotonicity issues, by “resetting”
the monitor at specific points. A recent approach has been proposed by Zhang
et al. [40] (called ResM in the following) that is able to identify each “violation
episode” (i.e., it solves the problem of violation masking), but does not solve theevolution masking problem. For the example in Fig. 1, ResM is able to detect
the two violation episodes in intervals [20, 35] and [40, 45], but it is not able toreport that the speed decreases after b = 10 (in a non-violating situation), andthat the severity of the violation is mitigated after b = 30.
Contribution. In this paper, in order to provide more information about theevolution of the monitored system, we propose to monitor the causation of violation or satisfaction, instead of considering the robustness directly. To do this, werely on the notion of epoch [5]. At each instant, the violation (satisfaction) epoch
identifies the time instants at which the evaluation of the atomic propositions of
the specification φ causes the violation (satisfaction) of φ.
Based on the notion of epoch, we define a Boolean causation monitor (called
BCauM) that, at runtime, not only assesses the specification violation/satisfaction,
but also tells whether each instant is relevant to it. Namely, BCauM marks eachcurrent instant b as (i) a violation causation instant, if b is added to the violation
epoch; (ii) a satisfaction causation instant, if b is added to the satisfaction epoch;(iii) an irrelevant instant, if b is not added to any epoch. We show that BCauM is4

Z. Zhang, J. An, P. Arcaini, I. Hasuo

able to detect all the violation episodes (so solving the violation masking issue),as violation causation instants can be followed by irrelevant instants. Moreover,
we show that the information provided by the classic Boolean online monitor
can be derived from that of the Boolean causation monitor BCauM.
However, BCauM just tells us whether the current instant is a (violation orsatisfaction) causation instant or not, but does not report how far the instant isfrom being a causation instant. To this aim, we introduce the notion of causation
distance, as a quantitative measure characterizing the spatial distance of thesignal value at b from turning b into a causation instant. Then, we propose
the quantitative causation monitor (QCauM) that, at each instant, returns its
causation distance. We show that using QCauM, besides solving the violation
masking problem, we also solve the evolution masking problem. Moreover, weshow that we can derive from QCauM both the classic quantitative monitor ClaM,
and the Boolean causation monitor BCauM.
Experimental results show that the proposed monitors, not only provide more
information, by they do it in an efficient way, not requiring a significant additional monitoring time w.r.t. the existing monitors.
Outline. §2 reports necessary background. We introduce BCauM in §3, and QCauM
in §4. Experimental assessment of the two proposed monitors is reported in §5.
Finally, §6 discusses some related work, and §7 concludes the paper.

2

Preliminaries

In this section, we review the fundamentals of signal temporal logic (STL) in§2.1, and then introduce the existing classic online monitoring approach in §2.2.
2.1

Signal Temporal Logic

Let T ∈ R+ be a positive real, and d ∈ N+ be a positive integer. A d -dimensionalsignal is a function v : [0, T ] → Rd , where T is called the time horizon of v.
Given an arbitrary time instant t ∈ [0, T ], v(t) is a d -dimensional real vector;
each dimension concerns a signal variable that has a certain physical meaning,e.g., speed, RPM, acceleration, etc. In this paper, we fix a set Var of variables
and assume that a signal v is spatially bounded, i.e., for all t ∈ [0, T ], v(t) ∈ Ω,
where Ω is a d -dimensional hyper-rectangle.
Signal temporal logic (STL) is a widely-adopted specification language, used
to describe the expected behavior of systems. In Def. 1 and Def. 2, we respectively
review the syntax and the robust semantics of STL [17, 21, 30].
Definition 1 (STL syntax). In STL, the atomic propositions α and the formulas φ are defined as follows:α ::≡ f (w1 , . . . , wK ) > 0

φ ::≡ α | ⊥ | ¬φ | φ ∧ φ | 2I φ | 3I φ | φ UI φ

Here f is a K-ary function f : RK → R, w1 , . . . , wK ∈ Var, and I is a closed
interval over R≥0 , i.e., I = [l, u], where l, u ∈ R and l ≤ u. In the case that

Online Causation Monitoring of STL5

l = u, we can use l to stand for I. 2, 3 and U are temporal operators, which
are known as always, eventually and until, respectively. The always operator 2
and eventually operator 3 are two special cases of the until operator U, where
3I φ ≡ ⊤ UI φ and 2I φ ≡ ¬3I ¬φ. Other common connectives such as ∨, → areintroduced as syntactic sugar: φ1 ∨ φ2 ≡ ¬(¬φ1 ∧ ¬φ2 ), φ1 → φ2 ≡ ¬φ1 ∨ φ2 .
Definition 2 (STL robust semantics). Let v be a signal, φ be an STL formula and τ ∈ R+ be an instant. The robustness R(v, φ, τ ) ∈ R ∪ {∞, −∞} of v
w.r.t. φ at τ is defined by induction on the construction of formulas, as follows.
R(v, α, τ ) := f (v(τ ))R(v, ⊥, τ ) := −∞R(v, ¬φ, τ ) := −R(v, φ, τ )R(v, φ1 ∧ φ2 , τ ) := min (R(v, φ1 , τ ), R(v, φ2 , τ ))R(v, 2I φ, τ ) :=inf R(v, φ, t)R(v, 3I φ, τ ) := sup R(v, φ, t)t∈τ +IR(v, φ1 UI φ2 , τ ) := sup min R(v, φ2 , t), ′ inf R(v, φ1 , t′ )t∈τ +It∈τ +It ∈[τ,t)Here, τ + I denotes the interval [l + τ, u + τ ].
The original STL semantics is Boolean, which represents whether a signal v
satisfies φ at an instant τ , i.e., whether (v, τ ) |= φ. The robust semantics in Def. 2
is a quantitative extension that refines the original Boolean STL semantics, inthe sense that, R(v, φ, τ ) > 0 implies (v, τ ) |= φ, and R(v, φ, τ ) < 0 implies(v, τ ) ̸|= φ. More details can be found in [21, Prop. 16].
2.2

Classic Online Monitoring of STL

STL robust semantics in Def. 2 provides an offline monitoring approach forcomplete signals. Online monitoring, instead, targets a growing partial signal atruntime. Besides the verdicts ⊤ and ⊥, an online monitor can also report theverdict unknown (denoted as ?), which represents a status when the satisfactionof the signal to φ is not decided yet. In the following, we formally define partial
signals and introduce online monitors for STL.
Let T be the time horizon of a signal v, and let [a, b] ⊆ [0, T ] be a subinterval in the time domain [0, T ]. A partial signal va:b is a function which isonly defined in the interval [a, b]; in the remaining domain [0, T ]\[a, b], we denotethat va:b = ϵ, where ϵ stands for a value that is not defined.
Specifically, if a = 0 and b ∈ (a, T ], a partial signal va:b is called a prefix(partial) signal; dually, if b = T and a ∈ [0, b), a partial signal va:b is called asuffix (partial) signal. Given a prefix signal v0:b , a completion v0:b · vb:T of v0:b
is defined as the concatenation of v0:b with a suffix signal vb:T .
Definition 3 (Classic Boolean STL online monitor). Let v0:b be a prefix
signal, and φ be an STL formula. An online monitor M(v0:b , φ, τ ) returns a

6

Z. Zhang, J. An, P. Arcaini, I. Hasuo

verdict in {⊤, ⊥, ?} (namely, true, false, and unknown), as follows:⊤ if ∀vb:T . R(v0:b · vb:T , φ, τ ) > 0
M(v0:b , φ, τ ) := ⊥ if ∀vb:T . R(v0:b · vb:T , φ, τ ) < 0? otherwise
Namely, the verdicts of M(v0:b , φ, τ ) are interpreted as follows:– if any possible completion v0:b · vb:T of v0:b satisfies φ, then v0:b satisfies φ;– if any possible completion v0:b · vb:T of v0:b violates φ, then v0:b violates φ;– otherwise (i.e., there is a completion v0:b · vb:T that satisfies φ, and there is
a completion v0:b · vb:T that violates φ), then M(v0:b , φ, τ ) reports unknown.
Note that, by Def. 3 only, we cannot synthesize a feasible online monitor,
because the possible completions for v0:b are infinitely many. A constructive
online monitor is introduced in [12], which implements the functionality of Def. 3
by computing the reachable robustness of v0:b . We review this monitor in Def. 4.
Definition 4 (Classic Quantitative STL online monitor (ClaM)). Let v0:bα
be a prefix signal, and let φ be an STL formula. We denote by Rα
max and Rmin the4possible maximum and minimum bounds of the robustness R(v, α, τ ) . Then, anαonline monitor [R](v0:b , φ, τ ), which returns a sub-interval of [Rαmin , Rmax ] at the
instant b, is defined as follows, by induction on the construction of formulas.
(
f (v0:b (τ )) , f (v0:b (τ ))if τ ∈ [0, b]
[R](v0:b , α, τ ) :=  αRmin , Rαotherwisemax[R](v0:b , ¬φ, τ ) := −[R](v0:b , φ, τ )[R](v0:b , φ1 ∧ φ2 , τ ) := min [R](v0:b , φ1 , τ ), [R](v0:b , φ2 , τ )[R](v0:b , 2I φ, τ ) := inf [R](v0:b , φ, t)t∈τ +I[R](v0:b , φ1 UI φ2 , τ ) := sup min [R](v0:b , φ2 , t), ′ inf [R](v0:b , φ1 , t′ )t ∈[τ,t)t∈τ +I

Here, f is defined as in Def. 1, and the arithmetic rules over intervals I = [l, u] aredefined as follows: −I := [−u, −l] and min(I1 , I2 ) := [min(l1 , l2 ), min(u1 , u2 )].
UL

We denote by [R] (v0:b , φ, τ ) and [R] (v0:b , φ, τ ) the upper bound and thelower bound of [R](v0:b , φ, τ ) respectively. Intuitively, the two bounds together
form the reachable robustness interval of the completion v0:b · vb:T , under any
Upossible suffix signal vb:T . For instance, in Fig. 2, the upper bound [R] at b = 20
is 0, which indicates that the robustness of the completion of the signal speed,
under any suffix, can never be larger than 0.
The quantitative online monitor ClaM in Def. 4 refines the Boolean one inDef. 3, and the Boolean monitor can be derived from ClaM as follows:
4

R(v, α, τ ) is bounded because v is bounded by Ω. In practice, if Ω is not know, we
α
set Rαmax and Rmin to, respectively, ∞ and −∞.

Online Causation Monitoring of STL

7

L– if [R] (v0:b , φ, τ ) > 0, it implies that M(v0:b , φ, τ ) = ⊤;U
– if [R] (v0:b , φ, τ ) < 0, it implies that M(v0:b , φ, τ ) = ⊥;LU– otherwise, if [R] (v0:b , φ, τ ) < 0 and [R] (v0:b , φ, τ ) > 0, M(v0:b , φ, τ ) = ?.
The classic online monitors are monotonic by definition. In the Boolean monitor (Def. 3), with the growth of v0:b , M(v0:b , φ, τ ) can only turn from ? to {⊥, ⊤},but never the other way around. In the quantitative one (Def. 4), as shown inULLem. 1, [R] (v0:b , φ, τ ) and [R] (v0:b , φ, τ ) are both monotonic, the former one
decreasingly, the latter one increasingly. An example can be observed in Fig. 2.
Lemma 1 (Monotonicity of STL online monitor). Let [R](v0:b , φ, τ ) be
the quantitative online monitor for a partial signal v0:b and an STL formula φ.
UWith the growth of the partial signal v0:b , the upper bound [R] (v0:b , φ, τ ) monoL
tonically decreases, and the lower bound [R] (v0:b , φ, τ ) monotonically increases,
Ui.e., for two time instants b1 , b2 ∈ [0, T ], if b1 < b2 , we have (i) [R] (v0:b1 , φ, τ ) ≥UL
L[R] (v0:b2 , φ, τ ), and (ii) [R] (v0:b1 , φ, τ ) ≤ [R] (v0:b2 , φ, τ ).
Proof. This can be proved by induction on the structures of STL formulas. The
detailed proof can be found in the full version [38].
⊔⊓3

Boolean Causation Online Monitor

As explained in §1, monotonicity of classic online monitors causes different typesof information masking, which prevents some information from being delivered.
In this section, we introduce a novel Boolean causation (online) monitor BCauM,
that solves the violation masking issue (see §1). BCauM is defined based on online
signal diagnostics [5, 40], which reports the cause of violation or satisfaction of
the specification at the atomic proposition level.
Definition 5 (Online signal diagnostics). Let v0:b be a partial signal andφ be an STL specification. At an instant b, online signal diagnostics returns aUviolation epoch E⊖ (v0:b , φ, τ ), under the condition [R] (v0:b , φ, τ ) < 0, as follows:(U{⟨α, τ ⟩} if [R] (v0:b , α, τ ) < 0E⊖ (v0:b , α, τ ) :=∅otherwiseE⊖ (v0:b , ¬φ, τ ) := E⊕ (v0:b , φ, τ )[E⊖ (v0:b , φ1 ∧ φ2 , τ ) :=E⊖ (v0:b , φi , τ )i∈{1,2} s.t.
[R]U (v0:b ,φi ,τ )<0[E⊖ (v0:b , 2I φ, τ ) :=E⊖ (v0:b , φ, t)t∈τ +I s.t.
[R]U (v0:b ,φ,t)<0E⊖ (v0:b , φ1 UI φ2 , τ ) :=[E⊖ (v0:b , φ2 , t) ∪t∈τ +I s.t.
[R]U (v0:b ,φ1 Ut φ2 ,τ )<0
[t′ ∈[τ,t)E⊖ (v0:b , φ1 , t′ )

8

Z. Zhang, J. An, P. Arcaini, I. Hasuo

Land a satisfaction epoch E⊕ (v0:b , φ, τ ), under the condition [R] (v0:b , φ, τ ) > 0,
as follows:(L{⟨α, τ ⟩} if [R] (v0:b , α, τ ) > 0⊕
E (v0:b , α, τ ) :=∅otherwiseE⊕ (v0:b , ¬φ, τ ) := E⊖ (v0:b , φ, τ )[E⊕ (v0:b , φ1 ∧ φ2 , τ ) :=E⊕ (v0:b , φi , τ )i∈{1,2} s.t.
[R]L (v0:b ,φi ,τ )>0[

E⊕ (v0:b , 2I φ, τ ) :=E⊕ (v0:b , φ, t)t∈τ +I s.t.
[R]L (v0:b ,φ,t)>0E⊕ (v0:b , φ1 UI φ2 , τ ) :=[E⊕ (v0:b , φ2 , t) ∪t∈τ +I s.t.
[R]L (v0:b ,φ1 Ut φ2 ,τ )>0


[E⊕ (v0:b , φ1 , t′ )

t′ ∈[τ,t)If the conditions are not satisfied, E⊖ (v0:b , φ, τ ) and E⊕ (v0:b , φ, τ ) are both ∅.
Note that the definition is recursive, thus the conditions should also be checked
for computing the violation and satisfaction epochs of the sub-formulas of φ.
Computation for other operators can be inferred by the presented ones andthe STL syntax (Def. 1).
Intuitively, when a partial signal v0:b violates a specification φ, a violation
epoch starts collecting the evaluations (identified by pairs of atomic propositions
and instants) of the signal at the atomic proposition level, that cause the violation of the whole formula φ (which also applies to the satisfaction cases in a dual
manner). This is done inductively, based on the semantics of different operators:– in the case of an atomic proposition α, if α is violated at τ , it collects ⟨α, τ ⟩;– in the case of a negation ¬φ, it collects the satisfaction epoch of φ;– in the case of a conjunction φ1 ∧ φ2 , it collects the union of the violation
epochs of the sub-formulas violated by the partial signal;– in the case of an always operator 2I φ, it collects the epochs of the subformula φ at all the instants t where φ is evaluated as being violated.
– in the case of an until operator φ1 UI φ2 , it collects the epochs of the subformula φ2 at all the instants t and the epochs of φ1 at the instants t′ ∈ [τ, t),
in the case where the clause “φ1 until φ2 ” is violated at t.
Example 1. The example in Fig. 2 illustrates how an epoch is collected. The
specification requires that whenever the speed is higher than 10, the car should
decelerate within 5 time units. As shown by the classic monitor, the specification
is violated at b = 25, since v becomes higher than 10 at 20 but a remains positive
during [20, 25]. Note that the specification can be rewritten as φ ≡ 2[0,100] (¬(v >10) ∨ 3[0,5] (a < 0)). For convenience, we name the sub-formulas of φ as follows:φ′ ≡ ¬(v > 10) ∨ 3[0,5] (a < 0)

φ1 ≡ ¬(v > 10)

φ2 ≡ 3[0,5] (a < 0)

Online Causation Monitoring of STLv (speed)
15
13
10

5

10

15

20

25

30

35

b

a (acceleration)
6
3
0
-5
-10

v (speed)b=30

v (speed)
10

b=30

10

5

10

15

20

25

30

35

b

5

-10

10 15

5

10

15

20

25

30

35

b

classic quantitative online monitor ClaM

10 15

5

b=35

v (speed)

10
20 25

30

b

20 25

10 15

10 5

b

30

0
a (acceleration)

0

b=35

v (speed)a (acceleration)

classic Boolean online monitor

?

5

9

10 15

30

35

b

20 25

30

35

35

b

20 25

a (acceleration)
5

10 15

20 25

30

b

-10

0

5

10 15

20 25

30

The violation epochs (red parts) when b=30 and b=35

Fig. 3: The violation epochs(the red parts) reb -10
b
5 10
15 20causation
Booleanspectively
when25b 30= monitor
30 and b5= 103515 20 25 30 35-10⊕
The violation
epochs (red parts) when b=30 and b=35⊘
Booleancausation monitor BCauMb (time)5 10 15 20 25 30 35

10

5

10

15

20

25

30

35

b

⊕
⊖

-10

⊘

Fig. 2: Classic monitor (ClaM)
result for the STL specification:
2[0,100] (v > 10 → 3[0,5] (a < 0))b

a0 (acceleration)

5

10 15

20 25

30 35

b (time)⊖Fig. 4: Boolean causation monitor (BCauM) result

α1 ≡ v > 10

α2 ≡ a < 0

Fig. 3 shows the violation epochs at two instants 30 and 35. First, at b = 30,


S
S
⊕
⊖
E⊖ (v0:30 , φ, 0) =t∈[20,25] E (v0:30 , α1 , t) ∪t∈[20,30] E (v0:30 , α2 , t)= ⟨α1 , [20, 25]⟩ ∪ ⟨α2 , [20, 30]⟩
Similarly, the violation epoch E⊖ (v0:35 , φ, 0) at b = 35 is the same as that at
b = 30. Intuitively, the epoch at b = 30 shows the cause of the violation of v0:30 ;then since signal a < 0 in [30, 35], this segment is not considered as the cause of
the violation, so the epoch remains the same at b = 35.
Definition 6 (Boolean causation monitor (BCauM)). Let v0:b be a partial
signal and φ be an STL specification. We denote by A the set of atomic propositions of φ. At each instant b, a Boolean causation (online) monitor BCauM
returns a verdict in {⊖, ⊕, ⊘} (called violation causation, satisfaction causationand irrelevant), which is defined as follows,⊖⊖ if ∃α ∈ A. ⟨α, b⟩ ∈ E (v0:b , φ, τ )M (v0:b , φ, τ ) := ⊕ if ∃α ∈ A. ⟨α, b⟩ ∈ E⊕ (v0:b , φ, τ )⊘ otherwise
An instant b is called a violation/satisfaction causation instant if M (v0:b , φ, τ )returns ⊖/⊕, or an irrelevant instant if M (v0:b , φ, τ ) returns ⊘.
Intuitively, if the current instant b (with the related α) is included in theepoch (thus the signal value at b is relevant to the violation/satisfaction of φ),

10

Z. Zhang, J. An, P. Arcaini, I. Hasuo

BCauM will report a violation/satisfaction causation (⊖/⊕); otherwise, it willreport irrelevant (⊘). Notably BCauM is non-monotonic, in that even if it reports⊖ or ⊕ at some instant b, it may still report ⊘ after b. This feature allows BCauM
to bring more information, e.g., it can detect the end of a violation episode andthe start of a new one (i.e., it solves the violation masking issue in §1); see Ex. 2.
Example 2. Based on the signal diagnostics in Fig. 3, the Boolean causation
monitor BCauM reports the result shown as in Fig. 4.
Compared to the classic Boolean monitor in Fig. 2, BCauM brings more information, in the sense that it detects the end of the violation episode at b = 30,
by going from ⊖ to ⊘, when the signal a becomes negative.
Thm. 1 states the relation of BCauM with the classic Boolean online monitor.
Theorem 1. The Boolean causation monitor BCauM in Def. 6 refines the classic
Boolean online monitor in Def.
W 3, in the following sense:– M(v0:b , φ, τ ) = ⊥ iff.
(M (v0:t , φ, τ ) = ⊖)Wt∈[0,b]– M(v0:b , φ, τ ) = ⊤ iff.
(M (v0:t , φ, τ ) = ⊕)Vt∈[0,b]– M(v0:b , φ, τ ) = ? iff.
t∈[0,b] (M (v0:t , φ, τ ) = ⊘)Proof. The proof is based on Defs. 5 and 6, Lem. 1 about the monotonicity ofclassic STL online monitors, and two extra lemmas in the full version [38]. ⊔⊓4

Quantitative Causation Online Monitor

Although BCauM in §3 is able to solve the violation masking issue, it still does
not provide enough information about the evolution of the system signals, i.e., it
does not solve the evolution masking issue introduced in §1. To tackle this issue,
we propose a quantitative (online) causation monitor QCauM in Def. 7, which
is a quantitative extension of BCauM. Given a partial signal v0:b , QCauM reports⊖
a violation causation distance [R] (v0:b , φ, τ ) and a satisfaction causation dis⊕
tance [R] (v0:b , φ, τ ), which, respectively, indicate how far the signal value atthe current instant b is from turning b into a violation causation instant andfrom turning b into a satisfaction causation instant.
Definition 7 (Quantitative causation monitor (QCauM)). Let v0:b be a partial signal, and φ be an STL specification. At instant b, the quantitative causation⊖
monitor QCauM returns a violation causation distance [R] (v0:b , φ, τ ), as follows:(f (v0:b (τ )) if b = τ⊖[R] (v0:b , α, τ ) :=Rαotherwisemax⊖⊕[R] (v0:b , ¬φ, τ ) := −[R] (v0:b , φ, τ )


⊖
⊖
⊖
[R] (v0:b , φ1 ∧ φ2 , τ ) := min [R] (v0:b , φ1 , τ ) , [R] (v0:b , φ2 , τ )


 
⊖
U
max [R] (v0:b , φ1 , τ ) , [R] (v0:b , φ2 , τ ) ,⊖ [R] (v0:b , φ1 ∨ φ2 , τ ) := min U⊖max [R] (v0:b , φ1 , τ ), [R] (v0:b , φ2 , τ )Online Causation Monitoring of STL

11⊖[R] (v0:b , φ, t)t∈τ +I⊖⊖U[R] (v0:b , 3I φ, τ ) := inf max [R] (v0:b , φ, t) , [R] (v0:b , 3I φ, τ )t∈τ +I! ⊖inf [R] (v0:b , φ1 , t′ )′ ∈[τ,t)
t

 min

⊖
⊖
[R] (v0:b , φ1 UI φ2 , τ ) := inf max [R] (v0:b , φ2 , t)⊖

[R] (v0:b , 2I φ, τ ) :=inft∈τ +IU[R] (v0:b , φ1 UI φ2 , τ )⊕and a satisfaction causation distance [R] (v0:b , φ, τ ), as follows:(f (v0:b (τ )) if b = τ⊕[R] (v0:b , α, τ ) :=Rαotherwisemin⊕⊖[R] (v0:b , ¬φ, τ ) := −[R] (v0:b , φ, τ )

 

⊕
L
min
[R]
(v
,
φ
,
τ
)
,
[R]
(v
,
φ
,
τ
)
,
0:b
1
0:b
2
⊕

 
[R] (v0:b , φ1 ∧ φ2 , τ ) := max L⊕min [R] (v0:b , φ1 , τ ), [R] (v0:b , φ2 , τ )


⊕
⊕
⊕
[R] (v0:b , φ1 ∨ φ2 , τ ) := max [R] (v0:b , φ1 , τ ) , [R] (v0:b , φ2 , τ )



⊕
⊕
L
[R] (v0:b , 2I φ, τ ) := sup min [R] (v0:b , φ, t) , [R] (v0:b , 2I φ, τ )t∈τ +I⊕⊕[R] (v0:b , 3I φ, τ ) := sup [R] (v0:b , φ, t)t∈τ +I ⊕sup [R] (v0:b , φ1 , t′ )
 t′ ∈[τ,t)
 


 

 min  inf [R]L (v0:b , φ1 , t′ )  



′

 


t ∈[τ,t)⊕L[R] (v0:b , φ1 UI φ2 , τ ) := sup max [R] (v0:b , φ2 , t)t∈τ +I 


!
L
′



inf [R] (v0:b , φ1 , t )′
min t ∈[τ,t)⊕[R] (v0:b , φ2 , t)⊖

Intuitively, a violation causation distance [R] (v0:b , φ, τ ) is the spatial distanceof the signal value v0:b (b), at the current instant b, from turning b into a violation
causation instant such that b is relevant to the violation of φ (also applied tothe satisfaction case dually). It is computed inductively on the structure of φ:– Case atomic propositions α: if b = τ (i.e., at which instant α should be
evaluated), then the distance of b from being a violation causation instant is
f (v0:b (b)); otherwise, if b ̸= τ , despite the value of f (v0:b (b)), b can never bea violation causation instant, according to Def. 5, because only f (v0:b (τ )) isrelevant to the violation of α. Hence, the distance will be Rαmax ;– Case ¬φ: b is a violation causation instant for ¬φ if b is a satisfaction cau⊖⊕sation instant for φ, so [R] (v0:b , ¬φ, τ ) depends on [R] (v0:b , φ, τ );– Case φ1 ∧ φ2 : b is a violation causation instant for φ1 ∧ φ2 if b is a violation⊖
causation instant for either φ1 or φ2 , so [R] (v0:b , φ1 ∧ φ2 , τ ) depends on⊖⊖the minimum between [R] (v0:b , φ1 , τ ) and [R] (v0:b , φ2 , τ );

12

Z. Zhang, J. An, P. Arcaini, I. Hasuo      QCauM


[R]






 

[R]⊕

Fig. 5: Quantitative causation monitor (QCauM) result for Ex. 1– Case φ1 ∨ φ2 : b is a violation causation instant for φ1 ∨ φ2 if, first, φ1 ∨ φ2
has been violated at b, and second, b is the violation causation instant for⊖either φ1 or φ2 . Hence, [R] (v0:b , φ1 ∨ φ2 , τ ) depend on both the violationUstatus (measured by [R] (v0:b , φi , τ )) of one sub-formula and the violation
causation distance of the other sub-formula;– Case 2I φ: b is a violation causation instant for 2I φ if b is the violation
causation instant for the sub-formula φ evaluated at any instant in τ + I.
⊖
So, [R] (v0:b , 2I φ, τ ) depends on the infimum of the violation causation
distances regarding φ evaluated at the instants in τ + I;
– Case 3I φ: b is a violation causation instant for 3I φ if, first, 3I φ has been
violated at b, and second, b is a violation causation instant for the sub⊖formula φ evaluated at any instant in τ + I. So, [R] (v0:b , 3I φ, τ ) depends
Uon both the violation status of 3I φ (measured by [R] (v0:b , 3I φ, τ )) andthe infimum of the violation causation distances of φ evaluated in τ + I.
⊖
– Case φ1 UI φ2 : [R] (v0:b , φ1 UI φ2 , τ ) depends on, first, the violation status
Uof the whole formula (measured by [R] (v0:b , φ1 UI φ2 , τ )), and also, theinfimum of the violation causation distances regarding the evaluation of “φ1holds until φ2 ” at each instant in τ + I.
Similarly, we can also compute the satisfaction causation distance. We use Ex. 3
to illustrate the quantitative causation monitor for the signals in Ex. 1.
Example 3. Consider the quantitative causation monitor for the signals in
Ex. 1. At b = 30, the violation causation distance is computed as:[R]⊖ (v0:30 ,φ,0)= inf [R]⊖ v0:30 ,φ′ ,tt∈[0,100]



 
max [R]⊖ (v0:30 ,φ1 ,t),[R]U (v0:30 ,φ2 ,t) , = inf min
t∈[0,100]max [R]U (v0:30 ,φ1 ,t),[R]⊖ (v0:30 ,φ2 ,t)


⊕

U

!



′


 max −[R] (v0:30 ,α1 ,t), sup [R] (v0:30 ,α2 ,t )




t′ ∈t+[0,5]!! = inf min
U


[R]
(v
,φ
,t),
t∈[0,100]
0:30
2



max −[R]L (v0:30 ,α1 ,t),max
inf [R]⊖ v0:30 ,α2 ,t′t′ ∈t+[0,5]=max −[R]L (v0:30 ,α1 ,25),[R]U (v0:30 ,φ2 ,25), ′ inft ∈[25,30]=max(−3,−3,−5)=−3.

[R]⊖ v0:30 ,α2 ,t′Online Causation Monitoring of STL

13⊖

Similarly, at b = 35, the violation causation distance [R] (v0:35 , φ, 0) = 5.
See the result of QCauM shown in Fig. 5. Compared to ClaM in Fig. 2, it is evident
that QCauM provides much more information about the system evolution, e.g.,
it can report that, in the interval [15, 20], the system satisfies the specification“more”, as the speed decreases.

By using the violation and satisfaction causation distances reported by QCauM
jointly, we can infer the verdict of BCauM, as indicated by Thm. 2.
Theorem 2. The quantitative causation monitor QCauM in Def. 7 refines theBoolean causation monitor BCauM in Def. 6, in the sense that:⊖– if [R] (v0:b , φ, τ ) < 0, it implies M (v0:b , φ, τ ) = ⊖;⊕– if [R] (v0:b , φ, τ ) > 0, it implies M (v0:b , φ, τ ) = ⊕;⊖⊕– if [R] (v0:b , φ, τ ) > 0 and [R] (v0:b , φ, τ ) < 0, it implies M (v0:b , φ, τ ) = ⊘.
Proof. The proof is generally based on mathematical induction. First, by Def. 7
and Def. 5, it is straightforward that Thm. 2 holds for the atomic propositions.
Then, assuming that Thm. 2 holds for an arbitrary formula φ, we provethat Thm. 2 also holds for the composite formula φ′ constructed by applying
STL operators to φ. The complete proof for all three cases is shown in the fullversion [38].
As an instance, we show the proof for the first case with φ′ = φ1 ∨ φ2 , i.e.,⊖
we prove that [R] (v0:b , φ1 ∨ φ2 , τ ) < 0 implies M (v0:b , φ1 ∨ φ2 , τ ) = ⊖.
⊖[R] (v0:b , φ1 ∨ φ2 , τ ) < 0⊖U⇒ max [R] (v0:b , φ1 , τ ) , [R] (v0:b , φ2 , τ ) < 0⊖⇒[R] (v0:b , φ1 , τ ) < 0(by def. of max)

⇒M (v0:b , φ1 , τ ) = ⊖⊖(by Def. 7 and w.l.o.g.)(by assumption)⊖⇒E (v0:b , φ1 ∨ φ2 , τ ) ⊇ E (v0:b , φ1 , τ )(by Def. 5 and Thm. 1)⊖⇒∃α. ⟨α, b⟩ ∈ E (v0:b , φ1 ∨ φ2 , τ )(by def. of ⊇)⇒M (v0:b , φ1 ∨ φ2 , τ ) = ⊖(by Def. 6)⊔⊓

The relation between the quantitative causation monitor QCauM and theBoolean causation monitor BCauM, disclosed by Thm. 2, can be visualized by
the comparison between Fig. 5 and Fig. 4. Indeed, when the violation causation
distance reported by QCauM is negative in Fig. 5, BCauM reports ⊖ in Fig. 4.
Next, we present Thm. 3, which states the relation between the quantitative
causation monitor QCauM and the classic quantitative monitor ClaM.
Theorem 3. The quantitative causation monitor QCauM in Def. 7 refines theclassic quantitative online monitor ClaM in Def. 4, in the sense that, the monitoring results of ClaM can be reconstructed from the results of QCauM, as follows:
U

⊖

(1)

⊕

(2)

[R] (v0:b , φ, τ ) = inf [R] (v0:t , φ, τ )t∈[0,b]L[R] (v0:b , φ, τ ) = sup [R] (v0:t , φ, τ )t∈[0,b]

14

Z. Zhang, J. An, P. Arcaini, I. Hasuo

Proof. The proof is generally based on mathematical induction. First, by Def. 7
and Def. 4, it is straightforward that Thm. 3 holds for the atomic propositions.
Then, we make the global assumption that Thm. 3 holds for an arbitrary⊖U
formula φ, i.e., both the two cases inf t∈[0,b] [R] (v0:t , φ, τ ) = [R] (v0:b , φ, τ )⊕Land supt∈[0,b] [R] (v0:t , φ, τ ) = [R] (v0:b , φ, τ ) hold. Based on this assumption,
we prove that Thm. 3 also holds for the composite formula φ′ constructed byapplying STL operators to φ.
⊖U
As an instance, we prove inf t∈[0,b] [R] (v0:t , φ′ , τ ) = [R] (v0:b , φ′ , τ ) withφ′ = φ1 ∨ φ2 as follows. The complete proof is presented in the full version [38].
– First, if b = τ , it holds that:⊖⊖inf [R] (v0:t ,φ1 ∨φ2 ,τ )=[R] (v0:τ ,φ1 ∨φ2 ,τ )UU=max [R] (v0:τ ,φ1 ,τ ),[R] (v0:τ ,φ2 ,τ )(by Def. 7 and global assump.)t∈[0,b]U=[R] (v0:b ,φ1 ∨φ2 ,τ )(by Def. 4)– Then, we make a local assumption that, given an arbitrary b, it holds that⊖U
inf t∈[0,b] [R] (v0:t , φ1 ∨ φ2 , τ ) = [R] (v0:b , φ1 ∨ φ2 , τ ). We prove that, for b′
which is the next sampling point to b, it holds that,⊖inf [R] (v0:t ,φ1 ∨φ2 ,τ )U⊖=min [R] (v0:b ,φ1 ∨φ2 ,τ ),[R] (v0:b′ ,φ1 ∨φ2 ,τ )

 

U
U
max [R] (v0:b ,φ1 ,τ ),[R] (v0:b ,φ2 ,τ ) ,


 


⊖
U
=min max [R] (v0:b′ ,φ1 ,τ ),[R] (v0:b′ ,φ2 ,τ ) , 

 

U
⊖
max [R] (v0:b′ ,φ1 ,τ ),[R] (v0:b′ ,φ2 ,τ )

 

U
U
max [R] (v0:b ,φ1 ,τ ),[R] (v0:b ,φ2 ,τ ) ,


 


⊖
U
 max [R] (v0:b′ ,φ1 ,τ ),[R] (v0:b ,φ2 ,τ ) , 

 
=min


U
⊖
 max [R] (v0:b ,φ1 ,τ ),[R] (v0:b′ ,φ2 ,τ ) , 



⊖
⊖
max [R] (v0:b′ ,φ1 ,τ ),[R] (v0:b′ ,φ2 ,τ )


 
U
⊖
min [R] (v0:b ,φ1 ,τ ),[R] (v0:b′ ,φ1 ,τ ) ,

 
=max
U
⊖
min [R] (v0:b ,φ2 ,τ ),[R] (v0:b′ ,φ2 ,τ )UU=max [R] (v0:b′ ,φ1 ,τ ),[R] (v0:b′ ,φ2 ,τ )t∈[0,b′ ]U=[R] (v0:b′ ,φ1 ∨φ2 ,τ )(by local assump.)(by Defs. 4 & 7)

(by global assump.)(by def. of min, max)(by global assump.)(by Def. 4)

U⊔⊓

Thm. 3 shows that the result [R] (v0:b , φ, τ ) of ClaM can be derived from the⊖result of QCauM by applying inf t∈[0,b] [R] (v0:b , φ, t). For instance, comparing
the results of QCauM in Fig. 5 and the results of ClaM in Fig. 2, we can find thatthe results in Fig. 2 can be reconstructed by using the results in Fig. 5.

Online Causation Monitoring of STL
M(v0:b , φ, τ )R(v, φ, τ )[R]U (v0:b , φ, τ )[R]L (v0:b , φ, τ )Thm. 1M (v0:b , φ, τ )Thm. 2(v, τ ) |= φ15

Thm. 3[R]⊖ (v0:b , φ, τ )[R]⊕ (v0:b , φ, τ )Fig. 6: Refinement among STL monitors

Remark 1. Fig. 6 shows the refinement relations between the six STL monitoring approaches. The left column lists the offline monitoring approaches derived
directly from the Boolean and quantitative semantics of STL respectively. The
middle column shows the classic online monitoring approaches. Our two causation monitors, namely BCauM and QCauM, are given in the column on the right.
Given a pair (A, B) of the approaches, A ← B indicates that the approach B
refines the approach A, in the sense that B can deliver more information than A,
and the information delivered by A can be derived from the information deliveredby B. It is clear that the refinement relation in the figure ensures transitivity.
Note that blue arrows are contributed by this paper. As shown by Fig. 6, therelation between BCauM and QCauM is analogous to that between the Boolean andquantitative semantics of STL.

5

Experimental Evaluation

We implemented a tool5 for our two causation monitors. It is built on the top of
Breach [15], a widely used tool for monitoring and testing of hybrid systems [18].
Being consistent with Breach, the monitors target the output signals given by
Simulink models, as an additional block. Experiments were executed on a MacOS
machine, 1.4 GHz Quad-Core Intel Core-i5, 8 GB RAM, using Breach v1.10.0.
5.1

Experiment Setting

Benchmarks. We perform the experiments on the following two benchmarks.
Abstract Fuel Control (AFC) is a powertrain control system from Toyota [27],which has been widely used as a benchmark in the hybrid system community [18–20]. The system outputs the air-to-fuel ratio AF, and requires that the deviationof AF from its reference value AFref should not be too large. Specifically, we
consider the following properties from different perspectives:– φAFC:= 2[10,50] (|AF − AFref| < 0.1): the deviation should always be small;1– φAFC:= 2[10,48.5] 3[0,1.5] (|AF − AFref| < 0.08): a large deviation should not2last for too long time;
5

Available at https://github.com/choshina/STL-causation-monitor, and Zenodo [39].

16

Z. Zhang, J. An, P. Arcaini, I. Hasuo– φAFC:= 2[10,48] (|AF−AFref| > 0.08 → 3[0,2] (|AF−AFref| < 0.08)): whenever3
the deviation is too large, it should recover to the normal status soon.
Automatic transmission (AT) is a widely-used benchmark [18–20], implementing
the transmission controller of an automotive system. It outputs the gear, speed
and RPM of the vehicle, which are required to satisfy this safety requirement:– φAT
1 := 2[0,27] (speed > 50 → 3[1,3] (RPM < 3000)): whenever the speed ishigher than 50, the RPM should be below 3000 in three time units.
Baseline and experimental design. In order to assess our two proposed monitors (the Boolean causation monitor BCauM in Def. 6, and the quantitative causation monitor QCauM in Def. 7), we compare them with two baseline monitors:
the classic quantitative robustness monitor ClaM (see Def. 4); and the state-ofthe-art approach monitor with reset ResM [40], that, once the signal violates the
specification, resets at that point and forgets the previous partial signal.
Given a model and a specification, we generate input signals by randomly
sampling in the input space and feed them to the model. The online output
signals are given as inputs to the monitors and the monitoring results are collected. We generate 10 input signals for each model and specification. To accountfor fluctuation of monitoring times in different repetitions6 , for each signal, theexperiment has been executed 10 times, and we report average results.
5.2

Evaluation

Qualitative evaluation. We here show the type of information provided by
the different monitors. As an example, Fig. 7 reports, for two specifications of
the two models, the system output signal (in the top of the two sub-figures), andthe monitoring results of the compared monitors. We notice that signals of bothmodels (top plots) violate the corresponding specifications in multiple points.
AT
Let us consider monitoring results of φAFC
1 ; similar observations apply to φ1 .
When using the ClaM, only the first violation right after time 15 is detected(the upper bound of robustness becomes negative); after that, the upper boundremains constant, without reporting that the system recovers from violation ataround time 17, and that the specification is violated again four more times.
Instead, we notice that the monitor with reset ResM is able to detect all
the violations (as the upper bound becomes greater than 0 when the violation
episode ends), but it does not properly report the margin of robustness; indeed,
during the violation episodes, it reports a constant value of around −0.4 for theupper bound, but the system violates the specification with different degrees ofseverity in these intervals; in a similar way, when the specification is satisfied
around after time 17, the upper bound is just above 0, but actually the system
satisfies the specification with different margins. As a consequence, ResM provides
sharp changes of the robustness upper bound that do not faithfully reflect thesystem evolution.
6Note that only the monitoring time changes across different repetitions; monitoring
results are instead always the same, as monitoring is deterministic for a given signal.

Online Causation Monitoring of STL
alw_[10, 50](abs(AF[t]-AFref[t]) < 0.1 )

alw_[0,30](not(speed[t] > 50) or ev_[1,3](RPM[t] < 3000))

100

AF
AFref

16

17
speed
RPM

4000

50

14
16
0
14
0.5 0
0.5

alw_[10, 50](abs(AF[t]-AFref[t]) < 0.1 )
5
5

10
10

15
20
25
30
and AFref
15 Signals
20 AF 25
30

35
35

40
40

45AF 50
AFref
45
50

Upper robustness
Upper
Lower robustness
robustness
Lower robustness

100
0
500
0
500 0

alw_[0,30](not(speed[t] > 50) or ev_[1,3](RPM[t] < 3000))
5

10

500

15

20

2000

4000

25

Signals
speed
10
15 and RPM
20

5

25

speed
30 2000
RPM

Upper robustness
Lower robustnessUpperrobustness

30

Lower robustness

0

0

0

alw_[10, 50](abs(AF[t]-AFref[t]) < 0.1 )

0
-0.5
16
140
0
0.5

5
5

-0.5
00

5

10

-0.5
16 0
14
0

5

10

classic
monitor15
20
25 with
30reset
35

40

5

10

Classic
monitorwith
15
20
25 reset
30 ResM
35

40

⊕

10
10

15
20
25
30
15Classic
20 monitor
25 ClaM
30

35
35

40
40

45 AF 50
AFref
45
50

Upper robustness
Lower robustness

15

20

25

30

35

40

-500
100
50 0
0
0
500
-500

alw_[0,30](not(speed[t] > 50) or ev_[1,3](RPM[t] < 3000))
5

0

50

0

45 AF

50

45

50

100
-500
50 0
0
0
⊕1

45

alw_[10, 50](abs(AF[t]-AFref[t]) < 0.1 )
AFref

10

15

20

10

15

20

Classic monitor ClaM

5
5

10

15

25

25

4000

speed 302000
RPM

30

Upper robustness
25 robustness
30
Lower

20

alw_[0,30](not(speed[t] > 50) or ev_[1,3](RPM[t] < 3000))
4000

5
5

10

15

20

25
25

Classic
10 monitor with
15 reset ResM
20

speed 2000
30
RPM

30

Boolean causation monitor verdict

Boolean causation monitor verdict

⊘0

⊘

⊖
-1

alw_[10, 50](abs(AF[t]-AFref[t]) < 0.1 )

⊖16

0
14
0
0.5

5
5

10
15
20
25
30
35
monitor
10 Boolean
15 causation
20
25
30 BCauM
3540
40

45 AF 50
AFref
45
50

Violation causation distance
Satisfaction causation distance

1000
50
0
0
500

0

0

-0.5

-500

0

5

10

15

20

25

30

35

Quantitative causation monitor QCauM

40

45

50

(a) Specification φAFCand signal #4
1

alw_[0,30](not(speed[t] > 50) or ev_[1,3](RPM[t] < 3000))
5

0

5

10

15

20

10

15

20
25 distance 30
Violation
causation
Satisfaction causation distance10

15

Boolean causation monitor BCauM

520

Quantitative causation monitor QCauM

2525304000200030(b) Specification φAT
1 and signal #8

Fig. 7: Examples of the information provided by the different monitors

Table 1: Experimental results – Average (avg.) and standard deviation (stdv.)
of monitoring and simulation times (ms)ClaM
monitoravg. stdv.
φAFC
14.6
1
φAFC
26.8
2
φAFC
42.0
3
φAT
16.7
1

ResM

total
monitoravg. stdv. avg. stdv.

0.1 982.8
0.2 998.5
0.3 1016.5
0.2 966.0

BCauM

total
monitoravg. stdv. avg. stdv.

QCauM

total
monitoravg. stdv. avg. stdv.

3.5 8.8 2.4 981.3 6.7 36.9 5.4 1009.7 16.5 15.1
9.0 20.2 5.2 988.0 9.9 50.4 22.4 1023.9 25.1 27.4
8.9 45.5 4.8 1016.9 7.5 48.4 6.2 1021.2 7.9 81.0
2.6 24.0 17.0 980.4 24.2 96.1 82.6 1065.2 93.4 31.2

total
avg. stdv.

0.1 981.9
0.2 999.5
1.2 1060.1
0.6 985.0

4.4
8.2
5.3
7.5

We notice that the Boolean causation monitor BCauM only reports information
about the violation episodes, but not on the degree of violation/satisfaction. Instead, the quantitative causation monitor QCauM is able to provide a very detailed
information, not only reporting all the violation episodes, but also properly characterizing the degree with which the specification is violated or satisfied. Indeed,
in QCauM, the violation causation distance smoothly increases from violation tosatisfaction, so faithfully reflecting the system evolution.
Quantitative assessment of monitoring time. We discuss the computation
cost of doing the monitoring.
In Table 1, we observe that, for all the monitors, the monitor ing time is much
lower than the total time (system execution + monitoring). It shows that, forthis type of systems, the monitoring overhead is negligible. Still, we compare the18

Z. Zhang, J. An, P. Arcaini, I. Hasuo

Table 2: Experimental results of the four monitoring approaches – Monitoringtime (ms) – ∆A = (QCauM−A)/A
ClaM ResM BCauM QCauM
φAFC1

QCauM stat. (%)

ClaM ResM BCauM QCauM
φAFC2∆ClaM ∆ResM ∆BCauM
#1
#2
#3
#4
#5
#6
#7
#8
#9
#10

14.5 8.2
14.5 8.1
14.8 8.0
14.7 8.5
14.6 8.0
14.6 8.2
14.6 15.5
14.7 7.9
14.6 7.8
14.5 8.0

37.4
39.9
38.2
38.8
37.3
37.6
21.6
39.5
39.9
38.4

15.2
15.0
15.0
15.3
14.9
15.1
15.0
15.0
15.1
15.1

ClaM ResM BCauM QCauM
φAFC
3

4.8
3.4
1.4
4.1
2.1
3.4
2.7
2.0
3.4
4.1

85.4
85.2
87.5
80.0
86.3
84.1
-3.2
89.9
93.6
88.8

-59.4
-62.4
-60.7
-60.6
-60.1
-59.8
-30.6
-62.0
-62.2
-60.7

QCauM stat. (%)

#1
#2
#3
#4
#5
#6
#7
#8
#9
#10

26.8
27.1
26.6
26.6
26.7
26.6
26.8
26.9
27.1
26.7

19.8 45.9
27.3 27.6
26.2 30.0
14.2 107.2
15.8 50.9
15.8 56.4
25.4 33.5
17.0 51.9
25.1 50.9
15.8 50.1

27.4
27.8
27.5
27.0
27.3
27.2
27.5
27.4
27.6
27.3

ClaM ResM BCauM QCauM
φAT
1

42.1
42.5
41.8
42.0
41.7
41.7
42.3
42.1
42.3
41.6

49.2
42.2
48.8
34.9
48.9
48.5
42.7
42.2
49.1
48.6

49.1
42.2
48.8
63.4
48.7
48.7
42.5
42.0
49.3
49.1

81.2
82.1
81.5
78.8
79.6
79.7
81.9
81.6
82.6
80.8

92.9 65.0
93.2 94.5
95.0 67.0
87.6 125.8
90.9 62.8
91.1 64.3
93.6 91.8
93.8 93.4
95.3 68.2
94.2 66.3

65.4
94.5
67.0
24.3
63.4
63.7
92.7
94.3
67.5
64.6

2.2
2.6
3.4
1.5
2.2
2.3
2.6
1.9
1.8
2.2

38.4
1.8
5.0
90.1
72.8
72.2
8.3
61.2
10.0
72.8

-40.3
0.7
-8.3
-74.8
-46.4
-51.8
-17.9
-47.2
-45.8
-45.5

QCauM stat. (%)∆ClaM ∆ResM ∆BCauM∆ClaM ∆ResM ∆BCauM
#1
#2
#3
#4
#5
#6
#7
#8
#9
#10

QCauM stat. (%)∆ClaM ∆ResM ∆BCauM

#1
#2
#3
#4
#5
#6
#7
#8
#9
#10

16.9
16.7
16.7
16.9
16.8
16.5
16.6
16.8
16.3
16.5

30.7
17.4
16.8
69.7
19.6
26.5
14.6
16.4
13.9
14.2

29.6
17.4
253.4
70.2
135.9
200.5
37.9
143.8
38.6
33.2

32.1
31.9
31.0
31.8
31.0
30.2
31.0
31.4
31.0
30.9

89.9
4.6
91.0 83.3
85.6 84.5
88.2 -54.4
84.5 58.2
83.0 14.0
86.7 112.3
86.9 91.5
90.2 123.0
87.3 117.6

8.4
83.3
-87.8
-54.7
-77.2
-84.9
-18.2
-78.2
-19.7
-6.9

execution costs for the different monitors. Table 2 reports the monitoring timesof all the monitors for each specification and each signal. Moreover, it reports
the percentage difference between the quantitative causation monitor QCauM (themost informative one) and the other monitors.
We first observe that ResM and BCauM have, for the same specification, highvariance of the monitoring times across different signals. ClaM and QCauM, instead, provide very consistent monitoring times. This is confirmed by the standard deviation results in Table 1. The consistent monitoring cost of QCauM is agood property, as the designers of the monitor can precisely forecast how longthe monitoring will take, and design the overall system accordingly.
and φAFC
We observe that QCauM is negligibly slower than ClaM for φAFC
1
2 , andat most twice slower for the other two specifications. This additional monitoring
cost is acceptable, given the additional information provided by QCauM. Compared to ResM, QCauM is usually slower (at most around the double); also in thiscase, as QCauM provides more information than ResM, the cost is acceptable.
Compared to the Boolean causation monitor BCauM, QCauM is usually faster,
as it does not have to collect epochs, which is a costly operation. However, weobserve that it is slower in φAFC
3 , because, in this specification, most of the signals
do not violate it (and so also BCauM does not collect epochs in this case).
To conclude, QCauM is a monitor able to provide much more information thatexiting monitors, with an acceptable overhead in terms of monitoring time.

Online Causation Monitoring of STL

6

19

Related Work

Monitoring of STL. Monitoring can be performed either offline or online. Offline monitoring [16, 30, 33] targets complete traces and returns either true or
false. In contrast, online monitoring deals with the partial traces, and thus
a three-valued semantics was introduced for LTL monitoring [7, 8], and in further for MTL and STL qualitative online monitoring [24, 31], to handle thesituation where neither of the conclusiveness can be made. In usual, the quantitative online monitoring provides a quantitative value or a robust satisfaction
interval [12–14, 25, 26]. Based on them, several tools have been developed, e.g.,
AMT [32,33], Breach [15], S-Taliro [1], etc. We refer to the survey [3] for comprehensive introduction. Recently, in [35], Qin and Deshmukh propose clairvoyant
monitoring to forecast future signal values and give probabilistic bounds on thespecification validity. In [2], an online monitoring is proposed for perception
systems with Spatio-temporal Perception Logic [23].
Monotonicity issue. However, most of these works do not handle the monotonicity issue stated in this paper. In [10], Cimatti et al. propose an assumptionbased monitoring framework for LTL. It takes the user expertise into account andallows the monitor resettable, in the sense that it can restart from any discrete
time point. In [37], a recovery feature is introduced in their online monitor [25].
However, the technique is an application-specific approach, rather than a generalframework. In [40], a reset mechanism is proposed for STL online monitor. However, as experimentally evaluated in §5, it essentially provides a solution for the
Boolean semantics and still holds monotonicity between two resetting points.
Signal diagnostics. Signal diagnostics [5, 22, 32] is originally used in an offlinemanner, for the purpose of fault localization and system debugging. In [22], theauthors propose an approach to automatically address the single evaluations(namely, epochs) that account for the satisfaction/violation of an STL specification, for a complete trace. This information can be further used as a reference
for detecting the root cause of the bugs in the CPS systems [5, 6, 32]. The online
version of signal diagnostics, which is the basis of our Boolean causation monitor, is introduced in [40]. However, we show in §5 that the monitor based on
this technique is often costly, and not able to deliver the quantitative runtime
information compared to the quantitative causation monitor.

7

Conclusion and Future WorkIn this paper, we propose a new way of doing STL monitoring based on causation that is able to provide more information than classic monitoring based on
STL robustness. Concretely, we propose two causation monitors, namely BCauM
and QCauM. In particular, BCauM intuitively explains the concept of “causation”
monitoring, and thus paves the path to QCauM that is more practically valuable.
We further prove the relation between the proposed causation monitors and theclassic ones.

20

Z. Zhang, J. An, P. Arcaini, I. Hasuo

As future work, we plan to improve the efficiency the monitoring, by avoiding
some unnecessary computations for some instants. Moreover, we plan to apply
it to the monitoring of real-world systems.

References
1. Annpureddy, Y., Liu, C., Fainekos, G., Sankaranarayanan, S.: S-TaLiRo: A tool for
temporal logic falsification for hybrid systems. In: TACAS 2011. LNCS, vol. 6605,
pp. 254–257. Springer (2011). https://doi.org/10.1007/978-3-642-19835-9 21
2. Balakrishnan, A., Deshmukh, J., Hoxha, B., Yamaguchi, T., Fainekos, G.: PerceMon: Online monitoring for perception systems. In: RV 2021. pp. 297–308. Springer(2021). https://doi.org/10.1007/978-3-030-88494-9 18
3. Bartocci, E., Deshmukh, J.V., Donzé, A., Fainekos, G., Maler, O., Nickovic, D.,
Sankaranarayanan, S.: Specification-based monitoring of cyber-physical systems:
A survey on theory, tools and applications. In: Lectures on Runtime Verification- Introductory and Advanced Topics, LNCS, vol. 10457, pp. 135–175. Springer(2018). https://doi.org/10.1007/978-3-319-75632-5 5
4. Bartocci, E., Falcone, Y. (eds.): Lectures on Runtime Verification - Introductory and Advanced Topics, LNCS, vol. 10457. Springer (2018).
https://doi.org/10.1007/978-3-319-75632-5
5. Bartocci, E., Ferrère, T., Manjunath, N., Ničković, D.: Localizing faults inSimulink/Stateflow models with STL. In: HSCC 2018. pp. 197–206. ACM (2018).
https://doi.org/10.1145/3178126.3178131
6. Bartocci, E., Manjunath, N., Mariani, L., Mateis, C., Ničković, D.: CPSDebug:
Automatic failure explanation in CPS models. International Journal on Software
Tools for Technology Transfer 23(5), 1–14 (2021). https://doi.org/10.1007/s10009020-00599-4
7. Bauer, A., Leucker, M., Schallhart, C.: Monitoring of real-time properties. In: FSTTCS 2006. LNCS, vol. 4337, pp. 260–272. Springer (2006).
https://doi.org/10.1007/11944836 25
8. Bauer, A., Leucker, M., Schallhart, C.: Runtime verification for LTL and TLTL.
ACM Transactions on Software Engineering and Methodology 20(4), 1–64 (2011).
https://doi.org/10.1145/2000799.2000800
9. Ciccone, L., Dagnino, F., Ferrando, A.: Ain’t no stopping us monitoring now. arXiv
preprint arXiv:2211.11544 (2022)
10. Cimatti, A., Tian, C., Tonetta, S.: Assumption-based runtime verification with partial observability and resets. In: RV 2019. LNCS, vol. 11757, pp. 165–184. Springer(2019). https://doi.org/10.1007/978-3-030-32079-9 10
11. Decker, N., Leucker, M., Thoma, D.: Impartiality and anticipation for monitoring of visibly context-free properties. In: Legay, A., Bensalem, S. (eds.) Runtime
Verification. pp. 183–200. Springer Berlin Heidelberg, Berlin, Heidelberg (2013)
12. Deshmukh, J.V., Donzé, A., Ghosh, S., Jin, X., Juniwal, G., Seshia, S.A.: Robust online monitoring of signal temporal logic. Formal Methods in System Design51(1), 5–30 (2017). https://doi.org/10.1007/s10703-017-0286-7
13. Dokhanchi, A., Hoxha, B., Fainekos, G.: On-line monitoring for temporal logic
robustness. In: RV 2014. LNCS, vol. 8734, pp. 231–246. Springer (2014).
https://doi.org/10.1007/978-3-319-11164-3 19
14. Dokhanchi, A., Hoxha, B., Fainekos, G.: Metric interval temporal logic specification elicitation and debugging. In: MEMOCODE 2015. pp. 70–79. IEEE (2015).
https://doi.org/10.1109/MEMCOD.2015.7340472

Online Causation Monitoring of STL

21

15. Donzé, A.: Breach, A toolbox for verification and parameter synthesis of hybrid systems. In: CAV 2010. LNCS, vol. 6174, pp. 167–170. Springer (2010).
https://doi.org/10.1007/978-3-642-14295-6 17
16. Donzé, A., Ferrère, T., Maler, O.: Efficient robust monitoring for STL. In: CAV
2013. LNCS, vol. 8044, pp. 264–279. Springer (2013). https://doi.org/10.1007/9783-642-39799-8 19
17. Donzé, A., Maler, O.: Robust satisfaction of temporal logic over real-valued
signals. In: FORMATS 2010. LNCS, vol. 6246, pp. 92–106. Springer (2010).
https://doi.org/10.1007/978-3-642-15297-9 9
18. Ernst, G., Arcaini, P., Bennani, I., Chandratre, A., Donzé, A., Fainekos, G., Frehse,G., Gaaloul, K., Inoue, J., Khandait, T., Mathesen, L., Menghi, C., Pedrielli, G.,
Pouzet, M., Waga, M., Yaghoubi, S., Yamagata, Y., Zhang, Z.: ARCH-COMP
2021 category report: Falsification with validation of results. In: Frehse, G., Althoff, M. (eds.) 8th International Workshop on Applied Verification of Continuousand Hybrid Systems (ARCH21). EPiC Series in Computing, vol. 80, pp. 133–152.
EasyChair (2021). https://doi.org/10.29007/xwl1
19. Ernst, G., Arcaini, P., Bennani, I., Donzé, A., Fainekos, G., Frehse, G., Mathesen, L., Menghi, C., Pedrielli, G., Pouzet, M., Yaghoubi, S., Yamagata, Y.,
Zhang, Z.: ARCH-COMP 2020 category report: Falsification. In: 7th International Workshop on Applied Verification of Continuous and Hybrid Systems(ARCH20). EPiC Series in Computing, vol. 74, pp. 140–152. EasyChair (2020).
https://doi.org/10.29007/trr1
20. Ernst, G., Arcaini, P., Fainekos, G., Formica, F., Inoue, J., Khandait, T., Mahboob, M.M., Menghi, C., Pedrielli, G., Waga, M., Yamagata, Y., Zhang, Z.:
ARCH-COMP 2022 category report: Falsification with ubounded resources. In:
Frehse, G., Althoff, M., Schoitsch, E., Guiochet, J. (eds.) Proceedings of 9th International Workshop on Applied Verification of Continuous and Hybrid Systems(ARCH22). EPiC Series in Computing, vol. 90, pp. 204–221. EasyChair (2022).
https://doi.org/10.29007/fhnk
21. Fainekos, G.E., Pappas, G.J.: Robustness of temporal logic specifications forcontinuous-time signals. Theoretical Computer Science 410(42), 4262–4291 (2009).
https://doi.org/10.1016/j.tcs.2009.06.021
22. Ferrère, T., Maler, O., Nickovic, D.: Trace diagnostics using temporal implicants. In: ATVA 2015. LNCS, vol. 9364, pp. 241–258. Springer (2015).
https://doi.org/10.1007/978-3-319-24953-7 20
23. Hekmatnejad, M., Hoxha, B., Deshmukh, J.V., Yang, Y., Fainekos,
G.: Formalizing and evaluating requirements of perception systems
for automated vehicles using spatio-temporal perception logic (2022).
https://doi.org/10.48550/arxiv.2206.14372
24. Ho, H.M., Ouaknine, J., Worrell, J.: Online monitoring of metric temporal logic. In: RV 2014. LNCS, vol. 8734, pp. 178–192. Springer (2014).
https://doi.org/10.1007/978-3-319-11164-3 15
25. Jakšić, S., Bartocci, E., Grosu, R., Kloibhofer, R., Nguyen, T., Ničkovié, D.: Fromsignal temporal logic to FPGA monitors. In: MEMOCODE 2015. pp. 218–227.
IEEE (2015). https://doi.org/10.1109/MEMCOD.2015.7340489
26. Jakšić, S., Bartocci, E., Grosu, R., Nguyen, T., Ničković, D.: Quantitative monitoring of STL with edit distance. Formal methods in system design 53, 83–112(2018). https://doi.org/10.1007/s10703-018-0319-x
27. Jin, X., Deshmukh, J.V., Kapinski, J., Ueda, K., Butts, K.: Powertrain
control verification benchmark. In: HSCC 2014. pp. 253–262. ACM (2014).
https://doi.org/10.1145/2562059.2562140

22

Z. Zhang, J. An, P. Arcaini, I. Hasuo

28. Koymans, R.: Specifying real-time properties with metric temporal logic. RealTime Syst. 2(4), 255–299 (1990). https://doi.org/10.1007/BF01995674
29. Leucker, M., Schallhart, C.: A brief account of runtime verification.
The Journal of Logic and Algebraic Programming 78(5), 293–303 (2009).
https://doi.org/10.1016/j.jlap.2008.08.004
30. Maler, O., Ničković, D.: Monitoring temporal properties of continuous signals.
In: FORMATS/FTRTFT 2004, LNCS, vol. 3253, pp. 152–166. Springer (2004).
https://doi.org/10.1007/978-3-540-30206-3 12
31. Maler, O., Ničković, D.: Monitoring properties of analog and mixedsignal circuits. Int. J. Softw. Tools Technol. Transf. 15(3), 247–268 (2013).
https://doi.org/10.1007/s10009-012-0247-9
32. Ničković, D., Lebeltel, O., Maler, O., Ferrère, T., Ulus, D.: AMT 2.0: qualitative and quantitative trace analysis with extended signal temporal logic. International Journal on Software Tools for Technology Transfer 22(6), 741–758 (2020).
https://doi.org/10.1007/s10009-020-00582-z
33. Ničković, D., Maler, O.: AMT: A property-based monitoring tool for analog
systems. In: FORMATS 2007. LNCS, vol. 4763, pp. 304–319. Springer (2007).
https://doi.org/10.1007/978-3-540-75454-1 22
34. Pnueli, A.: The temporal logic of programs. In: FOCS 1977. pp. 46–57. IEEE
(1977). https://doi.org/10.1109/SFCS.1977.32
35. Qin, X., Deshmukh, J.V.: Clairvoyant monitoring for signal temporal logic. In:
FORMATS 2020. Lecture Notes in Computer Science, vol. 12288, pp. 178–195.
Springer (2020). https://doi.org/10.1007/978-3-030-57628-8 11
36. Sánchez, C., Schneider, G., Ahrendt, W., Bartocci, E., Bianculli, D., Colombo,
C., Falcone, Y., Francalanza, A., Krstić, S., Lourenço, J.M., et al.: A survey of challenges for runtime verification from advanced application domains(beyond software). Formal Methods in System Design 54(3), 279–335 (2019).
https://doi.org/10.1007/s10703-019-00337-w
37. Selyunin, K., Jaksic, S., Nguyen, T., Reidl, C., Hafner, U., Bartocci, E., Nickovic, D., Grosu, R.: Runtime monitoring with recovery of the SENT communication protocol. In: CAV 2017. LNCS, vol. 10426, pp. 336–355. Springer (2017).
https://doi.org/10.1007/978-3-319-63387-9 17
38. Zhang, Z., An, J., Arcaini, P., Hasuo, I.: Online causation monitoring of signal
temporal logic. arXiv (2023). https://doi.org/10.48550/arXiv.2305.17754
39. Zhang, Z., An, J., Arcaini, P., Hasuo, I.: Online Causation Monitoring of Signal Temporal Logic (Artifact). Zenodo (2023), https://doi.org/10.5281/zenodo.
7923888
40. Zhang, Z., Arcaini, P., Xie, X.: Online reset for signal temporal logic monitoring.
IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems
41(11), 4421–4432 (2022). https://doi.org/10.1109/TCAD.2022.3197693