Alexey Bakhirkin

Thomas Ferrère

Dejan Nickovic

Oded Maler

Eugene Asarin

Online Timed Pattern Matching using Automata

We provide a procedure for detecting the sub-segments of an incrementally observed Boolean signal w that match a given temporal pattern ϕ. As a pattern specification language, we use timed regular expressions, a formalism well-suited for expressing properties of concurrent asynchronous behaviors embedded in metric time. We construct a timed automaton accepting the timed language denoted by ϕ and modify it slightly for the purpose of matching. We then apply zone-based reachability computation to this automaton while it reads w, and retrieve all the matching segments from the results. Since the procedure is automaton based, it can be applied to patterns specified by other formalisms such as timed temporal logics reducible to timed automata or directly encoded as timed automata. The procedure has been implemented and its performance on synthetic examples is demonstrated.

Introduction and Motivation

Complex cyber-physical systems and reactive systems in general exhibit temporal behaviors that can be viewed as dense-time signals or discrete-time sequences and time-series. The correctness and performance of such systems is based on properties satisfied by these behaviors. In formal verification, a system model is used to generate all possible behaviors and check for their inclusion in the language defined by the specifications. In runtime verification, interpreted as lightweight simulation-based verification, property satisfaction by individual system behaviors is checked. In many situations, we would like to monitor the ongoing behavior of a real system, already deployed and running, rather than traces of a simulation model during design time. In this context we want to detect property violation and other patterns of interest such as suspicious activities, degradation of performance and other alarming signs known to precede unpleasant or even catastrophic situations. The detection of such patterns and the reaction to them can be the basis of another level of supervisory control that reacts to situations as they occur without achieving the challenging and often impossible task of verifying offline against all possible scenarios. In fact, in the software engineering literature for safety-critical systems there is an actuatormonitor decomposition (safety bag) where one module computes the reaction while the other checks the results. Such an architecture has been proposed recently as a way to handle autonomous systems such as driver-free cars [START_REF] Koopman | Challenges in autonomous vehicle testing and validation[END_REF].

Properties traditionally used in verification often correspond to complete behaviors or their prefixes that start from time zero. In pattern matching one is interested in segments that may start and end in any time point. To be useful, the detection of patterns should be done online, as soon as they occur. In this paper we provide an automaton-based online pattern matching procedure where patterns are specified using timed regular expressions, a formalism suitable for describing patterns in concurrent and asynchronous behaviors. Before moving to our contribution, let us make a brief survey of some well-known classical results on string pattern matching. A regular expression ϕ defines a regular language L(ϕ) consisting of sequences that match it. It can be transformed into a non-deterministic automaton A ϕ that recognizes L(ϕ) in the sense that L(ϕ) is exactly the set of words w that admit a run from an initial to a final state. [START_REF] Mcnaughton | Regular expressions and state graphs for automata[END_REF] The existence for such an accepting run in A ϕ can be checked by exploring the finitely many such runs associated with w. As a byproduct of classifying w, the automaton can classify any prefix w[0..j] of w for j < k, just by observing the states reachable by the runs at time j. It is worth noting that the determinization procedure (subset construction) due to Rabin and Scott [START_REF] Rabin | Finite automata and their decision problems[END_REF] corresponds to a breadth-first exploration of these runs for all words, combined with the fact that runs that reach the same state can be merged (see Figure 3). A simple modification of A ϕ , to our knowledge first described in [START_REF] Thompson | Programming techniques: Regular expression search algorithm[END_REF], allows also to find all sub-segments w[i..j] of w that match ϕ. First, a counter t is used which increments each time a symbol is read -such a counter exists anyway in any implementation of a membership tester as a pointer to the current symbol in the sequence. Then a new initial state s is added to A ϕ , and in this state the automaton can self-loop indefinitely and postpone the selection of the point in time when it starts reading w. When it moves to the original initial state of A ϕ , it records the start time in an auxiliary variable t (see Figures 1 and2 for an example). Then whenever there is a run reaching an accepting state with t = r and t = r , one can conclude that w[r..r ] matches ϕ. This modification, also pointed to in [START_REF] Aho | The design and analysis of computer algorithms[END_REF], enabled the later implementation of fast and reliable string matching tools [START_REF] Aho | The AWK programming language[END_REF][START_REF] Pike | The text editor sam[END_REF] which are now standard. The application of regular expressions since extends beyond text processing but also occurs, e.g. in DNA analysis and programming languages.

