## On-Line Monitoring for Temporal Logic Robustness

Adel Dokhanchi, Bardh Hoxha, and Georgios Fainekos

School of Computing, Informatics and Decision Systems Engineering Arizona State University f adokhanc,bhoxha,fainekos @asu.edu g

Abstract. In this paper, we provide a Dynamic Programming algorithm for online monitoring of the state robustness of Metric Temporal Logic specifications with past time operators. We compute the robustness of MTL with unbounded past and bounded future temporal operators (MTL &lt; + 1 + pt ) over sampled traces of Cyber-Physical Systems. We implemented our tool in Matlab as a Simulink block that can be used in any Simulink model. We experimentally demonstrate that the overhead of the MTL &lt; + 1 + pt robustness monitoring is acceptable for certain classes of practical specifications.

## 1 Introduction

Modern airplanes, automobiles and medical devices are prime examples of safety critical Cyber-Physical Systems (CPS). Nowadays, the majority of safety critical functions in such systems is controlled by embedded computers. Due to the critical nature of these components, it is of paramount importance to verify the functional correctness of the embedded software. However, as the number of computer controlled components increases so does the complexity of the verification of functional correctness. Moreover, the verification problem of most classes of CPS is even an undecidable problem [1].

As an alternative to verification and o GLYPH&lt;11&gt; -line testing, runtime monitoring has been proposed. The underlying idea is that given a set of formal requirements, these requirements are analyzed at runtime by an independent monitor and if a violation is detected, it is reported to a supervisor. The supervisor can then decide on remedial actions to fix the problem or reduce its impact to the system. The monitoring problem has been extensively studied [2-14] for the cases where the formal requirements are expressed in Linear Temporal Logic (LTL) [15] or in Metric Temporal Logic (MTL) [16].

In this paper, we revisit the MTL runtime monitoring problem when targeted to CPS. In particular, we claim that the classical Boolean semantics (or even three valued semantics) are not su GLYPH&lt;14&gt; ciently informative for CPS behaviors. For instance, consider the specification ' After a takeo GLYPH&lt;11&gt; command is received, then reach altitude of 600ft within 5 minutes ' for an autonomous Unmanned Aerial Vehicle (UAV) as introduced in [8]. Clearly, knowing that the specification failed or passed at runtime is important. However, more useful information from the perspective of the supervisor would be the knowledge of how far is the aircraft from satisfying the requirement. More specifically, -10ft from the requirement of 600ft at 1 min away from the 5 min threshold should potentially be less alarming than -100ft at exactly the same time. A supervisor that has a model of the dynamics of the aircraft can determine whether the UA V can climb 100ft

within 1 min or not. We remark that the determination of the climb rate can only occur at runtime since this depends on the atmospheric parameters, the payload of the UAV, etc. Hence, the climb rate cannot be a precomputed parameter unless it is very conservatively set.

Our goal is to construct MTL monitors for estimating the robustness of satisfaction [17-19]. Temporal logic robustness gives a quantitative interpretation of satisfaction of an MTL formula. In detail, if an MTL formula valuates to positive robustness " , then the specification is true and, moreover, the state sequences can tolerate perturbations up to " and still satisfy the specification. Similarly, if the robustness is negative, then the specification is false and, moreover, the state sequences under " perturbations still do not satisfy the specification. Thus, robust semantics can be used to give quantitative values to the satisfaction of MTL formulas when the target is CPS.

The challenge here is that automata based monitors [13, 14] cannot be synthesized for computing the robustness valuations. Therefore, formula rewriting methods [11] or dynamic programming [9] methods must be used. Here, we take the latter approach for combined unbounded past time and bounded future time MTL specifications. Since we are working with CPS, we assume that it is possible - if desired - to have a model predictive component in the system [20] which will provide a finite horizon prediction of the system behavior. That finite horizon prediction could be appended with the observed system behavior to provide a robustness estimate of a likely system behavior. Hence, it becomes possible to monitor specifications such as ' If at anytime in the past a takeo GLYPH&lt;11&gt; command is issued, then within 5 min the altitude of 600ft is reached '. Thus, such requirements can now be monitored using only the actual observed system behavior or the observed system behavior with the predicted system behavior.

Our contributions in this paper are as follows: We provide a dynamic programming algorithm for on-line monitoring of the robustness metric of MTL formulas with bounded future and unbounded past. In addition, we provide a Matlab Simulink tool-/ box that can be used in any Simulink model for runtime monitoring of MTL robustness. The memory usage of our method is bounded and its runtime overhead is negligible for practical applications. Additional benefits in utilizing an on-line monitor are that it can be used in temporal logic testing algorithms [21, 22], where it may be desirable that the simulation stops as soon as the property is violated, as well as in feedback control for MTL specifications. Although temporal logic robustness has been considered in previous works [17-19], the solutions were provided for o GLYPH&lt;11&gt; -line testing. To the best of our knowledge, this is the first attempt to solve the on-line MTL robustness monitoring problem e GLYPH&lt;14&gt; ciently.

## 2 Problem Formulation

In the following, we represent the set of natural numbers including zero by N and the finite interval of N up to m by N m = f 0 1 ; ; : : : ; m g . In this work, we consider monitoring of Cyber-Physical Systems (CPS). We assume that we have access to some discrete time execution or simulation traces of the CPS. We view (execution or simulation) traces as timed state sequences T = T T T 0 1 2 : : : T m = ( GLYPH&lt;28&gt; 0 ; s 0 ) ( GLYPH&lt;28&gt; 1 ; s 1 ) ( GLYPH&lt;28&gt; 2 ; s 2 ) : : : ( GLYPH&lt;28&gt; m ; sm ) where for each k 2 N m , GLYPH&lt;28&gt; k 2 R GLYPH&lt;21&gt; 0 is a time stamp and sk 2 S is a vector containing the

Fig. 1. Overview of the solution of the MTL &lt; + 1 + pt on-line monitoring problem. The monitored robustness values could be used as feedback to the CPS or it could be plotted to be observed by a human supervisor if needed.

![image](https://ac.marcodsn.me/arxiv-markdown-images/1408.0045v1-figure-b9385086-95de-4e9b-baef-0d0815690759.jpg)

values of the state variables of the system at each sampling instance k . For example, for m = 2, the trace T = (0 ; (2 ; 0 34))(0 1 : : ; (3 ; 0 356))(0 2 : : ; (2 ; 0 36)) captures the finite : time execution of a CPS with two state variables in the vector sk : one ranging over the natural numbers N and the other over the reals R . That is, for k = 1, the state of the system at time GLYPH&lt;28&gt; 1 = 0 1 was : s 1 = (3 ; 0 356) : 2 N GLYPH&lt;2&gt; R . We further assume that S = ( S ; d ) is a generalized quasi-metric space [23]. The existence of metrics is necessary so that distances can be defined for quantitative valuations of the atomic propositions [18, 21].

Throughout the paper, the variable i , which ranges over N , is used to represent the current simulation step or the current index of the sampling process. We assume a fixed sampling period for the monitored system. Thus, there exists a fixed time period between consecutive time stamps. For the fixed time period GLYPH&lt;1&gt; t &gt; 0, for all i GLYPH&lt;21&gt; 0, we have GLYPH&lt;28&gt; i + 1 GLYPH&lt;0&gt; GLYPH&lt;28&gt; i = GLYPH&lt;1&gt; t (or equivalently GLYPH&lt;28&gt; i = i GLYPH&lt;1&gt; t ). As a result, we can simply compute each time stamp GLYPH&lt;28&gt; i knowing the trace index (or simulation step) i by multiplication ( GLYPH&lt;28&gt; i = i GLYPH&lt;1&gt; t ). Therefore, we use the trace index (simulation step i ) as the reference of time.

The property of interest is stated in Metric Temporal Logic (MTL) with bounded future and unbounded past (MTL &lt; + 1 + pt ) for timed state sequences [11]. More specifically, at each time i , we would like to monitor safety requirements represented as MTL &lt; + 1 + pt formulas. These formulas capture safety properties of the system, such as bounded reactivity, which can be periodically analyzed for violation. In our formulation, we use the robust (quantitative) semantics [18] that quantify the distance between a given execution trace of a CPS and all the execution traces that violate the property. The robustness of a formula J ' K with respect to a trace T at time i is a value that measures how far is the trace from the satisfaction falsification. This measure is an extension of boolean val-/ ues representing satisfaction or falsification which is used in conventional monitoring. A positive robustness value means that the trace satisfies the property and a negative robustness means that the specification is not satisfied.

Our goal in this paper is to provide monitoring tools for temporal logic robustness. We assume that at each time i , the CPS outputs its current state si along with a finite prediction si + 1 , si + 2 , : : : , si + Hrz of horizon length Hrz 2 N (see Fig. 1). The horizon length Hrz will be formally defined in Sec. 4; however, informally, it is the required number of samples after time i so that any future requirements in the MTL specification GLYPH&lt;30&gt; are resolved, i.e., the horizon depends on the structure of the formula GLYPH&lt;30&gt; , Hrz = hrz ( GLYPH&lt;30&gt; ).

When dealing with CPS, there exist numerous methods by which such a prediction horizon (forecasting) can be computed [24-26].

Next, we formally define the main problem presented in this paper.

Problem 1 (MTL &lt; + 1 + pt Robustness Monitoring) Given an MTL &lt; + 1 + pt specification ' , a sampling instance i and an execution trace T = T T 0 1 : : : T m such that m = i + hrz ( ' ) , compute the current robustness estimate [ [ ' ] ]( T ; i ) at time GLYPH&lt;28&gt; i .

Intuitively, ' represents a system invariant that must hold at every point in the system execution. This can also be viewed as testing for the specification robustness [ [ GLYPH&lt;3&gt; ' ] ]( T ; 0), where GLYPH&lt;3&gt; is the operator for ' always in the future ' and ' is an arbitrary MTL &lt; + 1 + pt specification. However, instead of caring about the satisfaction of the formula at the beginning of the time, we care about the potential of violating ' for which we design an on-line monitor.

