{'fraction_non_alphanumeric': 0.038584529189460606, 'fraction_numerical': 0.00697692856576548, 'mean_word_length': 4.322081575246132, 'pattern_counts': {'":': 0, '<': 1, '<?xml version=': 0, '>': 9, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 10, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Technical Report: Property-Directed Verified Monitoring of Signal Temporal Logic

Signal Temporal Logic monitoring over numerical simulation traces has emerged as an effective approach to approximate verification of continuous and hybrid systems. In this report we explore an exact verification procedure for STL properties based on monitoring verified traces in the form of Taylor model flowpipes as produced by the Flow* verified integrator. We explore how tight integration with Flow*'s symbolic flowpipe representation can lead to more precise and more efficient monitoring. We then show how the performance of monitoring can be increased substantially by introducing masks, a property-directed refinement of our method which restricts flowpipe monitoring to the time regions relevant to the overall truth of a complex proposition. Finally, we apply our implementation of these methods to verifying properties of a challenging continuous system, evaluating the impact of each aspect of our procedure on monitoring performance.


Introduction
Signal Temporal Logic (STL) [35] is an established and effective framework for describing and monitoring temporal properties of real-valued signals in continuous time, enabling verification of both continuous and hybrid systems. Much work on STL has focused on monitoring signals derived from numerical simulation traces. This is a powerful technique, but the approximate nature of such traces can lead to erroneous signal values at some timepoints whilst the signals do not account for uncertainties in the underlying model. Recently Ishii, Yonezaki, and Goldsztejn [27] have explored combining signal-based monitoring techniques with interval analysis to perform exact verification of STL properties over traces produced via verified integration.
In this report we propose a new verified STL monitoring algorithm based on preconditioned Taylor model flowpipes [34] generated with the Flow* verified integrator [13]. Our algorithm starts from such a Flow* flowpipe, which tracks our uncertain knowledge of the system state at each point in time (whether due to numerical errors or uncertain model parameters), and produces a three-valued signal reflecting our resulting uncertain knowledge in the truth value of a STL property over time. One of Flow*'s key features is its sophisticated symbolic flowpipe representation, which allows it to handle a wide range of non-linear continuous and hybrid systems [15], but poses challenges to effectively monitoring properties over these flowpipes, since overapproximating the value of the flowpipe at a given timepoint can be expensive and requires a careful tradeoff between accuracy and efficiency. We tackle these challenges by tightly integrating our monitoring strategy for atomic propositions with Flow*'s flowpipe representation, in contrast to most previous verified monitoring approaches which treat the flowpipe as a closed box by evaluating it as an interval function. This allows us to vary our evaluation strategy on demand at each timepoint, as required to verify a given atomic proposition. We are thus able to maximize precision for complex atomic propositions by utilizing Taylor model arithmetic to avoid the dependency problem [9], or fall back to simpler interval evaluation strategies when this suffices to determine the value of the signal at the current timepoint.
We further refine our method by introducing masks, a special type of signal representing the region of time for which each proposition of a STL formula is required by the overall monitoring process. We present methods for computing masks in a top-down manner, complementing the normal bottom-up signal monitoring process. We also see how to efficiently monitor each atomic proposition under a given mask. This allows us to handle the monitoring of each atomic proposition as a single-pass offline verification problem with a mask providing a condensed view of the regions of interest; we are hence able to utilize Taylor model methods to refine the signal in the most crucial time regions whilst avoiding unnecessary work elsewhere. Altogether, this gives a property-directed algorithm for efficient and precise STL monitoring over Flow* flowpipes.
The structure of this report is as follows. In Section 1.1 we review related work. Section 2 covers necessary background information regarding interval arithmetic, Taylor Models, Flow*, and STL, and establishes our notation. In Section 3 we introduce our verified monitoring algorithm by defining three-valued signals and our method of monitoring atomic propositions over Flow* flowpipes. In Section 4 we present masks and show how they may be used to perform property-directed monitoring. In Section 5 we evaluate the benefits of each part of our method for monitoring STL properties in a complex continuous system. Finally, in Section 6 we present our conclusions and discusses future directions.

Related Work
The most closely related work is the verified STL monitoring algorithm of Ishii et al. [25][26][27]. We build upon their approach of monitoring atomic propositions using interval root finding to derive verified signals; however, whilst their method treats the result of verified integration as a generic interval function, we work directly with the symbolic Taylor model flowpipes produced by Flow*. Our formulation of verified signals is also quite different, representing signals using three-valued logic rather than inner and outer interval approximations. Other works have looked at three-valued extensions of STL [5,32], but have not applied this in the context of exact, interval-based, formal verification of continuous systems. Three valued logic has also been applied to model checking LTL properties over discrete systems with partially known state spaces [11]. Fisman and Kugler [23] also investigated a more general semantics for Linear Temporal Logic (LTL) and STL over a number of different forms of incomplete traces.
A variety of different approaches have been explored for formal verification of temporal logics over hybrid and continuous systems. Early methods include [2] which initially focused on linear systems and the temporal logic TCTL. Piazza et al. [40] developed methods for temporal logic verification of semi-algebraic hybrid systems based on quantifier elimination. Bresolin [10] developed a method for encoding LTL properties of hybrid systems as hybrid automata reachability problems, extending the common automata theoretic approach [42] to temporal logic verification, allowing existing reachability tools to be applied to LTL model checking. However, applying this method to even relatively simple LTL properties can result in large hybrid automata which are beyond the abilities of current reachability analysis tools. Cimatti et al. [16] presented another approach to reducing LTL verification on hybrid systems to reachability analysis. The dynamic temporal logic dTL 2 [28] takes a rather different approach, including both hybrid systems and nested temporal modalities as part of the logic and providing an associated proof calculus.
A number of recent works have focused specifically on exact STL verification using ideas from reachability analysis. Roehm et al. [41] provided an approach to STL verification for hybrid automata based on checking (discrete) time sampled versions of STL formulae against reachsets produced by reachability analysis tools such as CORA [1]. Bae and Lee [4] introduced an approach to STL verification which translates properties into constraint problems which can be verified exactly using a SMT solver such as Z3 for linear systems [17] or the ε-complete decision procedure dReal for non-linear systems [24,30]. This work is the closest to providing an automated property-directed model checking procedure for STL. The constraint solving tools on which this work relies are very different from verified integration tools such as Flow*, and currently which approach performs better depends heavily on the system at hand [15,31]. These exact verificationbased methods also compete with approximate methods such as [3,5,19,22] which attempt to verify properties by sampling trajectories and may use quantiative measures of robust satisfaction [20,21] to give some assurance of robustness of results and to cover uncertain model parameters and initial conditions. Our method has some similarities with online monitoring in that in both cases we have partial knowledge of the underlying signal, and wish to avoid unnecessary (re)evaluation of signals for atomic propositions. Deshmukh et al. [18] introduced an interval quantitative semantics for STL in order to perform online monitoring over partial traces. In their method partiality of traces is used to record the fact that part of the trace has not yet been received at the time of monitoring whereas in our method it reflects uncertainty in the underlying system. Both [18] and the earlier incremental marking procedure [36,38] attempt to avoid evaluation of atomic propositions at timepoints unnecessary for the operators in which they occur similarly to masks, however, we statically calculate a mask for the timepoints of interest in a complete proposition, whilst online monitoring algorithms calculate (contiguous) time horizons for propositions each time they are revisited. Masks also play a quite different role to these optimizations, since masks are computed in a top-down manner to allow specific parts of the verified monitoring process to be avoided on a non-contiguous region throughout the time domain, whilst the role of these optimizations in online monitoring is to reduce memory usage by allowing time points outside of a proposition's time horizon to be forgotton or to allow early termination of simulations.

Background
In this section we review some background material including interval arithmetic and Taylor models, which will form the centre of our monitoring process.

Interval Arithmetic
We will work with interval arithmetic [37] over closed intervals and denote the lower and upper endpoint of interval I = l I , u I x ∈ R l I ≤ x ≤ u I by l I , u I ∈ R ∪ {−∞, ∞} respectively. Arithmetic operations can be computed using interval endpoints so that I + J x + y x ∈ I, y ∈ J = l I + l J , u I + u J and IJ and I − J are computed similarly. We can also define set operations on intervals so I ∩ J = max{l I , l J }, min{u I , u J } , and whilst the set-theoretic union I ∪ J is not necessarily an interval, we may over-approximate and use I ∪ J min{l I , l J }, max{u I , u J } in its place. Given a real-valued function f : I → R over interval domain I, an interval valued function F is an interval extension of f if f (x) ∈ F (X) for every point x and interval X such that x ∈ X. Assuming f is differentiable and we have an interval extension F of its derivative f , we may apply the Extended Interval Newton method, a generalisation of the Newton root finding method, which uses interval evaluation of F to produce guaranteed interval enclosures of all roots of f [27, 37, Chapter 8.1]; we denote the set of such intervals as roots(F, F , I).

Taylor Model Arithmetic
When used in verified numerical computation, interval arithmetic often leads to imprecise or inconclusive results due to the so called dependency problem in which the functional dependencies within an expression are ignored by an interval overapproximation, causing the approximation errors to be compounded throughout the computation. This motivates the use of symbolic methods such as Taylor models [9,33], which give a higher-order symbolic over-approximation of a function based on a Taylor series expansion and an interval remainder bound. Definition 1. Given a function f : D → R n with domain D ⊆ R m , a k th -order Taylor model for f is a pair (p, I) of an n-dimensional vector p of k th -order m-variable polynomials and an n-dimensional box I such that f (x) ∈ p(x) + I for all x ∈ D.
The precision of the approximation increases as the order of the Taylor model increases and the size of the remainder decreases. Given two Taylor models (p, I) and (q, J) enclosing functions f and g respectively, we can carry out various operations symbolically. Addition of Taylor models may be defined piecewise, so that if f has Taylor model (p f , I f ) and g has Taylor model (p g , I g ) (both of order k) then f + g has Taylor model Multiplication of Taylor models is similar except, in order to preserve the order of the Taylor model, we must truncate higher-order terms into the remainder interval. Hence we define a k th -order Taylor model for fg over domain D by where p E contains all terms from p f p g of order strictly greater than k. Other common operations including multiplication, division, and differentiation can be carried out with a suitable expansion of the remainder intervals [9].
Finally, we may define the symbolic composition (q, J) (p, I), by symbolically substituting each dimension of (p, I) into (q, J) in place of the corresponding variable. This gives a Taylor model which is guaranteed to enclose the composition g • f of the underlying functions [8].

Consider a continuous system described by an n-dimensional collection of ODEs
with initial conditions x(0) in some starting set S ⊆ R n and with f being, for example, Lipschitz continuous. Such a system has a unique solution x s for any given initial condition s ∈ S [29]. The aim of verified integration is to find an interval function F : [0, T ] → R n enclosing every solution x s for s ∈ S over a bounded time window [0, T ]. Flow* [13] uses verified integration based on Taylor models [9] to compute such an enclosure covering the whole set S, soundly accounting for the uncertainty in the initial point s as well as floating point rounding errors. Flow* represents the solution as a flowpipe consisting of a sequence of preconditioned Taylor models [34], that is, over each interval time , the solution is enclosed in a composition of two Taylor models pre . Whilst this representation is extremely powerful, allowing Flow* to handle nonlinear systems with complex continuous dynamics, it can be expensive to work with the generated flowpipes: each pair of preconditioned Taylor models must be composed symbolically (and then be placed into Horner form [12,39]) in order to carry out accurate interval evaluation. This step is a prerequisite for applying most forms of analysis to the flowpipe including reach-avoidance checking, plotting [13], and the verified monitoring algorithm [26].

Signal Temporal Logic
Signal Temporal Logic [35] specifies properties of continuous trajectories in dynamical systems such as Eq. (1). Propositions are defined according to the grammar, ϕ, ψ : where I is an interval and atomic propositions consist of inequalities ρ p > 0 defined by polynomials p over the system's variables.
The semantics for the connectives are defined by specifying when a system trajectory x satisfies a property ϕ at time t, written (x, t) |= ϕ. Then the semantics for atomic propositions is given by (x, t) |= p > 0 iff p(x(t)) > 0 and the normal boolean connectives are extended to each time point so that, for example, The problem of verified monitoring of a STL property ϕ at a time point t ∈ [0, T ] is to determine whether or not (x s , t) |= ϕ for every trajectory x s of a given system.

Three-Valued Monitoring over Flow* flowpipes
In this section we present our basic verified monitoring algorithm for Signal Temporal Logic. In Section 3.1 we introduce three-valued signals and specify rules to combine these to derive signals for complex propositions. We then develop an efficient algorithm for monitoring signals of atomic propositions based over Flow* flowpipes in Sections 3.2 and 3.3.

Three-Valued Signals
Our verified monitoring algorithm is based on three-valued signals: Definition 3. Given a proposition ϕ and a three-valued signal s, we say s is a signal for ϕ (over the trajectories of a given system) if at every time t, This definition allows a single proposition ϕ to be approximated by many different signals to differing degrees of precision. Indeed, the signal which is unknown everywhere is a valid (but uninformative) signal for every proposition.
For concrete computation we work with those three-valued signals s that can be represented by a finite set of nonempty disjoint intervals I j = [a j , b j ] and logical values s j ∈ {T, F}, with j ranging over some index set Γ . These values determine signal s on those intervals, with U assumed elsewhere, and we write s = (I j , s j ) j . For convenience we also admit some improper representations including empty intervals, values s j = U, and intervals with overlapping endpoints (but consistent logical values); these may all be rewritten as proper representations.
Given propositions ϕ and ψ with s = (I j , s j ) j a signal for ϕ and w = (I j , w j ) j a signal for ψ, we have the following constructions: ¬ϕ has a signal given by ¬s = (I j , ¬s j ) j ϕ ∧ ψ has a signal given by In the above we have assumed, without loss of generality, that s and w are represented using a common set of intervals I j ; this is always possible by taking a common refinement of the representations of s and w respectively.
In the case of boolean signals, the until signal s U J w is usually computed by subdividing s into disjoint unitary signals s j (that is, signals which are indicator functions s j (t) = χ Ij (t) = (T if t ∈ I j otherwise F) of pairwise disjoint intervals) [35]. For three-valued signals we will follow a similar approach, however we need an appropriate three-valued generalisation of unitary signals. To this end we define a connected signal. Definition 4. We say a three-valued signal s is connected if for every interval [a, b] we have that, under the ordering F U T.
Proof. First we note that an indicator signal χ J, I is clearly connected. Conversely, given a connected signal s, take t and (for simplicity we assume that the properties defining these intervals hold at their endpoints; the other cases result in open/half-open intervals and are analogous).
Then we see that s = χ J, I : for any t ∈ J, T ≥ s(t) ≥ min(s(j l ), s(j u )) = T by the connectedness of s, whilst for any t ∈ I, supposing s(t) = F and w.l.o.g. that t > j u , since s is connected, s([t u , t]) = {T, U} contrary to the maximality of j u , and finally, for any t ∈ I \ J, we first see by connectedness of s that s(t) ∈ {T, U}, and then if we suppose s(t) = T we get a contradiction, similarly to the previous case, leading us to conclude that s(t) = U.
We note that it is straightforward to compute a signal for ϕ U K ψ on connected signals.
Proposition 2. If s and w are respectively signals for ϕ and ψ, and s is connected then is a signal for ϕ U K ψ.
Proof. Suppose (s U K w)(t) = T. Then s(t) = T and for some t ∈ t+K, s(t ) = T and w(t ) = T. But then since s is connected, Then either s(t) = F in which case (x, t) |= ϕ U K ψ, or for all t ∈ t + K, s(t) = F or w(t) = F, in which case again (x, t) |= ϕ U K ψ.
We next decompose a three-valued signal into connected signals.
Proposition 3. Given a three-valued signal s and disjoint intervals I j such that s −1 ({T, U}) = j I j , we have a decomposition s = j k s j,k of s into the connected components: Proof. Give any time t, if s(t) = F then for any I j and any J ⊆ I j since t / ∈ s −1 ({T, F}) = j I j .
If s(t) = T, then we see that t ∈ J j,k ⊆ I j for some j, k. But then If s(t) = U then we have t ∈ I j for some unique j and so l m But then we note s j,0 (t) = χ ∅, Ij (t) = U and for m > 0, s j,m (t) = χ J j,k , Ij (t) = U, showing that the RHS is U also. We now use this decomposition to construct a signal for ϕ U K ψ: Proposition 4. If ϕ has a three-valued signal s = j k s j,k with connected components s j,k and ψ has a signal w, then ϕ U K ψ has a signal given by, Proof. If (s U K w)(t) = T then for some j, k, Hence s j,k (t) = T and for some t ∈ t + K, s j,k (t ) = T and w(t) = T. However, since s j,k is connected, we conclude s j, Then s(t) = F and for some t ∈ t + K, w(t) = F and for all t ∈ [t, t ], s(t) = F and w(t) = F. Then since s(t ) = F on the connected region [t, t ], there must hence be some l with [t, t ] ⊆ I m . But then, (picking some m given l), s lm ∧ F K (s lm ∧ s ψ ) (t) = F, and so completing the proof by contrapositive.

Signals for Atomic Propositions
We now turn our attention to generating a signal for an atomic proposition ρ p > 0 with defining polynomial p, based on a Flow* flowpipe.
We do this in a single pass algorithm which iterates over each time segment of the flowpipe and encloses all roots of p for the current timestep. For each timestep [t k , t k+1 ], Flow* provides two Taylor models, q pre whose composition encloses all trajectories of the system over the time step. The value of p over system trajectories is hence enclosed by the Taylor model G where t ∈ [t k , t k+1 ] and s ranges over the n-dimensional box [−1, 1] n [12,34]. Therefore, we have an interval extension of p over the time interval [t k , t k+1 ] given by the interval function H We may then determine a signal for ρ.
Proposition 5. Given atomic proposition ρ = p(x) > 0, the three-valued signal s (I j , s j ) j is a signal for ρ where I j are the interval components of and s j is T iff H which may be derived by Taylor model differentiation [9]), and are guaranteed to enclose the roots of p. Then ρ must have a consistent boolean value in between these roots, which we may sample by performing interval evaluation of H (k) p (see Fig. 2).

Efficient Monitoring of Composed Taylor Models
The method described in Section 3.2 relies on being able to efficiently compute the interval function H (k) p defined as a symbolic composition of Taylor models (Eq. (3)). This is potentially very expensive since the composition involves symbolic operations on high-order polynomials and a Flowpipe may consist of thousands of time steps, each requiring a separate composition.
However, since we only need to deduce the signal for the atomic proposition, rather than the exact function value at each point, it will often be sufficient to inexpensively over-approximate the range of Eq. (3) over the current time step via interval arithmetic, which we do by replacing some of the Taylor model compositions (denoted ) with functional compositions (denoted •). Hence, we use the following adaptive algorithm: -Perform the interval evaluation stepwise using interval arithmetic to check if 0 ∈ range p • q Hence, we are able to generate a precise signal for an atomic proposition over the whole time domain, whilst only performing symbolic Taylor model composition and root finding on demand where necessary to disambiguate the result of the signal (i.e. near the roots of the atomic proposition). We may additionally skip the composition of the preconditioned Taylor model on dimensions which do not correspond to any variable of p.
This method may, however, still spend effort trying to determine the truth value of the signal of an atomic proposition in regions of time which are not crucial to the truth of the overall signal; this issue is addressed in the next section with the introduction of masks.

Masks
In this section we introduce masks which allow us to direct the monitoring process to certain time-regions on the flowpipe. We then see how the mask required for each proposition may be constructed in a top-down manner, taking into account the context of an atomic proposition in the overall STL monitoring process (Sections 4.2 and 4.3). Once we have an appropriate mask, in Section 4.4 we see how to reduce the cost of monitoring an atomic proposition by avoiding work associated within time points outside of the mask.

Basic Notions
Firstly we introduce masks as follows: Definition 5. A mask is a finite sequence m = (I j ) j of disjoint intervals I j . We refer to these intervals as the regions of interest under the mask m.
We can interpret a mask m as a boolean signal m : Such a mask represents the region of time for which we wish to monitor a given proposition. Since for soundness of monitoring we only need to overapproximate these regions of interest, in a practical implementation we may restrict ourselves to masks whose components are all closed intervals I j [a j , b j ] (using e.g. floating point endpoints) and consistently round outwards. We will however sometimes use other types of interval endpoints in what follows in order to state crisp results.
We can apply a mask to an existing signal, erasing any truth values that lie outside the mask.
Examples of Masking Before laying out rules for using and computing masks, we will illustrate their use in two different examples, demonstrating the importance of the temporal and logical context of a proposition within a STL formula.
This means that in checking ϕ it is sufficient to compute a signal for ψ under the mask m ( [5,8]), allowing us to ignore more than half of the time-domain. then it is evident that computing a signal for ϕ only depends on the truth value of σ on the intervals [0, 2) and (4,5]. It thus suffices to compute a signal for σ under the mask m ([0, 2), (4,5]). This demonstrates how masks can enable a form of temporal short-circuiting.
Whilst in both of the above examples the required masks are quite simple, for general propositions they quickly become much more complex depending on what signals we have already computed for parts of the property (as in Example 3) or the position of the current proposition in a larger property. Later in this section we will see how the reasoning in these two examples can be generalised and combined to build up masks for arbitrary properties in a compositional manner.
Operations on Masks We next need to define the operations with which masks can be build. Firstly, masks inherit all of the normal logical operations on boolean signals [35]. In particular, given masks m I = (I k ) k and m J = (J l ) l we have that m I ∧ m J = (I k ∩ J l ) l,k , and we write the negation of a mask m as ¬m.
We will also need the temporal operators P J m (past) and H J m (historically) defined on masks by,

Monitoring Contexts
Before we specify how the masks for the monitoring algorithm should be computed, we must first formalise what is required of a mask for it to be used at a given stage of the monitoring algorithm. This motivates us to define contexts which capture our existing knowledge at each recursive step of the monitoring algorithm, by recording the position of an argument ψ within the STL operator currently being monitored and the signals s we have already computed for any other arguments.

Definition 8.
A monitoring context is defined similarly to a STL formula except with subformulae replaced by concrete signals s and, in exactly one place, a hole [·]. That is, a monitoring context is defined according to the grammar A monitoring context C([·]) is a monitoring context of the subformula ψ of a STL formula ϕ, if C([·]) has the same structure as ϕ except that, in the place of each atomic proposition ρ of ϕ, C([·]) has a signal s ρ that is a signal for ρ, and the hole [·] in place of ψ.
Given a signal s, we can evaluate a monitoring context C([·]) to give a signal C(s) by substituting s in the place of the hole [·] and following the usual rules for combining signals. This means that a monitoring context captures how the signal for the overall formula depends on the signal for the proposition which remains to be monitored.
We are now able to define when a mask is sufficient for monitoring in a context.

Definition 9.
A mask m is sufficient for a monitoring context C([·]) under mask n, if for any signal s we have that That is, a mask is sufficient if signals masked by it are just as good as unmasked signals for monitoring the overall formula.
We also wish to know when a mask is as small as possible for monitoring in a given context. It follows directly that the mask defined above is unique (for a given context and overall mask), allowing us to talk about the mask for a given context.

Monitoring Under a Mask: Complex Propositions
We are now ready to detail how our masked monitoring algorithm deals with complex propositions, by introducing suitable masks for each temporal and logical context. In each case we prove that these masks are sufficient (and optimal) for the relevant context, which collectively shows the correctness of masked monitoring.
Negation Suppose we want to monitor a negation ¬ϕ under mask m, then this is equivalent to monitoring ϕ under mask m and then negating the resulting signal. because the truth of ϕ at time t could determine the truth of either F [a,b] ϕ or G [a,b] ϕ at any point between a and b seconds ago (in the former case by witnessing its truth, and in the latter case, by witnessing its falsehood) -this generalises the reasoning given in Example 2.
Proposition 7. Given a context under the overall mask m, in each case the mask P [a,b] m is sufficient and optimal for C([·]).
Proof. Here we just prove sufficiency and optimality for C( Sufficiency For sufficiency we need to show that  Disjunctions and Conjunctions Suppose we want to monitor a disjunction ϕ ∨ ψ under mask m. We should first monitor ϕ under the mask m to give the signal s. Then, generalising Example 3, we can use the signal s to generate a mask m ∨ s , the or-mask of s. Definition 11. Given a three-valued signal s = (I j , s j ) j , the or-mask of s is the mask m ∨ s defined by m ∨ is the mask consisting of the two interval complements If this mask turns out to be empty (i.e. if s(t) = F = m ∨ s (t) for all x ∈ m), then we can stop and conclude s is a signal for ϕ ∨ ψ under m. Otherwise, we monitor ψ under the mask m ∨ s giving a signal w, and hence the signal s ∨ w for ϕ ∨ ψ under m.
We see that the mask m ∨ s is optimal and sufficient for the context C([·]) = s∨[·]. Proof.
Sufficiency Take any signal w and any time t whilst if s(t) ∈ {T, U}, then m ∧ s (t) = T and hence showing m ∧ s is sufficient.
Optimality Let m be any mask such that m < m ∧ s . Then there must be some time t 0 such that m (t 0 ) = F and m ∧ s (t 0 ) = T and hence s(t 0 ) ∈ {T, U}. But then if we pick the signal w(t) ≡ F, we see that hence m is not sufficient, proving that m ∧ s must be optimal.
We treat conjunctions similarly, and can see that the that and-mask m ∧ s defined by m ∧ s (t) = sj =F m j is an optimal and sufficient mask for conjunctions Until (ϕ U [a,b] ψ) Finally, suppose we wish to monitor the signal for the property ϕ U [a,b] ψ under the mask m. As in Section 3, we will compute the signal for ϕ U [a,b] ψ based on signals for ϕ and ψ using Eq. (2), however we now need to monitor ϕ and ψ under appropriate masks. We start by monitoring ϕ under the mask m ∨ P [a,b] m (taking into account the two places in which it appears in Eq. (2)). Then we could find a suitable mask for ψ by applying the above rules for ∨, ∧, and F [a,b] to Eq. (2). However, it turns out that this mask may be computed directly using the historically operator.
For this we first need the case of unitary masks, Proposition 9. Given an unitary mask m we have that Proof. Given in Appendix A (Proposition 9).
And we can see historically distributes over disjoint unitary masks.
Proof. Given in Appendix A (Proposition 10).
Together these give us the mask for the until operator. Proof. Given in Appendix A (Proposition 11).

Monitoring Under a Mask: Atomic Propositions
Once we have determined a mask m = (I j ) j for a given atomic proposition ρ given its context in the monitoring process, we then aim to directly monitor a signal s for ϕ under the mask m. This means that we only care about the value of s(t) at time points t for which m(t) is true, and so can increase the efficiency of monitoring by avoiding work associated with time points outside of the mask. Whilst there is no way to save Flow* from having to generate the flowpipes for these time points (since they may be required for determining the future evolution of the system), we can avoid the effort associated with every subsequent step of the monitoring process. We do this by modifying how we carry out monitoring of ρ (via H (k) p ) on each flowpipe segment (Section 3.3) over its associated time domain T k = [t k , t k+1 ] as follows:   if m ∧ (T k ) = ∅ then we set s(t) = U for all t ∈ T k and avoid monitoring over this segment; otherwise, we restrict the time domain to the interval T k = j T k ∩ I j and apply the normal monitoring process.
This immediately saves us from performing root finding on regions outside of the mask. Additionally, since we have already seen how the symbolic composition of the preconditioned Taylor model flowpipe and between the flowpipe and the atomic propositions may be performed on demand, these expensive operations may also be avoided outside of the mask. Thus masks allow us to direct the monitoring process for each atomic proposition based on its context within a wider STL formula.

Demonstration and Performance Analysis
We have implemented the monitoring techniques discussed in this report as a Python library with Cython [6] code implementing interval and Taylor model operations by interfacing with Flow*'s internal C++ libraries. In this section we will use this implementation to demonstrate the application of our method to verifying STL properties of a known challenging continuous system, the 9dimensional genetic oscillator [14,43] involving non-linear (polynomial) ODEs over the variables x 1 , . . . , x 9 and an uncertain box of interval initial conditions x i ∈ [a i , b i ] (given in full along with other details of our benchmarking approach in Appendix B). The evolution of the variables x 4 and x 6 over 5 seconds is shown in Fig. 3 which includes numerical traces from a sample of many different fixed initial conditions alongside a coarse interval over-approximation of a Flow* flowpipe covering the whole box of uncertain initial conditions. We can describe the temporal behaviour of this system much more precisely with STL properties such as ϕ G [0,1] P ∨ G [3,3.5] (Q) in which we have polynomial atomic propositions P x 6 − 1 > 0 and Q 0.032 − 125 2 (x 4 − 0.003) 2 − 3(x 6 − 0.5) 2 > 0. The property ϕ states that at any point within the first second, the system will either remain within the half-space P or, at any point between 3 and 3.5 seconds in the future will be within the elliptical region Q.
In Fig. 5 we break down the time taken to monitor ϕ for 0.5 seconds using a number of variants of our monitoring algorithm in order to evaluate the impact of each of its elements on monitoring cost and precision. First we consider the closed box monitoring approach where we first run Flow* to perform verified integration and flowpipe composition, before using interval analysis and functional composition to monitor ϕ over the entire flowpipe. Whilst the monitoring cost for the propositions P and Q is very small in comparison to the time it took Flow* to perform verified integration, the flowpipe composition stage is more expensive and takes almost as long as the verified integration itself. Next we monitor ϕ in the same way, but perform the flowpipe composition on demand as described in Section 3.3. We see that if we just monitor the simple atomic proposition P we save most of the cost of flowpipe composition, although once we also monitor Q we need to pay the full cost. These two methods also do not yield sufficient precision to verify ϕ, both producing a useless signal which is unknown everywhere. This imprecision can be seen in Fig. 4a which shows the result of monitoring the complex polynomial atomic proposition Q over the flowpipe using functional composition and the corresponding signal.
In order to produce a useful signal for ϕ we need to run our full monitoring algorithm, permitting symbolic composition at each stage. Whilst the monitoring cost for the simple proposition P is similar to before, the cost for the complex proposition Q is significantly higher. This, however, now gives a much more precise signal for Q as shown in Fig. 4b. This means we now get the overall signal s = (([0, 0.0237], T)) for ϕ, allowing us to verify that ϕ is true at time 0 and that P ∨ G [3,3.5] (Q) holds for at least the first 1.0237 seconds. Finally, we reran our monitoring algorithm but monitored each atomic proposition under appropriate masks. For example, Q is monitored under the mask shown in Fig. 4c. This produced the same overall signal as the full unmasked monitoring algorithm but reduced the monitoring time for Q by 65%.

Conclusion and Future Work
In this report we explored a symbolic algorithm for monitoring STL properties over Taylor model flowpipes via three-valued signals and introduced masking to direct the monitoring process to time regions critical to the property at hand. We saw that, whilst direct integration with the symbolic structure of flowpipes can add some overhead for complex propositions, it significantly increases the precision of the results generated and is sometimes necessary to produce definitive results at all. We have also seen that masking can have an important impact on reducing this cost, by avoiding the need to carry out symbolic operations for regions of time not necessary for the overall result of the monitoring algorithm. Our current method relies on interval analysis to evaluate flowpipes over the whole set of uncertain initial conditions, whereas Flow*'s flowpipes in fact track the functional dependency of each system variable on the initial condition [9]. In future we intend to use this additional information to extend our algorithm to produce spatio-temporal signals exploring refinements of the initial conditions and introduce spatio-temporal masks to enable spatio-temporal short-circuiting.