To reason about the dynamic behaviors of complex systems, cyber-physical or not, one needs a language richer than traditional expressions [START_REF] Ulus | Pattern Matching with Time: Theory and Applications[END_REF]. To start with, the behaviors of such systems, unlike sequential text, are multi-dimensional by nature, involving several state variables and components working in parallel. In principle, it is possible to express patterns in the behavior of such systems using a global product alphabet, but such a flattening of the structure is impractical for both readability and complexity reasons. Instead we use a more symbolic variant of regular expressions (first used in the timed setting in [START_REF] Ulus | Timed pattern matching[END_REF], see also the proposal [START_REF] Havlicek | Realtime regular expressions for analog and mixed-signal assertions[END_REF] to add timing to the regular expressions of the industrial specification language PSL which admits variables) where one can refer to state variables and write expressions like p • q rather than (pq ∪ pq) • (pq ∪ pq). Needless to say, the whole practice of verification, starting with temporal logic specifications, via compositional system descriptions to their symbolic model-checking [START_REF] Clarke | Model checking[END_REF] is based on such an approach, which seems to be less developed in formal language theory. To reason about what happens in various parts of the system, we also employ intersection in our syntax. In the one-dimensional untimed case it does not increase the expressive power, but affects the complexity of online membership testing since the minimal DFA translating such expressions can be exponentially larger [START_REF] Gelade | Succinctness of regular expressions with interleaving, intersection and counting[END_REF]. The second observation is that system components need not be synchronized and they may operate on different time scales. Consequently, reasoning in discrete time with a pre-selected time step is wasteful and we use instead the timed regular expressions of [START_REF] Asarin | A Kleene theorem for timed automata[END_REF][START_REF] Asarin | Timed regular expressions[END_REF], a formalism tailored for specifying properties of timed behaviors such as Boolean signals [START_REF] Asarin | A Kleene theorem for timed automata[END_REF] or time-event sequences [START_REF] Asarin | Timed regular expressions[END_REF], where value changes and events can occur anywhere along the time axis. Thus the expression p ∩ (true • q • true) is matched by any segment of a Boolean signal where p holds continuously and a burst of q occurs anywhere inside this segment. Us-ing duration constraints we can refine the patterns, for example the expression p ∩ (true • q [a,∞] • true) considers only q-bursts that last for at least a time. The problem of timed pattern matching has been introduced and solved in [START_REF] Ulus | Timed pattern matching[END_REF]: find all the sub-segments of a multi-dimensional Boolean signal of a bounded variability that match a timed regular expression. This work was automaton-free and worked inductively on the structure of the formula in an offline manner. An online version of that procedure has been developed in [START_REF] Ulus | Online timed pattern matching using derivatives[END_REF] based on a novel extension of Brzozowski derivatives [START_REF] Brzozowski | Derivatives of regular expressions[END_REF] to timed regular expressions and dense time signals. Both works, which have been implemented in the tool Montre [START_REF] Ulus | Montre: A tool for monitoring timed regular expressions[END_REF] did not use the full syntax of timed regular expressions and hence did not match the expressive power of timed automata (see [START_REF] Herrmann | Renaming is necessary in timed regular expressions[END_REF]). In this paper we explore an alternative automaton-based procedure whose scope of application is wider than the expressions used in [START_REF] Ulus | Timed pattern matching[END_REF][START_REF] Ulus | Online timed pattern matching using derivatives[END_REF] as it works with any timed language definable by a timed automaton and is agnostic about the upstream pattern specification language. Let us mention another recent automaton-based approach is the one of [START_REF] Waga | A boyer-moore type algorithm for timed pattern matching[END_REF], a real-time extension of the Boyer-Moore pattern matching method. In contrast to our work, the procedure in [START_REF] Waga | A boyer-moore type algorithm for timed pattern matching[END_REF] works on TA defined over time-event sequences and it requires pre-computing the region graph from the TA specification. The same authors improve this result in [START_REF] Waga | Efficient online timed pattern matching by automata-based skipping[END_REF], by using a more efficient variant of the Boyer-Moore algorithm and by replacing the region automaton by the more efficient zone-simulation graph.

The essence of our contribution is the following. Starting with an expression ϕ, we build a non deterministic timed automaton A ϕ which accepts L(ϕ). Then by a small modification, similar to the discrete case, we convert it to a matching automaton A ϕ with two additional clocks x 0 and x s that record, respectively the time since the beginning of the signal (absolute time) and the time since we started reading it. Then, given a bounded variability Boolean signal we compute the reachability tree of the automaton whose nodes are pairs of the form (q, Z) where Z is a zone in the extended clock space of A ϕ . This tree captures all (possibly uncountably many) runs induced by w. By projecting zones associated with accepting states of the automaton on x 0 and x 0 -x s , we retrieve the matches. We combine this procedure with incremental observation of the input signal to obtain an online matching procedure. We implemented this procedure using the zone library of IF [START_REF] Bozga | IF: An intermediate representation and validation environment for timed asynchronous systems[END_REF].

Preliminaries

Signals Let B = {0, 1} and let P = {p 1 , . . . , p n } be a set of propositions. A state over P is an element of 2 P or equivalently a Boolean vector u ∈ B n assigning the truth value for any p ∈ P . The time domain T is taken to be the set of non-negative reals.

[t] = w[t] for all t < d, ww [t] = w [t -d] for all t ∈ [d, d + d ).
We consider signals of finite variability, which can be written as a finite concatenation of constant signals. The empty signal of duration zero is denoted . We use w w to denote the parallel composition of two signals of the same duration defined over disjoint sets of propositions. Timed Regular Expressions To specify sets of signals we use the timed regular expressions (TRE) of [START_REF] Asarin | A Kleene theorem for timed automata[END_REF], augmented with the use of a structured alphabet represented by a set P of atomic propositions [START_REF] Ulus | Timed pattern matching[END_REF]. The set of state constraints, denoted by Σ(P ) is simply the set of Boolean formulas over P . The syntax of TRE is given by the grammar