Overview of solution and summary of contributions: We provide an on-line monitoring approach for computing the robustness of an MTL &lt; + 1 + pt formula with respect to execution traces of a CPS. An overview of the solution for the MTL &lt; + 1 + pt on-line monitoring problem appears in Fig. 1. Our method monitors the behavior of a CPS as it executes. Our toolbox is also useful for applications where Simulink models are actually used for process monitoring (and not simulation). In addition, it can also be used for code generation for general MTL &lt; + 1 + pt monitors for deployment on actual systems. Our method computes the robustness of invariants [ [ ' ] ]( T ; i ) by storing previous specification robustness values - if needed - and by only utilizing a bounded number of pairs of the execution trace T Hst ; : : : ; T Hrz where Hst 2 N i and it will be formally defined in Sec. 4. Our monitor uses bounded memory and, in the worst case, it has quadratic time complexity that depends on the magnitude of Hrz GLYPH&lt;0&gt; Hst . In principle, our solution for robustness monitoring is inspired by the boolean temporal logic monitoring algorithm in [2].

## 3 Robustness of Metric Temporal Logic Specifications

In digital control and monitoring of CPS, it is inevitable that physical quantities are measured through a sampling process. As mentioned in the Problem Formulation section, when we mention time, we are actually referring to the corresponding sampling index i . With a slight abuse of notation and under the assumption of constant sampling rate, an execution trace T can also be represented by a function s : N i + Hrz ! S . The view of the sequence s 0 s 1 : : : si + Hrz as a function s simplifies the presentation of the robust semantics for MTL.

Using a metric d [23], we can define a distance function that captures how far away a point x 2 X is from a set S GLYPH&lt;18&gt; X . Intuitively, the distance function assigns positive values when x is in the set S and negative values when x is outside the set S . The metric d must be at least a generalized quasi-metric as described in [21] which also includes the case where d is a metric as it was introduced in [18].

Definition 1 (Signed Distance). Let x 2 X be a point, S GLYPH&lt;18&gt; X be a set and d be a metric. Then, we define the Signed Distance from x to S to be

$$\text{Dist} _ { d } ( x, S ) \coloneqq \begin{cases} - \inf \{ d ( x, y ) \, | \, y \in S \} & \text{if} \, x \notin S \\ \inf \{ d ( x, y ) \, | \, y \in X \bar { \ } S \} & \text{if} \, x \in S \end{cases}$$

where inf is the infimum.

Metric Temporal Logic (MTL) was introduced by Koymans [16] to reason about the quantitative timing properties of boolean signals. In this paper, we use the standard fragment of MTL with bounded future, but also we allow the use of past time operators.

Definition 2 (MTL &lt; + 1 + pt Syntax). Let AP be the set of atomic propositions and I be any non-empty interval of N , and I be any non-empty interval of N [ f + 1g . The set MTL &lt; + 1 + pt formulas is inductively defined as ' :: = &gt; j p j : ' j \_ ' j UI ' j S I ' where p 2 AP and &gt; stands for true .

Note that we use the number of samples to represent the time interval constraints of temporal operators. For example assume that GLYPH&lt;1&gt; t = 0 1, then the MTL formula : ^ [0 0 5] ; : a where the timing constraints are over time is instead represented by ^ [0 5] ; a in MTL &lt; + 1 + pt .

The propositional operators conjunction ( ^ ) and implication ( ! ) are defined the usual way. All other bounded future temporal operators can be syntactically defined using Until ( UI ), where GLYPH&lt;7&gt; (Next), ^ (Eventually), and GLYPH&lt;3&gt; (Always) are defined as GLYPH&lt;7&gt; ' GLYPH&lt;17&gt; &gt;U [1 1] ; ' , ^ I ' GLYPH&lt;17&gt; &gt;UI ' , and GLYPH&lt;3&gt; I ' GLYPH&lt;17&gt; : ^ I: ' respectively. The intuitive meaning of the U [ a b ; ] ' operator at sampling time i is a follows: has to hold at least until ' becomes true within the time interval of [ i + a i ; + b ] in the future. Similarly, all other bounded unbounded past temporal operators can be defined using Since ( / S I ), where GLYPH&lt;12&gt; (Previous), GLYPH&lt;144&gt; (Eventually in the past), and GLYPH&lt;26&gt; (Always in the past) are defined as GLYPH&lt;12&gt; ' GLYPH&lt;17&gt; &gt;S [1 1] ; ' , GLYPH&lt;144&gt; I ' GLYPH&lt;17&gt; &gt;S I ' , and GLYPH&lt;26&gt; I ' GLYPH&lt;17&gt; : GLYPH&lt;144&gt; I : ' respectively. The intuitive meaning of the S [ a b ; ] ' operator at sampling time i is as follows: since ' becomes true within the interval [ i GLYPH&lt;0&gt; b i ; GLYPH&lt;0&gt; a ] in the past, must hold till now (current time i ).

MTL &lt; + 1 + pt can state requirements over the observable trajectories of a CPS. In order to capture these requirements, each predicate p 2 AP is mapped to a subset of the metric space X . We use an observation map O to interpret each predicate p 2 AP . In other words, the observation map is defined as O : AP ! P X ( ) such that for each p 2 AP the corresponding set is O ( p ). Here, P S ( ) denotes the powerset of a set S . We define the robust valuation of an MTL &lt; + 1 + pt formula ' over a trace s as follows [17].

Definition 3 (MTL &lt; + 1 + pt Robustness Semantics). Let s be a trace s : N ! X, and O be an observation map O : AP ! P X , then the robust semantics of any formula ( ) ' 2

MTL &lt; + 1 + pt with respect to s is recursively defined as:

$$\ n u \in \L _ { + p t } \ v u n \ r e s p e c t o v s i n c e v e y u e j n e u a u s. \\ [ [ T ] ] ( s, i ) \coloneqq + \infty \\ [ [ p ] ] ( s, i ) \coloneqq \text{Dist} _ { d } ( s ( i ), \mathcal { O } ( p ) ) \\ [ [ \neg \varphi ] ( s, i ) \coloneqq - [ \varphi ] ( s, i ) \\ [ \psi \vee \varphi ] ( s, i ) \coloneqq [ \psi ] ( s, i ) \sqcup [ \varphi ] ( s, i ) \\ [ [ \psi \mathcal { U } _ { [ l, u ] } \varphi ] ( s, i ) \coloneqq \bigsqcup _ { j = i + l } ^ { i + u } \left ( [ \varphi ] ( s, j ) \sqcap \prod _ { k = l } ^ { j - 1 } [ \psi ] ( s, k ) \right ) \\ [ \psi \mathcal { S } _ { [ l ^ { \prime }, u ^ { \prime } } \rangle \varphi ] ( s, i ) \coloneqq \bigsqcup _ { j = max \{ 0, i - u ^ { \prime } \} } ^ { i - l ^ { \prime } } \left ( [ \varphi ] ( s, j ) \sqcap \prod _ { k = j + 1 } ^ { i } [ \psi ] ( s, k ) \right ) \\ v h e r e \sqcup \text{ stands for max, } \sqcap \text{ stands for min, } p \in \text{ AP, } l, u, l ^ { \prime } \in \mathbb { N } \text{ and } u ^ { \prime } \in \mathbb { N } \cup \{ \infty \}$$

where t stands for max, u stands for min, p 2 AP, l u l ; ; 0 2 N and u 0 2 N [ f1g . Furthermore, the symbol i in S 0 [ l ; u 0 i will be ) when u 0 = + 1 and ] when u 0 , + 1 .

We should point out that we use the extended definition of maximum ( t ) and minimum ( u ), with slight abuse of notation, we let max( ; ) = GLYPH&lt;0&gt;1 and min( ; ) = + 1 . i.e., over empty sets we treat min and max as infimum and supremum, respectively. For exact definition of infimum and supremum see [27].

## 4 Robustness Monitoring of MTL &lt; + 1 + pt

## 4.1 Finite horizon and history of MTL &lt; + 1 + pt

For each MTL &lt; + 1 + pt formula we define the finite horizon hrz ( ) as the number of samples we need to consider in the future. In MTL, the satisfaction of the formula depends on what will happen in the future. In bounded MTL, the finite horizon hrz ( ) is the number of steps (samples) which we need to consider in the future in order to evaluate the formula at the current time i . In other words, hrz ( ) is the number of steps into the future for which the truth value of the sub-formula depends on [2]. Similarly, we define the finite history hst ( ) of as the number of samples we need to look into the past. That is, the number of steps in the past for which the truth value of the sub-formula depends on. Intuitively, the hst ( ) is the size of the history we need to consider in order to keep track of what happened in the past to evaluate the formula at present time. The finite horizon and the history can be defined recursively. We define hrz ( ) (similar to h ( ) in [2]) and we add the recursive definition of hst ( ) in the following:

hrz p ( ) = 0 hst ( p ) = 0 hrz ( : ) = hrz ( ) hst ( : ) = hst ( ) hrz ( OP ' ) = max hrz f ( ; ) hrz ( ' ) g hst ( OP ' ) = max hst f ( ; ) hst ( ' ) g hrz ( U [ l u ; ] ' ) = max hrz f ( ) + u GLYPH&lt;0&gt; 1 ; hrz ( ' ) + u g hst ( U [ l u ; ] ' ) = max hst f ( ; ) hst ( ' ) g hrz ( S 0 [ l ; u 0 i ' ) = max hrz f ( ; ) hrz ( ' ) g hst ( S 0 [ l ; u 0 i ' ) = ( max hst f ( ) + u 0 GLYPH&lt;0&gt; 1 ; hst ( ' ) + u 0 g if u 0 , + 1 max hst f ( ) + l 0 GLYPH&lt;0&gt; 1 ; hst ( ' ) + l 0 g if u 0 = + 1

Table 1. Pre Vector and Robustness Table

| Pre[ k ]              | T k ; j   | column j )             | -2                        | -1                        | 0               | 1                    | 2                  |
|-----------------------|-----------|------------------------|---------------------------|---------------------------|-----------------|----------------------|--------------------|
|                       | row k +   | Time( i )              | i GLYPH<0> 2              | i GLYPH<0> 1              | i               | i + 1                | i + 2              |
|                       | 1 = '     | 2 ^ 3                  | ' ( s ; i GLYPH<0> 2)     | ' ( s ; i GLYPH<0> 1)     | ' ( s ; i )     | ' ( s ; i + 1)       | ' ( s ; i + 2)     |
|                       | 2         | GLYPH<3> [1 ; 2] q     | J K 2 ( s ; i GLYPH<0> 2) | J K 2 ( s ; i GLYPH<0> 1) | J K 2 ( s ; i ) | J K 2 ( s ; i + 1)   | J K 2 ( s ; i + 2) |
| 3 ( s ; i GLYPH<0> 3) | 3         | GLYPH<26> [0 ; + 1 ) p | J K 3 ( s ; i GLYPH<0> 2) | J K 3 ( s ; i GLYPH<0> 1) | J K 3 ( s ; i ) | J K 3 ( s ; i + 1)   | J K 3 ( s ; i + 2) |
| J K                   | 4         | p                      | J K 4 ( s ; i GLYPH<0> 2) | J K 4 ( s ; i GLYPH<0> 1) | J K 4 ( s ; i ) | J K 4 ( s ; i + 1)   | J K 4 ( s ; i + 2) |
|                       | 5         | q                      | J K 5 ( s ; i GLYPH<0> 2) | J K 5 ( s ; i GLYPH<0> 1) | J K 5 ( s ; i ) | J K J 5 ( s ; i + 1) | K 5 ( s ; i + 2)   |

J

K

J

K

J

K

J

K

J

K

where p 2 AP . Here, OP is any binary operator in propositional logic, and ; ' are MTL &lt; + 1 + pt formulas. For the unbounded S [0 ; + 1 ) operator, the computation of finite history is more involved and needs more explanation. Namely, we need to restate the dynamic programming algorithm for monitoring a sub-formula S [0 ; + 1 ) ' based on the following works [9, 5]. According to the robustness semantics, the robustness of S [0 ; + 1 ) ' at time i is as follows:

$$[ \psi \mathcal { S } _ { [ 0, + \infty ) } \varphi ] ( s, i ) = \bigsqcup _ { j = 0 } ^ { i } \left ( [ \varphi ] ( s, j ) \cap \prod _ { k = j + 1 } ^ { i } [ \psi ] ( s, k ) \right ) \\. \quad \dots \, \dots$$

also robustness of S [0 ; + 1 ) ' at time i GLYPH&lt;0&gt; 1 is

$$\left [ \psi \mathcal { S } _ { [ 0, + \infty ) } \varphi \right ] ( s, i - 1 ) = \bigsqcup _ { j = 0 } ^ { i - 1 } \left ( \left [ \varphi \right ] ( s, j ) \cap \prod _ { k = j + 1 } ^ { i - 1 } \left [ \psi \right ] ( s, k ) \right )$$

Thus, we can rewrite J S [0 ; + 1 ) ' K ( s ; i ) as

$$[ \psi \mathcal { S } _ { ( 0, + \infty ) } \varphi ] ( s, i ) & = [ \varphi ] ( s, i ) \sqcup \left ( [ \psi ] ( s, i ) \sqcap \left ( \bigsqcup _ { j = 0 } ^ { i - 1 } \left ( [ \varphi ] ( s, j ) \sqcap \prod _ { k = j + 1 } ^ { i - 1 } [ \psi ] ( s, k ) \right ) \right ) \right ) \\ & = [ \varphi ] ( s, i ) \sqcup \left ( [ [ \psi ] ] ( s, i ) \sqcap \left ( [ [ \psi \mathcal { S } _ { ( 0, + \infty ) } \varphi ] ( s, i - 1 ) \right ) \right )$$

Therefore, similar to [5] we recursively update the robustness of S [0 ; + 1 ) ' at the current time i and save it in a variable called ' Pre ' to reuse it for the computation of the next time step (see [5] for more details). As a result, when we have an unbounded past time operator, we do not need the full history table. However, if the formula contains a nested future time operator, we need to extend the history to be long enough to contain the actual values. In other words, although for unbounded past time operators we do not need the whole history table, we should still extend the history to be able to store the actual simulation values (not the predicted values) in ' Pre '.

## 4.2 Robustness Computation Algorithm

For each MTL &lt; + 1 + pt formula ' we construct a table called Robustness Table with width of Hst + 1 + Hrz , where Hrz = hrz ( ' ) is the finite horizon of the specification formula ' , and, Hst = Hrz + hst ( ' ), where hst ( ' ) is the finite history of the specification ' . Hst is extended conservatively due to the fact that ' Pre ' value can only store the robustness

## Algorithm 1 On-Line Monitor

Input : ' , s 0 i = si si + 1 : : : si + Hrz , d , O ; Global variables: T , Pre ; Output : T 1 0 ; ( robustness value ).

```
\text{Input: } \varphi, s _ { j } = s _ { i } s _ { i + 1 } \dots s _ { i + H r _ { 2 } }, d, O ; Global variables: T, \Pr e ; \text{Output: } T _ { 1, 0 } ( \text{robustness value} ). \\ \text{procedure Monitor} ( \varphi, s _ { j }, d, O ) & \quad \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
1: \text{ for } k \leftarrow 1 \, \overline { \varphi } \, \text{ do } \quad \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
2: \text{ for } k \leftarrow 1 \, \overline { \varphi } \rightarrow 0 \, \text{ then } \quad \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
3: \text{ end for } k \leftarrow 1 \, \overline { \varphi } \, \text{ do } \quad \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
4: \text{ for } j \leftarrow 1 - H s t \, \overline { \varphi } \rightarrow 0 \, \text{ then } \quad \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
5: \text{ end for } k \leftarrow 1 \, \overline { \varphi } \rightarrow 0 \, \text{ then } \quad \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
6: \text{ end for } k \leftarrow 1 - H s t \, \overline { \varphi } \rightarrow 0 \, \text{ then } \quad \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
7: \text{ end for } k \leftarrow 1 - H s t \, \overline { \varphi } \rightarrow 0 \, \text{ then } \quad \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
8: \text{ end if } k \leftarrow 1 - H s t \, \overline { \varphi } \rightarrow 0 \, \text{ then } \quad \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
9: \text{ end for } k \leftarrow 1 - H s t \, \overline { \varphi } \rightarrow 0 \, \text{ then } \quad \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \  \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \  \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \

1: \text{ for } k \leftarrow \leftarrow \leftarrow \leftarrow \rightarrow \leftarrow \rightarrow \leftarrow \rightarrow \leftarrow \rightarrow \leftarrow \rightarrow \leftarrow \rightarrow \rightarrow \leftarrow \rightarrow \rightarrow \rightarrow \rightarrow \rightarrow \rightarrow \rightarrow \rightarrow \rightarrow \rightarrow \rightarrow \rightarrow \rightarrow \rightarrow \rightarrow \rightarrow \rightarrow \rightarrow \rightarrow \rightarrow \rightarrow \rightarrow \rightarrow \rightarrow \rightarrow \rightarrow \rightarrow \rightarrow \rightarrow \rightarrow \rightarrow \rightarrow \rightarrow \rightarrow \rightarrow \rightarrow \rightarrow \rightarrow \rightarrow \rightarrow \rightarrow \rightarrow \rightarrow \rightarrow \rightarrow \rightarrow \rightarrow \rightarrow \rightarrow \rightarrow \rightarrow \rightarrow \rightarrow \rightarrow \rightarrow \rightarrow \rightarrow \rightarrow \rightarrow \rightarrow \rightarrow \rightarrow \rightarrow \rightarrow \rightarrow \rightarrow \rightarrow
\text{end for } k \leftarrow \leftarrow \leftarrow \leftarrow \rightarrow \rightarrow \rightarrow \rightarrow \rightarrow \rightarrow \rightarrow \rightarrow \rightarrow \rightarrow \rightarrow \rightarrow \rightarrow \rightarrow \rightarrow \rightarrow \rightarrow \rightarrow \rightarrow \rightarrow \rightarrow \rightarrow \rightarrow \rightarrow \rightarrow \rightarrow \rightarrow \rightarrow \rightarrow \rightarrow \rightarrow \rightarrow \rightarrow \rightarrow \rightarrow \rightarrow \rightarrow \rightarrow \rightarrow \rightarrow \rightarrow \rightarrow \rightarrow \rightarrow \rightarrow \rightarrow \rightarrow \rightarrow \rightarrow \rightarrow \rightarrow \rightarrow \rightarrow \rightarrow \rightarrow \rightarrow \rightarrow \rightarrow \rightarrow \rightarrow \rightarrow \rightarrow \rightarrow \rightarrow \rightarrow
\text` \text` \text` \text` \text` \text` \text` \text` \text` \text` \text` \text` \text` \text` \text` \text` \text` \text` \text` \text` \text` \text` \text` \text` \text` \text` \text` \text` \text` \text` \text` \text` \text` \text` \text` \text` \text` \text` \text` \text` \text` \text` \text` \text` \text` \text` \text` \text` \text` \text` \text` \text` \text` \text` \text` \text` \text` \text` \text` \text` \text` \text` \text` \text` \text` \text` \text` \text$ \text` \text` \text` \text` \text` \text` \text` \text` \text` \text` \text` \text` \text` \text` \text` \text` \text` \text` \text` \text` \text` \text` \text` \text` \text` \text` \text` \text` \text` \text` \text` \text` \text` \text` \text` \text` \text` \text` \text` \text` \text` \text` \text` \text` \text` \text` \text` \text` \text` \text` \text` \text` \text` \text` \text` \text` \text` \text` \text` \text` \text` \text` \text` \text` \text` \text` \end{array} }
```

values corresponding to the actual simulation. The height of the robustness table is the size of the formula ' ( j ' j ), where j ' j is the number of sub-formulas of ' including itself. For example, assume we have a formula ' = GLYPH&lt;26&gt; [0 ; + 1 ) p ^ GLYPH&lt;3&gt; [1 2] ; q and we intend to compute [ [ ' ] ]( T ; i ) at each time i . In formula ' , Hst = 2 and Hrz = 2. Since ' has unbounded past-time operators, it needs the Pre vector as well as the Robustness Table. The Pre vector appended to the Robustness Table is presented in Table 1. In particular, the Pre vector contains the value of past sub-formulas from the beginning of the time up to the current time.

In the following, we explain how the values of Table 2, the robustness table, are computed using Algorithms 1 and 2. In order to make our algorithms more readable, we used a vector to show the CPS output si , si + 1 , : : : , si + Hrz to the monitoring (see Fig. 1). We define a vector s 0 i = si si + 1 : : : si + Hrz which appends current state si with predictions si + 1 , si + 2 , : : : , si + Hrz . In Table 1, i is the current simulation step which corresponds to column 0. At each simulation step i , for each unbounded past time sub-formula GLYPH&lt;30&gt; , we first save the values of the column GLYPH&lt;0&gt; Hst + hst ( GLYPH&lt;30&gt; ) in the Pre vector (Algorithm 1 lines 1-3) since the column GLYPH&lt;0&gt; Hst + hst ( GLYPH&lt;30&gt; ) contains the robustness value of GLYPH&lt;30&gt; from the beginning of the simulation. We need the Pre vector to compute the robustness of GLYPH&lt;30&gt; at the next sampling time using the dynamic programming method. In the above example, for

Table 2. Robustness Computation of each table entries (Gray cells are unused)

| T k ; j   | i GLYPH<0> 2                        | i GLYPH<0> 1                        | i                          | i + 1                       | i + 2                       |
|-----------|-------------------------------------|-------------------------------------|----------------------------|-----------------------------|-----------------------------|
| k + , j ) | j = GLYPH<0> 2                      | j = GLYPH<0> 1                      | j = 0                      | j = 1                       | j = 2                       |
| Pre[1]    | T 2 ; GLYPH<0> 2 u T 3 ; GLYPH<0> 2 | T 2 ; GLYPH<0> 1 u T 3 ; GLYPH<0> 1 | T 2 ; 0 u T 3 ; 0          | T 2 ; 1 u T 3 ; 1           | T 2 ; 2 u T 3 ; 2           |
| Pre[2]    | T 5 ; GLYPH<0> 1 u T 5 ; 0          | T 5 ; 0 u T 5 ; 1                   | T 5 ; 1 u T 5 ; 2          | T 5 ; 2                     | + 1                         |
| Pre[3]    | Pre[3] u T 4 ; GLYPH<0> 2           | T 3 ; GLYPH<0> 2 u T 4 ; GLYPH<0> 1 | T 3 ; GLYPH<0> 1 u T 4 ; 0 | T 3 ; 0 u T 4 ; 1           | T 3 ; 1 u T 4 ; 2           |
| Pre[4]    | Dist d ( s i GLYPH<0> 2 ; O ( p ))  | Dist d ( s i GLYPH<0> 1 ; O ( p ))  | Dist d ( s i ; O ( p ))    | Dist d ( s i + 1 ; O ( p )) | Dist d ( s i + 2 ; O ( p )) |
| Pre[5]    | Dist d ( s i GLYPH<0> 2 ; O ( q ))  | Dist d ( s i GLYPH<0> 1 ; O ( q ))  | Dist d ( s i ; O ( q ))    | Dist d ( s i + 1 ; O ( q )) | Dist d ( s i + 2 ; O ( q )) |

Input : ' k , j , s 0 i = si si + 1 : : : si + Hrz , d , O ; Global variables: T , Pre ; Output : Tk j ; .

```
Algorithm 2 Robustness Computation (CR)

Input: \varphi _ { k }, j, s _ { j } = s _ { i } s _ { i + 1 } \dots s _ { i + H r _ { z } }, d, O ; Global variables: T, Pre ; Output: T _ { k, j }.

    procedure CR(\varphi _ { k }, j, s _ { j }, d, O )                                                                                                                                                                                                        
1:   if \varphi _ { k } = T  then T _ { k, j } \leftarrow + \infty                                                                                                                                                                                                        1:   else if \varphi _ { m } S _ { j } ( r _ { v } ) \varphi _ { n }                                                                                                                                                                                                        2:                                                                                                                                                                                                        3:                                                                                                                                                                                                       3                                                                                                                                                                                                        0:                                                                                                                                                                                                       0                                                                                                                                                                                                        4:                                                                                                                                                                                                       4                                                                                                                                                                                                        6:                                                                                                                                                                                                       6                                                                                                                                                                                                        5:                                                                                                                                                                                                       5                                                                                                                                                                                                        7:                                                                                                                                                                                                       7                                                                                                                                                                                                        8:                                                                                                                                                                                                       8                                                                                                                                                                                                        9:
```

GLYPH&lt;26&gt; [0 ; + 1 ) p the value at column GLYPH&lt;0&gt; 2 is saved in Pre to be used during robustness computation. Then, we shift all the robustness table entries of the predicates by one position to the left (Algorithm 1, lines 4-10). Then the loop (Algorithm 1, lines 11-21) recursively calls Algorithm 2 to fill the robustness table for each sub-formula from bottom to top.

Each call of Algorithm 2 (CR) computes each table entry Tk j ; (see tables 1,2) where column j is the horizon history index and row / k is the sub-formula index. For past subformulas the table entries are computed from left to right (Algorithm 1, lines 13-15), and for future sub-formulas the table entries are computed from right to left (Algorithm 1, lines 17-19). New values for predicates (according to execution traces) will be placed in column 0 and the predicted values of the predicates will be saved in columns 1 to Hrz (Algorithm 2, lines 2-5). Table 2 shows the updates of predicate values in rows 4, and 5 which correspond to Algorithm 2, line 4.

In the following, we explain how the CR Algorithm 2 computes the MTL robustness values for three di GLYPH&lt;11&gt; erent cases of MTL:

Case 1 (Lines 10-20): The robustness of bounded future temporal sub-formulas with interval [ l ; u ] at each column j is computed given the values of its operands for columns j up-to min j f + u Hrz ; g (Line 14). For example, this case is used in Table 2 to compute the robustness of sub-formula 2 = GLYPH&lt;3&gt; [1 2] ; q from right to left. Case 1 in CR Algorithm is similar to the DP-TALIRO algorithm [28].

Case 2 (Lines 23-28): The robustness of bounded past temporal sub-formulas with interval [ l 0 ; u 0 ] at each column j is computed given the values of its operands for columns j down-to j GLYPH&lt;0&gt; u 0 (Line 25).

Case 3 (Lines 30-36): The robustness of unbounded past temporal sub-formulas with interval [ l 0 ; + 1 ) for column j is computed using the stored value in column j GLYPH&lt;0&gt; 1 in dynamic programming fashion (Line 33) and using the Pre vector (Line 31). For example, Case 3 is used to compute the robustness of 3 = GLYPH&lt;26&gt; [0 ; + 1 ] p using Pre [3] from left to right in Table 2.

Finally, we update table entries for the top row which corresponds to 1 = ' . Since its corresponding operator ^ is propositional (Algorithm 2 Lines 6-9), we can update its value from any direction. The high level explanation of Algorithm 1 is described as follows:

- 1. Store values of column GLYPH&lt;0&gt; Hst + hst ( GLYPH&lt;30&gt; k ) for each unbounded past sub-formula GLYPH&lt;30&gt; k in Pre k [ ] and shift the table entries of predicates one to the left (Lines 1-10).
- 2. For each row i from j ' j to 1 compute the robustness values according to:
- (a) If ' i is a future temporal operator, for each column j from Hrz down to GLYPH&lt;0&gt; Hst + hst ( ' i ), update table entry Ti j ; using Algorithm 2.
- (b) If ' i is a past temporal operator, for each column j from GLYPH&lt;0&gt; Hst + hst ( ' i ) up to Hrz update table entry Ti j ; using Algorithm 2.
- 3. Return the robustness ( T 1 0 ; ).

We provided the proof of this section in Appendix.

## 5 Experimental Analysis and Case Studies

## 5.1 Runtime Overhead

First, we measure the overhead of the proposed monitoring framework on a slightly modified version of the Automatic Transmission (AT) model provided by Mathworks as a Simulink demo 1 . The experiments were conducted on a Windows 7, Intel Core2 Quad (2.99 GHz) with 8 GB RAM.

The physical model of the AT system has two continuous (real-valued) state variables which are also its monitored outputs: the speed of the engine ! and the speed of the vehicle v . The model includes an automatic transmission controller that exhibits both continuous and discrete behavior. It is a typical CPS model and specifications over both boolean and continuous variables can be formalized. However, since the valuation of the robustness of predicates over continuous state variables is computationally more expensive than a boolean valuation, we consider only specifications over continuous state variables for the impact analysis.

We introduce our MTL &lt; + 1 + pt monitoring block in the AT model and test the performance over a set of specifications. In order to test the runtime overhead of our work, we artificially generate 30 di GLYPH&lt;11&gt; erent MTL &lt; + 1 + pt formulas based on typical critical safety formulas to show that the runtime overhead depends on both of the size of the formula and the horizon history. We test our method for 100 runs of monitoring algorithm for / each specification (formula), and for each run we use 100 simulation steps. Then, we compute the mean and variance of the overhead for each simulation step which is the

1 Available at: http://www.mathworks.com/help/simulink/examples/ modeling-an-automatic-transmission-controller.html

Table 3. The overhead on each simulation step on the Automatic Transmission model with specifications of increasing length. Table entries are in milliseconds.

| #                 | H = 1,000   | H = 1,000   | H = 1,000   | H = 1,000   | H = 2,000   | H = 2,000   | H = 2,000   | H = 2,000   | H = 10,000   | H = 10,000   | H = 10,000   |
|-------------------|-------------|-------------|-------------|-------------|-------------|-------------|-------------|-------------|--------------|--------------|--------------|
|                   | E           | E           | U           | U           | E           | E           | U           | U           | E            | U            | U            |
|                   | Mean        | Var.        | Mean        | Var.        | Mean        | Var.        | Mean        | Var.        | Mean Var.    | Mean Var.    |              |
| GLYPH<30> 1 ( H ) | 2.39        | 0.00        | 4.83        | 0.00        | 8.03        | 0.00        | 15.8        | 0.001       | 188.8 0.001  | 358.5 0.036  |              |
| GLYPH<30> 3 ( H ) | 4.24        | 0.00        | 7.5         | 0.001       | 12.7        | 0.00        | 25.09       | 0.005       | 314.4 0.01   | 599 0.665    |              |
| GLYPH<30> 5 ( H ) | 4.66        | 0.00        | 8.36        | 0.001       | 14.01       | 0.00        | 27.8        | 0.005       | 309.2 0.077  | 650 0.014    |              |
| GLYPH<30> 7 ( H ) | 4.95        | 0.00        | 8.94        | 0.00        | 14.83       | 0.00        | 29.33       | 0.006       | 311 0.013    | 674.2 0.033  |              |
| GLYPH<30> 9 ( H ) | 5.23        | 0.00        | 9.46        | 0.001       | 15.4        | 0.001       | 30.56       | 0.007       | 317.5 0.011  | 683.5 0.698  |              |

execution time of Algorithm 1 in Table 3. In this table, the overhead is measured on specifications that contain either nested Until operators (U columns) or nested Eventually operators (E columns).

We generate 30 formulas according to the following templates:

- -E formulas: GLYPH&lt;30&gt; n ( H ) = pj GLYPH&lt;0&gt; ! n ( H n = )

where H 2 N is the finite horizon of the formula. In Table 3, we used 1,000, 2,000 and 10,000 for the size of the horizon. Here, pj is an arbitrary predicate and n ( H n = ) is defined recursively as follows:

where h = H n = , i.e., the finite horizon H divided by the number of nested subformulas n and ; are arbitrary predicates.

- 1 ( h ) = ^ [0 ; h ] pk and n ( h ) = ^ [0 ; h ] ( pl ^ n GLYPH&lt;0&gt; 1 ( h )), for 1 &lt; n GLYPH&lt;20&gt; 9 pk pl
- -U formulas: GLYPH&lt;30&gt; n ( H ) = pj GLYPH&lt;0&gt; ! n ( H n = ) where H 2 N is the finite horizon of the formula. In Table 3, we used 1,000, 2,000 and 10,000 for the size of the horizon of H . Here, pj is an arbitrary predicate and n ( H n = ) is defined recursively as follows:
- 1 ( h ) = pk U [0 ; h ] pl and n ( h ) = pm U [0 ; h ] ( pn ^ n GLYPH&lt;0&gt; 1 ( Y )), for 1 &lt; n GLYPH&lt;20&gt; 9 are arbitrary predicates.

where h = H n = and pk ; pl ; pm ; pm

As illustrated in Table 3, the computational complexity of the monitoring algorithm is closely related to the horizon and history size. Since the algorithm's complexity is of order O n ( 2 ) where n is the horizon history, the added overhead (in worst case execution) / is quadratic in terms of the size of the horizon for some formulas in Table 3 (like GLYPH&lt;30&gt; 1 ( H )). Moreover, in most cases, the impact of the number of nested temporal operators is not significant compared to the size of horizon history windows. From Table 3, we / notice that when the horizon and history size is less than 2,000, the overhead for each simulation step is negligible with our prototype implementation. Furthermore, for most practical reactivity requirements, it is quite unlikely that even a window size of 2,000 sampling points is necessary. Therefore, the method could be utilized in real world monitoring applications.

## 5.2 Case Study

In the following, we utilize the monitoring method on an industrial size high-fidelity engine model. The model is part of the SimuQuest Enginuity [29] Matlab Simulink tool /

package. The Enginuity tool package includes a library of modules for engine component blocks. It also includes pre-assembled models for standard engine configurations. In this work, we use the Port Fuel Injected (PFI) spark ignition, 4 cylinder inline engine configuration. It models the e GLYPH&lt;11&gt; ects of combustion from first physics principles on a cylinder-by-cylinder basis, while also including regression models for particularly complex physical phenomena. The model includes a tire-model, brake system model, and a drive train model (including final drive, torque converter and transmission). The input to the system is the throttle schedule. The output is the normalized air-to-fuel(A F) ra-/ tio. Simulink reports that this is a 56 state model. Note that this number represents only the visible states. It is possible that more states are present in the blackbox s-functions which are not accessible. This is a high dimensional non-linear system for which reachability analysis is very di GLYPH&lt;14&gt; cult. It also includes lookup tables, non-linear components, and inputs that a GLYPH&lt;11&gt; ect the switching guards.

## Enginuity High-Fidelity Engine Model with On-Line Monitoring

Fig. 2. SimuQuest [29] Enginuity Matlab Simulink engine model with the on-line monitoring block.

![image](https://ac.marcodsn.me/arxiv-markdown-images/1408.0045v1-figure-5e783845-f648-477f-85a7-c713fa0450ca.jpg)

A specification of practical interest for an engine is the settling time for the A F / ratio, which is the quotient between the air mass and fuel mass flow. Ideally, the normalized A F ratio / GLYPH&lt;21&gt; should always be 1, indicating that the ratio of the air and fuel flow is the same as the stoichiometric ratio. Under engine operating conditions, this output fluctuates GLYPH&lt;6&gt; %10. We add the on-line monitoring block to the Simulink model as presented in Fig. 2.

Our goal is to monitor the engine while allowing temporary fluctuations to GLYPH&lt;21&gt; . We formally define the specification as follows:

GLYPH&lt;30&gt; pt = ( GLYPH&lt;21&gt; out of bounds) ! GLYPH&lt;144&gt; [0 1] ; [0 1] ; : ( GLYPH&lt;21&gt; out of bounds)

GLYPH&lt;26&gt; Here, the formal specification states that if the A F ratio exceeds the allowed bounds, / then the ratio should have been settled for at least one second within the last two seconds.

Notice that an alternative presentation of the formula would be to use the future eventually and always operators, i.e. the formula would be defined as follows:

Fig. 3. Runtime monitoring of specifications GLYPH&lt;30&gt; pt , GLYPH&lt;30&gt; f t and GLYPH&lt;30&gt; pt f t on the high-fidelity engine model. The figure presents a normalized stoichiometric ratio, and the corresponding robustness values for specifications GLYPH&lt;30&gt; pt , GLYPH&lt;30&gt; f t and GLYPH&lt;30&gt; pt f t . Note that no predictor is utilized when computing the robustness values.

![image](https://ac.marcodsn.me/arxiv-markdown-images/1408.0045v1-figure-4bcaf7f9-cd9f-419f-bfa9-241b56ca9ffc.jpg)

![image](https://ac.marcodsn.me/arxiv-markdown-images/1408.0045v1-figure-4d4d445a-59e8-470a-9db5-7af249663d00.jpg)

![image](https://ac.marcodsn.me/arxiv-markdown-images/1408.0045v1-figure-eca2d5e0-2e58-4151-82dc-e97f334e1305.jpg)

![image](https://ac.marcodsn.me/arxiv-markdown-images/1408.0045v1-figure-3a87613e-1067-458d-90fa-49a8ee770f81.jpg)

## GLYPH&lt;30&gt; f t = ( GLYPH&lt;21&gt; out of bounds) ! ^ [0 1] ; GLYPH&lt;3&gt; [0 1] ; : ( GLYPH&lt;21&gt; out of bounds)

In this case, the specification states that always, if the A F ratio output exceeds the / allowed bounds, then within one second it should settle inside the bounds and stay there for a second.

Clearly, both GLYPH&lt;30&gt; pt and GLYPH&lt;30&gt; f t are equivalent in terms of the set of traces that satisfy falsify / each specification 2 . However, in real-time robustness monitoring, there is an important distinction between the two. When the specification requires future information, either a predictor is put in place or the semantics will handle only the current information. In this case, without a predictor, the future time formula reduces to the propositional formula GLYPH&lt;30&gt; f t = ( GLYPH&lt;21&gt; out of bounds) !: ( GLYPH&lt;21&gt; out of bounds) GLYPH&lt;17&gt; ( GLYPH&lt;21&gt; out of bounds). Therefore, past time operators should be used. Recall that when monitoring robustness, our goal is to provide early warning on when the specification may fail by approaching dangerously an undesired threshold. In other words, the past formula allows us to reason about the robustness of the actual system observations, while the future formula in collaboration with a forecast model would allow us to estimate the likely robustness. This is in contrast to many boolean monitoring algorithms which issue an ' undecided until further notice ' verdict that does not provide any actionable information.

A third alternative monitoring specification is the following formula:

2 Formally, this is the case if we ignore the first 2 seconds of the execution trace as well as the last 2 seconds - if the execution trace is finite.

GLYPH&lt;30&gt; pt f t = [0 2] ; (( GLYPH&lt;21&gt; out of bounds) ! ^ [0 1] ; GLYPH&lt;3&gt; [0 1] ; : ( GLYPH&lt;21&gt; out of bounds))

GLYPH&lt;26&gt; This specification states that at some point in the last two seconds, when GLYPH&lt;21&gt; is out of bounds then within the next second, GLYPH&lt;21&gt; will not be out of bounds and stay there for one second. This alternative seems to be the balance between the GLYPH&lt;30&gt; pt and GLYPH&lt;30&gt; f t formulas. Where GLYPH&lt;30&gt; pt purely relies on past information, and GLYPH&lt;30&gt; f t relies on information from a predictor, GLYPH&lt;30&gt; pt f t has the advantage that it utilizes both the information from the past but also it could include information from the predictor.

An example of real-time monitoring on the high-fidelity engine model is presented in Fig. 3. The figure illustrates the significance of using past time operators when defining specifications. Due to the lack of predictor information, the GLYPH&lt;30&gt; f t monitor falsely returns falsification at about 4 seconds whereas the GLYPH&lt;30&gt; pt monitor does not.

In the following, we analyze the overhead of the monitoring algorithm for this case study. Since the runtime is influenced by numerous sources of nondeterminism, we apply the central limit theorem to form confidence intervals for the mean simulation runtime when running the simulations with and without the monitor. To generate the results in Table 4, we collected 30 samples with 100 simulation runtimes in each sample. We note that the di GLYPH&lt;11&gt; erence between the estimated mean simulation runtime when adding the monitor is 0.97%. The experimental results were generated on an Intel Xeon X5647 (2.993GHz, 8 CPUs) machine with 12 GB RAM, Windows 7, and Matlab 2012a.

Table 4. Simulation runtime statistics for the high-fidelity engine model running for 35 seconds with simulation stepsize of 0.01s. The results include the confidence intervals for the mean simulation runtime.

| Simulation runtime(sec.)   | Est. Mean   | Est. Std. Dev   | 95%    | 95%    | 99%    | 99%    |
|----------------------------|-------------|-----------------|--------|--------|--------|--------|
|                            |             |                 | LB     | UB     | LB     | UB     |
| Without monitor            | 10.811      | 0.090           | 10.778 | 10.844 | 10.766 | 10.857 |
| With monitor               | 10.987      | 0.086           | 10.955 | 11.019 | 10.944 | 11.030 |

## 6 Conclusions and Future Work

We have presented an algorithm for monitoring the robustness of combined past and future MTL specifications. Our framework can incorporate predicted or estimated data as provided by a model predictive component. We have created a Simulink toolbox for MTL robustness monitoring which is distributed with the S-Taliro tools [30]. Our experiments indicate that the toolbox adds minimal overhead to the simulation time of Simulink models and it can be used for both runtime analysis of the models and for o GLYPH&lt;11&gt; -line testing. Our future work will concentrate on several aspects. First, the current version of the tool allows reasoning over timed state sequences generated under a constant sampling rate. We would like to relax this constraint so that we allow arbitrary sampling functions. Second, we would like to investigate the possibility of porting our monitor on FPGA platforms similar to [2, 8]. Finally, we envision that utilizing information about the system through the form of a model will permit us to move to an event based monitoring framework while still su GLYPH&lt;14&gt; ciently approximating the robustness estimate.

Acknowledgments This work was partially supported by NSF awards CNS 1116136 and CNS 1319560. The authors would also like to thank the anonymous reviewers for the very detailed comments.

## References

- 1. Alur, R., Courcoubetis, C., Halbwachs, N., Henzinger, T.A., Ho, P.H., Nicollin, X., Olivero, A., Sifakis, J., Yovine, S.: The algorithmic analysis of hybrid systems. Theoretical Computer Science 138 (1995) 3-34
- 2. Finkbeiner, B., Kuhtz, L.: Monitor circuits for ltl with bounded and unbounded future. In: Runtime Verification. Volume 5779 of LNCS., Springer (2009) 60-75
- 3. Havelund, K., Rosu, G.: Monitoring programs using rewriting. In: Proceedings of the 16th IEEE international conference on Automated software engineering. (2001)
- 4. Havelund, K., Rosu, G.: Synthesizing monitors for safety properties. In: Tools and Algorithms for the Construction and Analysis of Systems. Number 2280 in LNCS, Springer (2002) 342-356
- 5. Havelund, K., Rosu, G.: E GLYPH&lt;14&gt; cient monitoring of safety properties. STTT 6 (2004) 158-173
- 6. Kristo GLYPH&lt;11&gt; ersen, K.J., Pedersen, C., Andersen, H.R.: Runtime verification of timed LTL using disjunctive normalized equation systems. In: Proceedings of the 3rd Workshop on Run-time Verification. Volume 89 of ENTCS. (2003) 1-16
- 7. Maler, O., Nickovic, D.: Monitoring temporal properties of continuous signals. In: Proceedings of FORMATS-FTRTFT. Volume 3253 of LNCS. (2004) 152-166
- 8. Reinbacher, T., Rozier, K.Y., Schumann, J.: Temporal-logic based runtime observer pairs for system health management of real-time systems. In: Proceedings of the 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Volume 8413 of LNCS., Springer (2014) 357-372
- 9. Rosu, G., Havelund, K.: Synthesizing dynamic programming algorithms from linear temporal logic formulae. Technical report, Research Institute for Advanced Computer Science (RIACS) (2001)
- 10. Tan, L., Kim, J., Sokolsky, O., Lee, I.: Model-based testing and monitoring for hybrid embedded systems. In: Proceedings of the 2004 IEEE International Conference on Information Reuse and Integration. (2004) 487-492
- 11. Thati, P., Rosu, G.: Monitoring algorithms for metric temporal logic specifications. In: Runtime Verification. Volume 113 of ENTCS., Elsevier (2005) 145-162
- 12. Basin, D.A., Klaedtke, F., Zalinescu, E.: Algorithms for monitoring real-time properties. In: Runtime Verification. Volume 7186 of LNCS., Springer (2011) 260-275
- 13. Geilen, M.: On the construction of monitors for temporal logic properties. In: Proceedings of the 1st Workshop on Runtime Verification. Volume 55 of ENTCS. (2001) 181-199
- 14. Maler, O., Nickovic, D., Pnueli, A.: From MITL to Timed Automata. In: Proceedings of FORMATS. Volume 4202 of LNCS., Springer (2006) 274-289
- 15. Pnueli, A.: The temporal logic of programs. In: Proceedings of the 18th IEEE Symposium Foundations of Computer Science. (1977) 46-57
- 16. Koymans, R.: Specifying real-time properties with metric temporal logic. Real-Time Systems 2 (1990) 255-299
- 17. Fainekos, G., Pappas, G.J.: Robustness of temporal logic specifications. In: Formal Approaches to Testing and Runtime Verification. Volume 4262 of LNCS., Springer (2006) 178192
- 18. Fainekos, G., Pappas, G.J.: Robustness of temporal logic specifications for continuous-time signals. Theor. Comput. Sci. 410 (2009) 4262-4291

- 19. Donze, A., Ferrre, T., Maler, O.: E GLYPH&lt;14&gt; cient robust monitoring for stl. In: Proceedings of the 25th International Conference on Computer Aided Verification. CAV, Berlin, Heidelberg, Springer-Verlag (2013) 264-279
- 20. Garcia, C.E., Prett, D.M., Morari, M.: Model predictive control: Theory and practice - a survey. Automatica 25 (1989) 335348
- 21. Abbas, H., Fainekos, G.E., Sankaranarayanan, S., Ivancic, F., Gupta, A.: Probabilistic temporal logic falsification of cyber-physical systems. ACM Trans. Embedded Comput. Syst. 12 (2013) 95
- 22. Jin, X., Donze, A., Deshmukh, J., Seshia, S.: Mining requirements from closed-loop control models. In: Hybrid Systems: Computation and Control, ACM Press (2013)
- 23. Seda, A.K., Hitzler, P.: Generalized distance functions in the theory of computation. The Computer Journal 53 (2008) bxm108443-464
- 24. Eklund, J.M., Sprinkle, J., Sastry, S.: Implementing and testing a nonlinear model predictive tracking controller for aerial pursuit evasion games on a fixed wing aircraft. / In: American Control Conference. (2005)
- 25. Bakirtzis, A., Petridis, V ., Kiartzis, S., Alexiadis, M., Maissis, A.: A neural network short term load forecasting model for the greek power system. IEEE Transactions on Power Systems 11 (1996) 858-863
- 26. Monteiro, C., Bessa, R., Miranda, V., Botterud, A., Wang, J., Conzelmann, G.: Wind power forecasting: State-of-the-art 2009. Technical Report ANL DIS-10-1, Argonne National Lab-/ oratory (2009)
- 27. Davey, B.A., Priestley, H.A.: Introduction to Lattices and Order (2. ed.). Cambridge University Press (2002)
- 28. Fainekos, G., Sankaranarayanan, S., Ueda, K., Yazarel, H.: Verification of automotive control applications using s-taliro. In: Proceedings of the American Control Conference. (2012)
- 29. Simuquest: Enginuity. http://www.simuquest.com/products/enginuity (2013) Accessed: 2013-10-14.
- 30. Annapureddy, Y.S.R., Liu, C., Fainekos, G.E., Sankaranarayanan, S.: S-taliro: A tool for temporal logic falsification for hybrid systems. In: Tools and algorithms for the construction and analysis of systems. Volume 6605 of LNCS., Springer (2011) 254-257

## Appendix: Proof of Section 4.2

We prove by induction the correctness of Algorithms 1 and 2. We need to prove that at each simulation step i , the returning value of the CR algorithm is the same as the robustness value. Without loss of generality, assume i GLYPH&lt;21&gt; Hst ; therefore, the values in the table columns GLYPH&lt;0&gt; Hst to 0 contain the robustness values based on the actual simulation. When i &lt; Hst then the proof is immediate by the semantics of temporal logic. We must show that, for each sub-formula ' k the value stored in column j of robustness table Tk j ; should be correctly computed according to the semantics

$$\left [ \varphi _ { k } \right ] & ( s, i + j ) = T _ { k, j } = C R ( \varphi _ { k }, j, s _ { i } ^ { \prime }, \mathfrak { d }, \mathcal { O } ) \\ \dots \dots \dots \ n \dots$$

given matrix T and vector Pre

## Base case:

We will show that for each MTL &lt; + 1 + pt sub-formula in the form of a predicate, the value which is returned by the CR algorithm (Algorithm 2) is equal to the semantics of the sub-formula. Assume the sub-formula is a predicate p = ' k , for each simulation time i + j , the corresponding robustness value is stored in the column j of robustness table as follows:

$$\forall j, - H s t \leq j \leq H r z, [ p ] ( s, i + j ) & = \text{Dist} _ { d } ( s ( i + j ), \mathcal { O } ( p ) ) = \text{Dist} _ { d } ( s _ { i + j }, \mathcal { O } ( p ) ) = \\ & \tau \quad \sim \infty \quad \cdot \, \varphi \ \lambda \ \wedge$$

$$T _ { k, j } = C R ( p, j, s _ { i } ^ { \prime }, \mathbf d, \mathcal { O } )$$

Therefore, for each predicate the algorithm 'CR' computes the correct robustness value.

## Induction Hypothesis:

For each temporal sub-formulas ' k , Hst GLYPH&lt;0&gt; hst ( ' k ) GLYPH&lt;21&gt; Hrz because of the fact that Hst = Hrz + hst ( ' ) GLYPH&lt;21&gt; Hrz + hst ( ' k ); therefore GLYPH&lt;0&gt; Hst + hst ( ' k ) GLYPH&lt;20&gt; GLYPH&lt;0&gt; Hrz .

As a result, the values at the columns from GLYPH&lt;0&gt; Hst up to GLYPH&lt;0&gt; Hst + hst ( ' k ) will only depend on the actual simulation values, i.e., the predicates from column GLYPH&lt;0&gt; Hst up to column 0 which will not change in next simulation steps. These values are shown in gray color cells of Table 5. As a result, all the table entries from GLYPH&lt;0&gt; Hst up to GLYPH&lt;0&gt; Hst + hst ( ' k ) will not change (in next run) and the re-computation is not needed. Therefore, we shift all the values of predicates one column to the left and we ignore columns GLYPH&lt;0&gt; Hst to GLYPH&lt;0&gt; Hst + hst ( ' k ) GLYPH&lt;0&gt; 1 in our current run of Algorithm1 (Lines 13 and 17). Therefore, it is not necessary to include the columns GLYPH&lt;0&gt; Hst to GLYPH&lt;0&gt; Hst + hst ( ' k ) GLYPH&lt;0&gt; 1 in proof and Induction Hypothesis.

For Induction Hypothesis, we assume that the value stored in the robustness table is the semantically correct robustness value for each sub-formula ' k :

$$\forall j, - H s t + h s t ( \varphi _ { k } ) \leq j \leq H r z, \left [ \varphi _ { k } \right ] ( s, i + j ) = T _ { k, j } = C R ( \varphi _ { k }, j, s _ { i } ^ { \prime }, \mathbf d, \mathcal { O } ) \\ \dots \colon c \colon \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots \ dots \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots \dots$$

And if there exists unbounded past operator sub-formula like ' k = S 0 [ l ; + 1 ) ' , we assume the Pre k ( ) = J S 0 [ l ; + 1 ) ' K ( s ; i GLYPH&lt;0&gt; 1 GLYPH&lt;0&gt; Hst + hst ( ' k ))) because it belongs to the previous run of i GLYPH&lt;0&gt; 1, i.e we store the value Tk ; ( GLYPH&lt;0&gt; Hst + hst ( ' k )) in Pre k ( ) before processing the current run ( ) (see Algorithm 1 line 2). i

## Induction Step:

## GLYPH&lt;15&gt; Negation:

8 j ; GLYPH&lt;0&gt; Hst + hst ( ' k ) GLYPH&lt;20&gt; j GLYPH&lt;20&gt; Hrz : J ' k K ( s ; i + j ) = J : ' m K ( s ; i + j ) = GLYPH&lt;0&gt; J ' m K ( s ; i + j ) = GLYPH&lt;0&gt; Tm j ; = CR ( : ' ; m j ; s 0 i ; d ; O )

## GLYPH&lt;15&gt;

- Disjunction:

8 j ; GLYPH&lt;0&gt; Hst + hst ( ' k ) GLYPH&lt;20&gt; j GLYPH&lt;20&gt; Hrz : J ' k K ( s ; i + j ) = J ' m \_ ' n K ( s ; i + j ) = J ' m K ( s ; i + j ) t J ' n K ( s ; i + j ) = Tm j ; t Tn j ; = CR ( ' m \_ ' ; n j ; s 0 i ; d ; O )

## GLYPH&lt;15&gt; Until:

For sub-formulas of the form ' k = ' m U [ l u ; ] ' n , either the corresponding robustness values are correctly saved in robustness matrix for ' ; ' m n or the semantics will satisfy the correctness if the corresponding values belong to columns beyond the Hrz :

$$\begin{array} { l } \ u r \leq. \\ \forall j, - H s t + h s t ( \varphi _ { k } ) \leq j \leq H r z \, \colon \, \left [ \varphi _ { k } \right ] = \left [ \varphi _ { m } \mathcal { U } _ { [ l, u ] } \varphi _ { n } \right ] ( s, i + j ) = \\ \bigsqcup _ { h = i + j + l } ^ { i + j + u } ( \left [ \varphi _ { n } \right ] ) ( s, h ) \, \sqcap \, \prod _ { r = i + j } ^ { h - 1 } \left [ \varphi _ { m } \right ] ( s, r ) ) = \\ \bigsqcup _ { h \in [ j + l, j + u ] \cap [ - H s t, H r z ] } ( T _ { n, h } \, \prod _ { r = j } ^ { h - 1 } T _ { m, r } ) = C R ( \varphi _ { m } \mathcal { U } _ { [ l, u ] } \varphi _ { n }, j, s ^ { \prime } _ { i }, \mathfrak { d }, \mathcal { O } ) \end{array}$$

$$\bigsqcup _ { h \in [ j + l, j + u ] \cap [ - H s t, H r z ] } ^ { \cdot } ( T _ { n, h } \sqcap \prod _ { r = j } ^ { \cdot } T _ { m, r } ) = C R ( \varphi _ { m } \mathcal { U } _ { [ l, u ] } \varphi _ { n }, j, s _ { i } ^ { \prime }, \mathfrak { d }, \mathcal { O } )$$

## GLYPH&lt;15&gt; Bounded Since:

For bounded sub-formula ' k = ' m S [ l u ; ] ' n , the robustness is defined as follows:

J ' k K ( s ; i + j ) = J ' m S [ l u ; ] ' n K ( s ; i + j ) = G i + j GLYPH&lt;0&gt; l h = + i j GLYPH&lt;0&gt; u ( J ' n K ( s ; h ) u l i + j r = + h 1 J ' m K ( s ; r )) Based on IH we know that j GLYPH&lt;21&gt; GLYPH&lt;0&gt; Hst + hst ( ' k ). We must show that the values of Tn p ; for j GLYPH&lt;0&gt; u GLYPH&lt;20&gt; p GLYPH&lt;20&gt; j GLYPH&lt;0&gt; l satisfy Tn p ; = J ' n K ( s ; i + p ) i.e. GLYPH&lt;0&gt; Hst + hst ( ' n ) GLYPH&lt;20&gt; j GLYPH&lt;0&gt; u and also we need to show that the values of Tmq ; for j GLYPH&lt;0&gt; u + 1 GLYPH&lt;20&gt; q GLYPH&lt;20&gt; j satisfy Tmq ; = J ' m K ( s ; i + q ) i.e. GLYPH&lt;0&gt; Hst + hst ( ' m ) GLYPH&lt;20&gt; j GLYPH&lt;0&gt; u + 1.

We have two cases for hst ( ' k ):

Case 1: hst ( ' k ) = hst ( ' n ) + u = max hst f ( ' n ) + u hst ; ( ' m ) + u GLYPH&lt;0&gt; 1 g According to IH, j GLYPH&lt;21&gt; GLYPH&lt;0&gt; Hst + hst ( ' k ), then j GLYPH&lt;21&gt; GLYPH&lt;0&gt; Hst + hst ( ' n ) + u . Thus j GLYPH&lt;0&gt; u GLYPH&lt;21&gt; GLYPH&lt;0&gt; Hst + hst ( ' n ) which satisfies the fact that Tn p ; = J ' n K ( s ; i + p ) for j GLYPH&lt;0&gt; u GLYPH&lt;20&gt; p GLYPH&lt;20&gt; j GLYPH&lt;0&gt; l . On the other hand, in this case: hst ( ' n ) + u GLYPH&lt;21&gt; hst ( ' m ) + u GLYPH&lt;0&gt; 1 1. )

According to IH, j + Hst GLYPH&lt;21&gt; hst ( ' k ) GLYPH&lt;21&gt; hst ( ' m ) + u GLYPH&lt;0&gt; 1, i.e., j + Hst GLYPH&lt;21&gt; hst ( ' m ) + u GLYPH&lt;0&gt; Thus j GLYPH&lt;0&gt; u + 1 GLYPH&lt;21&gt; GLYPH&lt;0&gt; Hst + hst ( ' m ), which satisfies the fact that Tmq ; = J ' m K ( s ; i + q for j GLYPH&lt;0&gt; u + 1 GLYPH&lt;20&gt; q GLYPH&lt;20&gt; j .

Table 5. Robustness Table (Unchangeable values in next runs are in gray color)

| column ( j ) )          | GLYPH<0> Hst   | ...   | GLYPH<0> Hst + hst ( ' k )   | ...   | GLYPH<0> Hrz = GLYPH<0> Hst + hst ( ' ) ...   | GLYPH<0> 1   |            | 0   | 1     | ...   | Hrz     |
|-------------------------|----------------|-------|------------------------------|-------|-----------------------------------------------|--------------|------------|-----|-------|-------|---------|
| index ( time ) )        | i GLYPH<0> Hst | ...   | i GLYPH<0> Hst + hst ( ' k ) | ...   | i GLYPH<0> Hrz                                | ... i        | GLYPH<0> 1 | i   | i + 1 | ...   | i + Hrz |
| Pre[1]                  |                |       |                              |       |                                               |              |            |     |       |       |         |
| Pre[...]                |                |       |                              |       |                                               |              |            |     |       |       |         |
| Pre[k]                  |                |       |                              |       |                                               |              |            |     |       |       |         |
| Pre[...]                |                |       |                              |       |                                               |              |            |     |       |       |         |
| Pre[ j ' j ](predicate) |                |       |                              |       |                                               |              |            |     |       |       |         |

Case 2: hst ( ' k ) = hst ( ' m ) + u GLYPH&lt;0&gt; 1 = max hst f ( ' n ) + u hst ; ( ' m ) + u GLYPH&lt;0&gt; 1 g According to IH, j GLYPH&lt;21&gt; GLYPH&lt;0&gt; Hst + hst ( ' k ) then j GLYPH&lt;21&gt; GLYPH&lt;0&gt; Hst + hst ( ' m ) + u GLYPH&lt;0&gt; 1. Thus j GLYPH&lt;0&gt; u + 1 GLYPH&lt;21&gt; GLYPH&lt;0&gt; Hst + hst ( ' m ) which satisfies the fact that Tmq ; = J ' m K ( s ; i + q ) for j GLYPH&lt;0&gt; u + 1 GLYPH&lt;20&gt; q GLYPH&lt;20&gt; j . On the other hand, in this case: hst ( ' m ) + u GLYPH&lt;0&gt; 1 GLYPH&lt;21&gt; hst ( ' n ) + u . According to IH, j + Hst GLYPH&lt;21&gt; hst ( ' k ) GLYPH&lt;21&gt; hst ( ' n ) + u i.e j + Hst GLYPH&lt;21&gt; hst ( ' n ) + u . Thus j GLYPH&lt;0&gt; u GLYPH&lt;21&gt; GLYPH&lt;0&gt; Hst + hst ( ' n ) which satisfies the fact that Tn p ; = J ' n K ( s ; i + p ) for j GLYPH&lt;0&gt; u GLYPH&lt;20&gt; p GLYPH&lt;20&gt; j GLYPH&lt;0&gt; l .

## As a result:

$$\begin{array} { l } \text{As a resu} \colon \\ \forall j, - H s t + h s t ( \varphi _ { k } ) \leq j \leq H r z \, \colon \, \left [ \varphi _ { k } \right ] \right ) ( s, i + j ) = \left [ \varphi _ { m } \mathcal { S } _ { [ l, u ] } \varphi _ { n } \right ] \left ( s, i + j \right ) = \\ \bigsqcup _ { h = i + j - u } ^ { i + j - l } ( \left [ \varphi _ { n } \right ] \right ] ( s, h ) \sqcap \prod _ { r = h + 1 } ^ { i + j } \left [ \varphi _ { m } \right ] \left ( s, r \right ) \right ) = \\ \bigsqcup _ { h = j - u } ^ { j - l } ( T _ { n, h } \sqcap \prod _ { r = h + 1 } ^ { j } T _ { m, r } ) = C R ( \varphi _ { m } \mathcal { S } _ { [ l, u ] } \varphi _ { n }, j, s _ { i } ^ { \prime }, \mathfrak { d }, \mathcal { O } ) \end{array}$$

## GLYPH&lt;15&gt; Unbounded Since:

For unbounded sub-formula ' k = ' m S [ l ; + 1 ) ' n , according to Induction Hypothesis:

$$P r e ( k ) = \left [ \varphi _ { m } \mathcal { S } _ { [ l, + \infty ) } \varphi _ { n } \right ] ( s, i - 1 - H s t + h s t ( \varphi _ { k } ) )$$

In dynamic programming we recursively update the value J ' m S [ l ; + 1 ) ' n K ( s ; i GLYPH&lt;0&gt; Hst + hst ( ' k ) + x ) given the previous robustness value in the table J ' m S [ l ; + 1 ) ' n K ( s ; i GLYPH&lt;0&gt; Hst + hst ( ' k ) + x GLYPH&lt;0&gt; 1)

(where x = 0 when we use the Pre k ( ))

According to Def. 3 the robustness semantics at time i + j :

$$\left [ \varphi _ { m } \mathcal { S } _ { [ l, + \infty ) } \varphi _ { n } \right ] ( s, i + j ) = \bigsqcup \int _ { h = 0 } ^ { i + j - l } \left ( \left [ \varphi _ { n } \right ] ( s, h ) \sqcap \prod \int _ { r = h + 1 } ^ { i + j } \left [ \varphi _ { m } \right ] ( s, r ) \right ) \\ \text{and robustness for previous time $i+i-1$} \colon$$

and robustness for previous time i + j GLYPH&lt;0&gt; 1:

$$& \left [ \varphi _ { m } \mathcal { S } _ { [ l, + \infty ) } \varphi _ { n } \right ] \left ( s, i + j - 1 \right ) = \bigsqcup _ { h = 0 } ^ { i + j - l ^ { - 1 } } \left ( \left [ \varphi _ { n } \right ] \right ] ( s, h ) \sqcap \prod _ { r = h + 1 } ^ { i + j - 1 } \left [ \varphi _ { m } \right ] \left ( s, r \right ) \right ) \\ & \text{We can define robustness value at time $i+j$ given the value at time $i+j-1$} \colon$$

We can define robustness value at time i + j given the value at time i + j GLYPH&lt;0&gt; 1:

$$& \text{We can define robustness value at time } i + j \, \text{given the value at time } i + j - 1 \colon \\ & \left [ \varphi _ { m } S _ { ( l, + \infty ) } \varphi _ { n } \right ] \right ] ( s, i + j ) = \bigsqcup _ { h = 0 } ^ { i + j - l } \left ( \left [ \varphi _ { n } \right ] ( s, h ) \, \Box \, \prod _ { r = h + 1 } ^ { i + j } \left [ \varphi _ { m } \right ] ( s, r ) \right ) = \\ & = \left ( \bigsqcup _ { l } ^ { i + j - l - 1 } \left ( \left [ \varphi _ { n } \right ] ( s, h ) \, \Box \, \prod _ { r = h + 1 } ^ { i + j - 1 } \left [ \varphi _ { m } \right ] ( s, r ) \right ) \, \Box \, \left [ \varphi _ { m } \right ] \right ] ( s, i + j ) \right ) \, \bigsqcup _ { l } \left [ \varphi _ { m } \right ] \right ] ( s, i + j ) \right ) \, \bigsqcup _ { l } \left ( \left [ \varphi _ { n } \right ] \right ] ( s, i + j - l ) \, \Box \, \prod _ { r = i + j - l + 1 } ^ { i + j } \left [ \varphi _ { m } \right ] ( s, r ) \right ) \\ & \text{Based on IH, we know that } j \, \geq \, - H s t + h s t ( \varphi _ { k } ). \, \text{We must show that } the \, \text{va} \, \\ & \sim \, \tau \, \tau \, \quad - \, \Pi _ { k } \, \cdots \, \colon \, \colon \, \colon \, \colon \, \colon \, \colon \, \colon \, \colon \, \colon \, \colon \, \colon \, \colon \, \colon \, \colon \, \colon \, \colon \, \colon \, \colon \, \colon \, \colon \, \colon \, \colon \, \colon \, \colon \, \colon \, \colon \, \colon \, \colon \, \colon \, \colon \, \colon \, \colon \, \colon \, \colon \, \colon \, \colon \, \colon \, \colon \, \colon \, \colon \, \colots \, \colon \, \colon \, \colon \, \colon \, \colon \, \colon \, \colon \, \colon \, \colon \, \colon \, \colon \, \colon \, \colon \, \colon \, \colon \, \colon \, \colon \, \colon \, \colon \, \colon \, \colon \, \colon \, \colon \, \colon \, \colon \, \colon \, \colon \, \colon \, \colon \, \colon \, \colon \, \colon \, \colon \, \colon \, \colon \, \colon \, \colon \, \colon \, \colon \, \text{$\alpha$} \, $\alpha$} \, $\alpha$} \, $ \alpha$}$$

Based on IH, we know that j GLYPH&lt;21&gt; GLYPH&lt;0&gt; Hst + hst ( ' k ). We must show that the value of Tn j ; GLYPH&lt;0&gt; l = J ' n K ( s ; i + j GLYPH&lt;0&gt; l ), i.e., GLYPH&lt;0&gt; Hst + hst ( ' n ) GLYPH&lt;20&gt; j GLYPH&lt;0&gt; l and also the values of Tmq ; for j GLYPH&lt;0&gt; l + 1 GLYPH&lt;20&gt; q GLYPH&lt;20&gt; j satisfy Tmq ; = J ' m K ( s ; i + q ), i.e., GLYPH&lt;0&gt; Hst + hst ( ' m ) GLYPH&lt;20&gt; j GLYPH&lt;0&gt; l + 1.

We have two cases for hst ( ' k ):

Case 1: hst ( ' k ) = hst ( ' n ) + l = max hst f ( ' n ) + l ; hst ( ' m ) + l GLYPH&lt;0&gt; 1 g According to IH, j GLYPH&lt;21&gt; GLYPH&lt;0&gt; Hst + hst ( ' k ); therefore, j GLYPH&lt;21&gt; GLYPH&lt;0&gt; Hst + hst ( ' n ) + l and j GLYPH&lt;0&gt; l GLYPH&lt;21&gt; GLYPH&lt;0&gt; Hst + hst ( ' n ) which satisfies Tn j ; GLYPH&lt;0&gt; l = J ' n K ( s ; i + j GLYPH&lt;0&gt; l ). On the other hand in this case: hst ( ' n ) + l GLYPH&lt;21&gt; hst ( ' m ) + l GLYPH&lt;0&gt; 1.

According to IH, j + Hst GLYPH&lt;21&gt; hst ( ' k ) GLYPH&lt;21&gt; hst ( ' m ) + l GLYPH&lt;0&gt; 1, i.e., j + Hst GLYPH&lt;21&gt; hst ( ' m ) + l GLYPH&lt;0&gt; 1. Thus j GLYPH&lt;0&gt; l + 1 GLYPH&lt;21&gt; GLYPH&lt;0&gt; Hst + hst ( ' m ) which satisfies the fact that Tmq ; = J ' m K ( s ; i + q ) for j GLYPH&lt;0&gt; l + 1 GLYPH&lt;20&gt; q GLYPH&lt;20&gt; j .

Case 2: hst ( ' k ) = hst ( ' m ) + l GLYPH&lt;0&gt; 1 = max hst f ( ' n ) + l ; hst ( ' m ) + l GLYPH&lt;0&gt; 1 g According to IH, j GLYPH&lt;21&gt; GLYPH&lt;0&gt; Hst + hst ( ' k ); therefore, j GLYPH&lt;21&gt; GLYPH&lt;0&gt; Hst + hst ( ' m ) + l GLYPH&lt;0&gt; 1 where j GLYPH&lt;0&gt; l + 1 GLYPH&lt;21&gt; GLYPH&lt;0&gt; Hst + hst ( ' m ) which satisfies the fact that Tmq ; = J ' m K ( s ; i + q ) for j GLYPH&lt;0&gt; l + 1 GLYPH&lt;20&gt; q GLYPH&lt;20&gt; j . On the other hand in this case: hst ( ' m ) + l GLYPH&lt;0&gt; 1 GLYPH&lt;21&gt; hst ( ' n ) + l . According to IH, j + Hst GLYPH&lt;21&gt; hst ( ' k ) GLYPH&lt;21&gt; hst ( ' n ) + l i.e. j + Hst GLYPH&lt;21&gt; hst ( ' n ) + l . thus j GLYPH&lt;0&gt; l GLYPH&lt;21&gt; GLYPH&lt;0&gt; Hst + hst ( ' n ) which satisfies Tn j ; GLYPH&lt;0&gt; l = J ' n K ( s ; i + j GLYPH&lt;0&gt; l )

## As a result:

8 j ; GLYPH&lt;0&gt; Hst + hst ( ' k ) GLYPH&lt;20&gt; j GLYPH&lt;20&gt; Hrz : J ' k K ( s ; i + j ) = J ' m S [ l ; + 1 ) ' n K ( s ; i + j ) = = GLYPH&lt;18&gt; J ' m S [ l ; + 1 ) ' n K ( s ; i + j GLYPH&lt;0&gt; 1) u J ' m K ( s ; i + j ) GLYPH&lt;19&gt; F

$$\begin{pmatrix} \nwarrow \\ \left ( \left [ \varphi _ { n } \right ] \right ) ( s, i + j - l ) \sqcap \prod _ { r = i + j - l + 1 } ^ { i + j } \left [ \varphi _ { m } \right ] ( s, r ) \right ) = \\ \cdot \, r \, \frac { r } { r } \, \frac { r } { r } \, \frac { r } { r } \, \cdot \, \cdot \, \cdot \, \cdot \, \cdot \, \cdot \, \cdot \, \cdot \, \cdot \, \cdot \, \cdot \, \cdot \, \cdot \, \cdot \, \cdot \, \cdot \, \end{pmatrix} ^ { \prime }$$

$$& = \left ( \begin{array} { c c } T _ { k, j - 1 } & \text{if $j>-Hs t+hst(\varphi_{k})$} \\ P r e [ k ] & \text{if $j=-Hs t+hst(\varphi_{k})$} \end{array} \right ) \sqcup \left ( T _ { m, j } \right ) \sqcup \left ( T _ { n, j - l } \sqcup \prod _ { r = j - l + 1 } ^ { j } T _ { m, r } \right ) =$$

GLYPH&lt;16&gt; tmp S GLYPH&lt;17&gt; F GLYPH&lt;16&gt; Tn j ; GLYPH&lt;0&gt; l u tmpmin GLYPH&lt;17&gt; = CR ( ' m S [ l ; + 1 ) ' ; n j ; s 0 i ; d ; O ).
Adel Dokhanchi Bardh Hoxha Georgios Fainekos
On-Line Monitoring for Temporal Logic Robustness
In this paper, we provide a Dynamic Programming algorithm for on-line
monitoring of the state robustness of Metric Temporal Logic specifications with
past time operators. We compute the robustness of MTL with unbounded past and
bounded future temporal operators MTL over sampled traces of Cyber-Physical
Systems. We implemented our tool in Matlab as a Simulink block that can be used
in any Simulink model. We experimentally demonstrate that the overhead of the
MTL robustness monitoring is acceptable for certain classes of practical
specifications.