ϕ ::= | σ | ϕ ∪ ϕ | ϕ ∩ ϕ | ϕ • ϕ | ϕ + | ϕ I | ∃p.ϕ
where σ ∈ Σ(P ) and I ⊆ T is an integer-bounded interval. As customary, iterations of ϕ are denoted in exponent with ϕ 0 ≡ and

ϕ k ≡ ϕ k-1 • ϕ for k ≥ 1.
The Kleene star is defined as

ϕ * ≡ ∪ ϕ + .
Any TRE ϕ is associated with a set of signals, the timed language L(ϕ), via the following inductive definitions:

L( ) = { } L(ϕ 1 • ϕ 2 ) = {w 1 • w 2 | w i ∈ L(ϕ i ), i = 1, 2} L(σ) = {w | ∀t ∈ [0, |w|) w[t] |= σ} L(ϕ + ) = ∞ k=1 L(ϕ k ) L(ϕ 1 ∪ ϕ 2 ) = L(ϕ 1 ) ∪ L(ϕ 2 ) L( ϕ I ) = {w | w ∈ L(ϕ) ∧ |w| ∈ I} L(ϕ 1 ∩ ϕ 2 ) = L(ϕ 1 ) ∩ L(ϕ 2 ) L(∃p.ϕ) = {w | ∃w over {p}, w w ∈ L(ϕ)}
Note that signals in L(σ) need not be a constant, for example L(p i ) consists of all signals in which p i is constantly true but p j , for j = i may go up and down. Note also that the semantics of σ does not specify any duration, and in this sense it resembles σ * in classical regular expressions. The duration restriction is expressed using the ϕ I operation. The ∃p.ϕ operation corresponds to the renaming operation in [START_REF] Asarin | A Kleene theorem for timed automata[END_REF] which has been proven in [START_REF] Herrmann | Renaming is necessary in timed regular expressions[END_REF] to be necessary in order to match the expressive power of timed automata. Timed Automata We use a variant of timed automata, finite-state automata extended with real-valued clock variables, as acceptors of timed languages over signals. Unlike the automata introduced originally in [START_REF] Alur | A theory of timed automata[END_REF] and used in [START_REF] Asarin | Timed regular expressions[END_REF], which are event-based with alphabet symbols associated with transitions, we use a statebased approach [START_REF] Asarin | A Kleene theorem for timed automata[END_REF] where signal values are associated with time passage inside states. Let X = {x 1 , . . . , x m } be a set of clock variables. A clock constraint is a Boolean combination of inequalities of the form x c where c ∈ N is a constant, x ∈ X is a clock variable, and ∈ {<, ≤, =, ≥, >} is a comparison sign. The set of clock constraints over X is written Φ(X). A valuation v ∈ T m associates any x ∈ X with a delay denoted v(x) ∈ T.

Definition 1 (Timed Automaton). A timed automaton over signals is a tuple A = (P, X, L, S, i, o, ∆) with locations L, initial locations S ⊆ L, input labeling i : L → Σ(P ), output labeling o : L → Φ(X), and set of edges

∆ ⊆ L × Φ(X) × 2 X × L.
A state (configuration) of the automaton is a pair ( , v) where is a location and v is a clock valuation. The behavior of the automaton while reading a signal consists of an alternation of two types of steps:

-A time step ( , v)

w ( , v + r) where the automaton consumes a signal w of duration r while advancing all clocks in the same pace provided that the signal satisfies continuously the state invariant specified by the input label:

∀t ∈ [0, r) w[t] |= i( ); -A discrete step ( , v) δ -→ ( , v ) for some transition δ = ( , ϕ, R, ) ∈ ∆ such that v |= ϕ (clocks satisfy transition guard) and v = v[R ← 0] (clocks in R are reset while taking the transition).
A run of automaton A over a signal w is a sequence

( 0 , 0) w0 ( 0 , v 0 ) δ1 -→ ( 1 , v 1 ) w1 ( 1 , v 1 ) δ2 -→ . . . δn -→ ( n , v n ) wn ( n , v n )
of discrete and time steps such that w = w 1 w 2 . . . w n , starting with an initial configuration, that is, 0 ∈ S and v 0 (x) = 0 for all x ∈ X. A run is accepting if it ends in an accepting configuration:

v n |= o( n ).
The language L(A) is the set of signals admitting an accepting run.

The object that we are going to compute is the match set of a signal w with respect to a timed language L defined either by an automaton A or a timed regular expression: M(w, L) = {(t, t ) : w[t..t ] ∈ L}. In [START_REF] Ulus | Timed pattern matching[END_REF] it has been proved that for an expression ϕ, M(w, L(ϕ)) is a finite union of two-dimensional zones. Our results extend it to languages accepted by timed automata where (t, t ) belong to the match set if w[t..t ] admits an accepting run in A.

Translating TRE into Automata We now demonstrate, following [START_REF] Asarin | A Kleene theorem for timed automata[END_REF], how a timed regular expression translates into a timed automaton accepting the same language. The construction is rather straightforward and the reader is referred to [START_REF] Asarin | A Kleene theorem for timed automata[END_REF] for a more lengthy intuitive presentation. The construction of an automaton A ϕ = (P, X ϕ , L ϕ , S ϕ , i ϕ , o ϕ , ∆ ϕ ) accepting L(ϕ), is obtained by structural induction. In the description that follows we assume that automata given by induction hypothesis have disjoint sets of locations, but may share the same clocks except for the case of intersection.

-Empty word: A is defined by letting X = {x}, L = S = { }, i ( ) ≡ true, o ( ) ≡ (x = 0), and

∆ = ∅. -State expressions: A σ is defined by X σ = ∅, L σ = S σ = { }, i σ ( ) ≡ σ, o σ ( ) ≡ , and ∆ σ = ∅. -Union: A ϕ∪ψ is defined as the component-wise union of A ϕ and A ψ . -Intersection: A ϕ∩ψ is given by X ϕ∩ψ = X ϕ X ψ , L ϕ∩ψ = L ϕ × L ψ , S ϕ∩ψ = S ϕ × S ψ , with input labels i ϕ∩ψ ( , m) = i ϕ ( ) ∧ i ψ (m) for every ∈ L ϕ , m ∈ L ψ , similarly for output labels. For a pair of edges ( , β, Q, ) ∈ ∆ ϕ , (m, γ, R, m ) ∈ ∆ ψ , A ϕ∩ψ has the edges (( , m), β, Q, ( , m)), (( , m), γ, R, ( , m )), and (( , m), β ∧ γ, Q ∪ R, ( , m )). -Concatenation: we let X ϕ•ψ = X ϕ ∪ X ψ , L ϕ•ψ = L ϕ ∪ L ψ and S ϕ•ψ = S ϕ .
Labels are given by i ϕ•ψ ( )

≡ i ϕ ( ) if ∈ L ϕ , i ϕ•ψ ( ) ≡ i ψ ( ) otherwise; o ϕ•ψ ( ) ≡ false if ∈ L ϕ , o ϕ•ψ ( ) ≡ o ψ ( ) otherwise. Edges are given by ∆ ϕ•ψ = ∆ ϕ ∪ ∆ ψ ∪ {(f, o ϕ (f ), X ψ , s) | f ∈ L ϕ , s ∈ S ψ }. -Iteration: A ϕ + is obtained from A ϕ by adding edges (f, o ϕ (f ), X ϕ , s) for every pair f ∈ L ϕ and s ∈ S ϕ .
-Duration constraint: A ϕ I is obtained by using a fresh clock x / ∈ X ϕ and replacing output labels ϕ with ϕ ∧ (x ∈ I) in every location.

-Existential quantification: A ∃p.ϕ is obtained by replacing input labels σ with σ[p ← true] ∨ σ[p ← false] in every location.

The above procedure yields the following:

Theorem 1 (TRE ⇒ TA). For any TRE of containing m atomic expressions and n duration constraints, one can construct an equivalent timed automaton with n clocks and 2 m locations.

The exponential blow-up in the number of locations is solely due to the intersection operator, with repeated application of the product construction, and would otherwise vanish. For a proof of the other direction, TA ⇒ TRE, see [START_REF] Asarin | A Kleene theorem for timed automata[END_REF][START_REF] Asarin | Timed regular expressions[END_REF].

Membership and Matching using Timed Automata

In this section we present a zone-based algorithm for testing membership of a signal in the language accepted by a timed automaton; then show how it can be extended to find and extract the match set of the signal in that language.

Checking Acceptance by Non-Deterministic Timed Automata

The automata constructed from expressions, as well as other typical timed automata, are non-deterministic. Part of this non-determinism is dense, coming from modeling duration uncertainty using intervals, and also from different factorizations of a signal segment into two concatenated expressions. Unlike classical automata, it can be shown that some timed automata cannot be determinized [START_REF] Alur | A theory of timed automata[END_REF] and even determinizability of a given automaton is an undecidable problem [START_REF] Finkel | Undecidable problems about timed automata[END_REF]. However, these results are concerned with converting the non-deterministic TA into a deterministic one, equivalent with respect to all possible inputs which include signals of arbitrary variability and hence the number of clocks cannot be bounded. In contrast, exploring all the (uncountably many) possible runs of a non-deterministic timed automaton while reading a given signal of finite duration and variability is feasible, as has already been demonstrated [START_REF] Tripakis | Fault diagnosis for timed automata[END_REF][START_REF] Larsen | Online testing of real-time systems using uppaal[END_REF][START_REF] Krichen | Conformance testing for real-time systems[END_REF] in the context of testing, using what has been termed on-the-fly subset construction. The procedure described in the sequel shows how despite their dense nondeterminism, timed automata can be effectively used as membership testers for bounded-variability signals and eventually as online pattern matching devices.

To this end we use a variant of the standard zone-based reachability algorithm for simulating uncountably many runs in parallel. This algorithm underlies all timed automata verification tools [START_REF] Daws | The tool kronos[END_REF][START_REF] Behrmann | Uppaal 4.0[END_REF][START_REF] Bozga | IF: An intermediate representation and validation environment for timed asynchronous systems[END_REF], see [START_REF] Yovine | Model checking timed automata[END_REF][START_REF] Larsen | Uppaal in a nutshell[END_REF]. The procedure computes the simulation/reachability graph whose nodes are symbolic states of the form ( , Z) where is a location and Z is a zone in the space of clock valuations.

Definition 2 (Zone). Let X be a set of clock variables. A difference constraint is an inequality of the form x -y ≺ c for x, y ∈ X, c ∈ T, and ≺ ∈ {<, ≤}. A zone is a polytope definable as a conjunction of clock and difference constraints.

Zones are known to be closed under intersection, projection, resets and forward time projection defined as Z = {v + t | v ∈ Z ∧ t ≥ 0}. These operations are implemented as simple operations on the difference bound matrix (DBM) representing the zone.

Let A = (P, X, L, S, i, o, ∆) be a timed automaton and let A be the automaton obtained from A by adding an auxiliary clock x 0 which is never reset since the beginning and hence it keeps track of the absolute time. We will consider zones in the extended clock space, and denote extended clock valuations as (v 0 , v). It is not hard to see that a configuration ( , (v 0 , v)) is reachable in A iff the input prefix w[0..v 0 ] admits a run to ( , v) in A.

Definition 3 (Discrete Successor). Let Z be a zone and let δ = ( , ϕ, R, ) ∈ ∆ be a transition. The δ-successor of Z is the zone

Succ δ Z = {v : ∃v ∈ Z v |= ϕ ∧ v = v[R ← 0]}
While doing zone-based time passage in a zone, we need to restrict ourselves to segments of the signal that satisfy the input constraints of the location and this is made possible through the use of absolute time.

Definition 4 (Temporal Scope). The temporal scope of a signal w in location is the set of time points where w satisfies the input constraint of :

J ( , w) = {t : w[t] |= i( )}.
For a bounded variability signal, J ( , w) is a sequence J 1 , . . . , J k of disjoint intervals of the form

J i = [α i , β i ).
When a symbolic state ( , Z) is reached via a discrete transition, we need to split Z into zones on which time can progress, using the following operation.

E( , Z) = {Z ∧ α ≤ x 0 ≤ β | [α, β) ∈ J ( , w)}.
The procedure Succ (Algorithm 1) computes the successors of a symbolic state by one discrete transition and one time passage. The whole reachability algorithm (Algorithm 2) applies this procedure successively to all reachable symbolic states. It accepts as arguments the automaton A, the signal w, and the set I of states from which to start the exploration. When calling Reach for the first time, we set I to be {( , 0) | ∈ S}. When Reach terminates, it outputs the set Q reach of reachable symbolic states. From Q reach , we can extract the set of accepting states by intersecting its elements with the output labels of locations:

Q acc = {( , Z a ) | Z a = Z ∧ o( ) ∧ Z a = ∅ ∧ ( , Z) ∈ Q}. If a configuration ( , (v, v 0 ))
is reachable and accepting (belongs to some element of Q acc ), then the prefix w[0..v(x 0 )] is accepted by the automaton.

Theorem 2 (Termination). Given a finite-variability signal, Algorithm 2 terminates.

Algorithm 3 ReachOnline(A, w i , Q i-1 r )

Require: A timed automaton A, signal segment wi defined on [ti, ti+1), previous set of reachable states Q i-1 r ; Ensure: The set Q i r contains the states reachable while reading wi

I = {( , Z ) | Z = Z ∧ x0 = ti ∧ Z = ∅ ∧ ( , Z) ∈ Q i-1 r
} {States that are reachable when wi starts} return Reach(A, wi, I)

Checking Acceptance Online

Algorithm 2 can be used to perform reachability computation in an online way. We can arbitrarily split the input signal w into segments w 1 , w 2 , • • • , w n and present them one by one to the procedure ReachOnline (Algorithm 3). After processing segment w i , the procedure returns the set of states reachable after reading w 1 • • • w i . From the previous set of reachable states, ReachOnline extracts the states which are reachable at the start of the new segment (those where the absolute time clock satisfies x 0 = |w 1 • • • w i |) and passes them on as initial states for Reach. More formally, we build the sequence

Q 1 r = ReachOnline(A, w 1 , {( , 0) | ∈ S}), Q 2 r = ReachOnline(A, w 2 , Q 1 r ), • • • Q n r = ReachOnline(A, w n , Q n-1 r )
and take the set of reachable states Q reach to be n i=1 Q i r . One useful property of ReachOnline in terms of memory use is that when processing a segment of the signal, it does not need to store previously processed segments and, after the new initial states are extracted, it does not need to store previously computed reachable states. Another property of ReachOnline is that it does not care about how we split w into segments. Segments may have different duration, different number of switching points, etc. The way we split the signal affects the performance though. As the segment size gets smaller, the number of times Algorithm 2 is called increases, but the cost to process a segment decreases. The influence of this parameter on performance is discussed in Section 4.

From Acceptance to Matching

To compute the segments of w which are accepted by an automaton A, we first construct a matching automaton A similar to the one used in the discrete case. It can stay indefinitely in an added initial state before it moves to an initial state of A, resets a clock x s and starts reading the remaining part of w. The automaton also uses the absolute time clock x 0 used for acceptance, see Figure 4. (P, X , L , S , i , o , ∆ ), where

X = X ∪ {x 0 , x s }; L = L ∪ { s }; S = { s }, i = i ∪ { s → true}, o = o ∪ { s → false}; ∆ = ∆ ∪ {( s , true, X -{x 0 }, ) | ∈ S}.
The start time of reading the segment is constantly maintained by the difference x 0 -x s . As a generalization of the case of acceptance, w admits a run that ends in an extended configuration ( , (v, v 0 , v s )) in A iff the signal segment w[v 0 -v s ..v 0 ] admits a run in A that leads to ( , v). Thus Algorithms 2 and 3 applied to A compute the reachable symbolic states in the extended clock space. Projecting zones associated with accepting locations on x 0 and x s we can can extract the matches. From Theorems 2 and 3 it follows that the for a given TRE and expression, the match set can be described by a finite set of zones. This extends the result obtained in [START_REF] Ulus | Timed pattern matching[END_REF] to arbitrary TA.

Example

Let us illustrate the matching algorithm with a simple example. As the pattern specification, we use the expression ϕ = p•q, and we translate it to the automaton shown in Fig. 5. As input, we use the signal w from Fig. 6. The signal is split into two segments: w 1 defined in the interval [0, 4), and w 2 defined in the interval [START_REF] Asarin | A Kleene theorem for timed automata[END_REF][START_REF] Brzozowski | Derivatives of regular expressions[END_REF]. We run the matching algorithm presenting it one segment at a time.

When the segment w 1 arrives, we start the exploration with the symbolic state ( , x 0 = 0) and immediately apply the time transition to it. We can stay in the location until the end of the segment, thus we add to the reachability tree the state s 1 = ( , x 0 ∈ [0, 4]). Next, from s 1 , we execute the discrete transition that leads to p . Changing the location, resetting the clock x s and constraining the zone to the interval where p holds, produces the state ( p , x 0 ∈

[1, 3] ∧ x s = 0 ∧ x 0 -x s ∈ [1, 3]).
Then, applying time elapse until the end of p produces the state

s 2 = ( p , x 0 ∈ [1, 3] ∧ x s = [0, 2] ∧ x 0 -x s ∈ [1, 3]
) that we add to the reachability tree. Finally, we execute from s 2 the discrete transition to q . After changing the location and restricting to the interval where q holds, we get the state

( q , x 0 ∈ [2, 3] ∧ x s ∈ [0, 2] ∧ x 0 -x s ∈ [1, 3]
). After applying time elapse until the end of q (the end of the fragment in this case), we get the state

s 3 = ( q , x 0 ∈ [2, 4] ∧ x s ∈ [0, 3] ∧ x 0 -x s ∈ [1, 3]
) that we add to the tree. We would like to point out again that time transitions from different states are not synchronized. When s 2 was created, we allowed x 0 to advance until time 3. When executing the transition to q , we discover that it could happen "in the past", between time 2 and 3; but also that after taking the transition, we can true p p xs := 0 q out: true q Fig. 5. Matching automaton for the expression p • q. p q 0 1 2 3 4 5 6 7 8 Fig. 6. Example of a signal. stay in q until time 4. At this point, there are no more states to explore, and we report the matches in the observed signal prefix. In this example, the matches are described by the state s 3 intersected with its output label true. Possible values of x 0 -x s in s 3 are the possible start times of the match, and possible values of x 0 are the end times. For us, the match should start between time 1 and 3, while p holds, and end between time 2 and 4, while q holds. We now proceed to read w 2 . We extract from the reachability tree all states that correspond to reading the first segment until the end, that is, states with valuations that lie on the hyperplane x 0 = 4. From state s 0 , we extract ( , x 0 = 4). Applying time transition to it results in the state s 4 = ( , x 0 ∈ [START_REF] Asarin | A Kleene theorem for timed automata[END_REF][START_REF] Brzozowski | Derivatives of regular expressions[END_REF]) that we add to the tree. From state s 3 , we extract ( q , x 0

s1, x0 ∈ [0, 4] s2, p x0 ∈ [1, 3] xs ∈ [0, 2] x0 -xs ∈ [1, 3] s3, q x0 ∈ [2, 4] xs ∈ [0, 3] x0 -xs ∈ [1, 3]
, x0 ∈ [4, 8] s5, p x0 ∈ [5, 7] xs ∈ [0, 2] x0 -xs ∈ [5, 7] s6, q x0 ∈ [5, 6] xs ∈ [0, 1] x0 -xs ∈ [5, 6] s7, q x0 ∈ [4, 6] xs ∈ [1, 5] x0 -xs ∈ [1, 3]
= 4∧x s ∈ [1, 3]∧x 0 -x s ∈ [1, 3]).
Applying time transition to it results in the state

s 7 = ( q , x 0 ∈ [4, 6] ∧ x s ∈ [1, 5] ∧ x 0 -x s ∈ [1, 3
]) that we add to the tree. At this point, we can discard the previous segment of the signal and the reachability tree corresponding to it; they will no longer be used. Then, we restart the exploration from s 4 and s 7 , which discovers two more states: s 5 and s 6 . Both s 6 and s 7 correspond to

Implementation and Experiments

We implemented a prototype of the algorithm in C++, using the zone library of the tool IF [START_REF] Bozga | IF: An intermediate representation and validation environment for timed asynchronous systems[END_REF]. We evaluate the performance of the prototype using a number of patterns and periodic signals of different length. We summarize the experimental results in Table 1. The columns "Expression" and "Signal" give the expression and the shape of the signal. Different expressions and signal shapes are discussed in more detail below. To present time-related parameters in a uniform way, we measure them in integer time units. The column "Seg" gives the length of the signal segment (in time units) that is presented at once to the reachability algorithm. We run every experiment with 2-3 segment lengths: presenting the whole signal at once ("offline") and presenting a fixed number of time units, based on the period of the signal. The last three columns show the results for different length of the signal: 10K, 100K, and 1 million time units. A cell of the table shows the run time of the matching algorithm in seconds and the number of explored symbolic states. The three parameters: signal length, signal shape, and segment length influence the performance of the algorithm in a connected way. The longer are the stable periods of the signal, the fewer switching points it has within a given length; but at the same time, if the segment length is small, longer stable periods become split into more segments. Time figures were obtained on a PC with a Core i7-3630QM and 8GB RAM.

Signals We use three different periodic signal shapes. The signal wave 2 has two components, p 0 and p 1 , which are square waves with the period of 2 time units, p 1 being the negation of p 0 . The signal wave 200 has four components, p 0 to p 3 , which are square waves with the period of 200 time units, shifted in time by different amount. The signal wave 30 /32 has two components, p 0 and p 1 . The component p 0 has the period of 30 time units, in every period it has hi value for 5 time units. The component p 1 has the period of 32 time units, in every period it has hi value for 4 time units.

Simple Expressions Expressions ϕ 1 to ϕ 4 are examples of basic regular operators: concatenation, disjunction, and duration constraint.

Intersection Example Intersection allows to assert that multiple properties should hold during the same interval. To evaluate it, we use the expression

ϕ 5 = ( p [4,5] • ¬p) ∩ (¬q • q [4,5] ) ∩ (true • p ∧ q [1,2] • true)
It denotes a pattern where p holds at the beginning and between 4 to 5 time units, q holds at the end between 4 to 5 time units, and in between p and q hold together for at least 1 to 2 time units. This could be an example of one resource (such as power source) replacing another in a redundant architecture. We cannot express this property without intersection; it would require duration constraints with unbalanced parentheses [START_REF] Asarin | A Kleene theorem for timed automata[END_REF].

Quantification Example Existential quantification allows to express synchronization with a signal which is not part of the input, but is itself described by a

• r [1,3] ) + ∩ (¬p • (¬p ∧ ¬r) • (p ∧ r) • p • (p ∧ ¬r) • (¬p ∧ r)) +
It denotes a signal p that changes its value on the rising edge of a virtual clock, denoted by r, that occurs every 100 ± 1 time units (note how we use (¬p ∧ ¬r) • (p ∧ r) to synchronize the rising edges of p and r). In the experiments, we use this property for prefix matching. We fix the start of the match to the start of the signal and use our algorithm to find matching prefixes. Discussion The run time of the matching algorithm is determined by the number of symbolic states that it explores, which depends on the structure of the expression, the input signal, and the way the signal is split into segments when presented to the matching algorithm. In our experiments, we focused on the case when the length of a segment given to the algorithm is greater than or equal to the length of a stable state of the signal. For example, for the signal wave 200 , we normally observe two cases: when the algorithm receives the whole signal immediately, and when the signal is split into segments 100 time units in length, which is the half-period of the signal. In this setup, for a variety of regular expressions we observe two properties of the algorithm: (i) the number of explored configurations (and thus the runtime) is linear in the length of the signal; and (2) going from offline to online matching (with the length of a segment greater or equal to the length of a stable state) increases the number of explored configurations only by a small constant factor. That said, one can always come up with adversarial examples, where the match set (and thus the number of explored configurations) requres at least quadratic number of zones in the length of the signal. One way to construct adversarial examples is to synchronize the start and end of a match with some event, e.g., a raising or a falling edge. In our experiments, this happens in the property ϕ 6 . For the signal wave 200 , every sequence of one or more full signal periods is a match, and the set of all matches is described by a quadratic number of zones. For this reason, we only do prefix matching in that experiment. Another way to construct adversarial examples is to perform "oversampling" and split every stable state of the input signal into a large number of segments. As a result, every zone in the match set may be split in a quadratic number of smaller zones, since the matches that start and/or end in different segments cannot be part of the same zone in the current algorithm. We can observe this effect for the property ϕ 1 and the signal wave 200 . Reducing the segment length from 100 to 25 time units causes oversampling and increases the number of explored configurations by a factor of 8 = 4 2 /2. In future work, we wish to address this issue, as it is reminiscent of the issue of interleaving in reachability of timed automata, which was addressed in [START_REF] Salah | On interleaving in timed automata[END_REF].

Removing Inactive Clocks The cost of zone operations is in the worst case cubic in the number of clocks (normalization is cubic, but is not required for some operations), thus it is important to remove clocks as soon as they are no longer needed. For automata produced from TREs, this is not difficult to do, since every clock is tied to a duration constraint and thus has a clearly defined set of locations where it is active (x 0 and x s are always active). When taking a transition, we erase (existentially quantify) clocks that are not active in the target location.

Introducing Clock Invariants The simple encoding of duration constraints that we describe may lead, during state exploration, to the creation of doomed symbolic states that may never lead to an accepting state. When time transition is applied to a state, we may increase a clock past a bound that will be much later checked by a guard of some transition. In the meantime, we may start exploring the successors of the doomed state, which are also doomed, then their successors, etc. To reduce the amount of such redundant work, in our implementation, we let locations have clock invariants. They are produced from the upper bounds of duration constraints and we use them to constrain the result of time transitions.

Conclusion

We presented a novel algorithm for timed pattern matching of Boolean signals.

We are particularly interested in patterns described by timed regular expressions, but our result applies to arbitrary timed automata. The algorithm can be applied online, without restriction on how the input signal is split into incrementally presented segments. The prototype implementation shows promising results, but also points out some pessimistic scenarios. In future work, we plan to improve the performance of matching with the major goal being to improve the handling of small signal segments by adapting partial order reduction techniques; we also expect that some constant factor can be gained by improving the quality of the code. In another direction, we wish to perform a more in-depth case study to be able to adapt the algorithm to the specifics of real applications.

Fig. 1 .Fig. 2 .

 12 Fig. 1. A non-deterministic automaton for (a ∪ b) * • (b ∪ c) + .

2 cFig. 3 .

 23 Fig. 3. Runs of the automaton in Fig. 1.Left -all runs for the word abbabc. Rightbreadth-first on-the-fly subset construction.

  A Boolean signal w of duration |w| = d is a right-continuous function w : [0, d) → B n whose value at time t is denoted by w[t]. We use w[t..t ] to denote the part of signal w between absolute times t and t . The concatenation of two signals w and w of respective durations d and d is the signal ww of duration d + d defined as ww

Definition 5 (Fig. 4 .

 54 Fig. 4. Matching automaton A for a property automaton A.

Fig. 7 .

 7 Fig. 7. Reachable symbolic states after reading the first fragment of the signal.

  s4

Fig. 8 .

 8 Fig. 8. Reachable symbolic states after reading the second fragment of the signal. States corresponding to the previous fragment were discarded.

Table 1 .

 1 Evaluation results.

	Expression		Signal	Seg	10K	Signal length 100K	1M
			wave2	offline 0.1s, 10K 0.96s, 100K 16s, 1M 1 0.14s, 30K 1.4s, 300K 21s, 3M
	ϕ1 = p0 • p1			signal < 0.01s, 100 0.02s, 1K 0.1s, 10K
			wave200	100 < 0.01s, 350 0.03s, 3.5K 0.18, 35K
				25 0.02s, 2.4K 0.1s, 24K 0.84s, 240K
	ϕ2 = p0 [0,20] • p1 [0,20] • p2 [0,20]	wave200	offline < 0.01s, 150 0.03s, 1.5K 0.22s, 15K 100 < 0.01s, 450 0.06s, 4.5K 0.4s, 45K
	ϕ3 = (p0 ∪ p1) • (p2 ∪ p3)	wave200	offline < 0.01s, 300 0.03s, 3K 0.24s, 30K 100 0.01s, 900 0.05s, 9K 0.4s, 90K
	ϕ4 = p1 • (p0 • p2) +	[0,1000] wave200	offline < 0.01s, 250 0.03s, 2.5K 0.26s, 25K 100 < 0.01s, 500 0.04s, 5K 0.3s, 50K
	ϕ5 (see text)		wave 30 /32	offline 0.02s, 800 30 0.03s, 1.4K 0.14s, 14K 1.4s, 140K 0.1s, 8K 1s, 80K
	ϕ6 (prefix match, see text) wave200	offline 0.01s, 400 100 0.03s, 6.3K 2.7s, 500K 0.04, 4K 0.24s, 40K TO

regular expression. To evaluate quantification, we use the expression ϕ 6 = ∃r. ( ¬r

[98,98]

q and describe newly discovered matches. State s 6 corresponds to the matches that start and end between time 5 and 6, when q still holds and p holds again. State s 7 corresponds to matches that start between time 11 and 3, that is, in the previous segment) and end before time 6 in the current segment.

This research was supported in part by the Austrian Science Fund (FWF) under grants S11402-N23 (RiSE/SHiNE) and Z211-N23 (Wittgenstein Award), and by the European Research Council under the European Union's Seventh Framework Programme (FP/2007-2013) / ERC Grant Agreement nr. 306595 "STATOR".

Algorithm 1 Succ( , Z)

Require: A timed automaton A and symbolic state ( , Z); Require: An input signal w for which J ( , w) has been computed for every location. Ensure: The set Q of successors of ( , Z) by one transition and one time step.

) {Compute the sub-zones of Z in which time can progress} for all non-empty ( , Z ) ∈ Q2 do

)} {Add to visited} P := P ∪ {( , Z )} {Add to pending} end if end for end while return Q reach Termination follows from the fact that the set of symbolic states is finite in our case. We can scale the signal so that all the switching points come at integer times, then, we can use zones with integer coefficients in Algorithm 2. The largest possible value of a clock and thus the largest constant that can appear in a reachable symbolic state is the duration of the signal, hence the number of possible symbolic states is finite.

Theorem 3 (Completeness).

There exists a run of the automaton A:

By induction on the number of discrete transitions, every reachable configuration is eventually visited by the algorithm as part of some symbolic state.


Lara Sassine

Mahmoud Khaska

Sophie Ressouche

Roland Simler

Joël Lancelot

Patrick Verdoux

Corinne Le Gal

La Salle

Coupling geochemical tracers and pesticides to determine recharge origins of a shallow alluvial aquifer: Case study of the Vistrenque hydrogeosystem (SE France)

niveau recherche, publiés ou non, émanant des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.