Online Timed Pattern Matching Using Derivatives
 18 Citations
 1.3k Downloads
Abstract
Timed pattern matching consists in finding all segments of a densetime Boolean signal that match a pattern defined by a timed regular expression. This problem has been formulated and solved in [17] via an offline algorithm that takes the signal and expression as inputs and produces the set of all matches, represented as a finite union of twodimensional zones. In this work we develop an online version of this approach where the input signal is presented incrementally and the matching is computed incrementally as well.
Naturally, the concept of derivatives of regular expressions due to Brzozowski [6] can play a role in defining what remains to match after having read a prefix of the signal. However the adaptation of this concept is not a straightforward for two reasons: the dense infinitestate nature of timed behaviors and the fact that we are interested in matching, not only in prefix acceptance. To resolve these issues we develop an alternative theory of signals and expressions based on absolute time and show how derivatives are defined and computed in this setting. We then implement an online timed pattern matching algorithm based on these results.
Keywords
Temporal Logic Regular Expression Constant Signal Propositional Variable Empty Word1 Introduction
Timed regular expressions (tre), introduced in [3, 4], constitute a formalism for expressing patterns in timed behaviors in a compact and natural way. They augment classical regular expressions with timing constraints and as such they provide an alternative specification style to realtime temporal logics such as MTL [10]. We believe that such expressions have numerous applications in many domains such as runtime verification, robotics, medical monitoring and circuit analysis [7, 9].
For a given expression \(\varphi \) and input signal w, timed pattern matching means computing the match set \(\mathcal {M}(\varphi , w)\) consisting of all pairs \((t,t')\) of time instants such that the segment of w between t and \(t'\) satisfies the expression \(\varphi \). In [17] we showed how to compute \(\mathcal {M}(\varphi , w)\) offline, assuming the input signal to be completely available before the matching. In this paper we develop an online matching algorithm where the input is presented incrementally and matches are computed on the fly. An online procedure can be used to monitor real systems during their actual executions (in contrast with monitoring simulations) and alert the user in real time. In addition, an online procedure can reduce memory requirements, discarding signals and intermediate matches when those are no longer needed.
The online pattern matching procedure that we develop in this paper is built upon the notion of derivatives of regular expressions, introduced by Brzozowski in 1964 [6]. In essence, the derivative of an expression with respect to a letter or word, tells us what remains to be observed in order to reach acceptance. In this sense it is very similar to the tableaux construction used to build automata from temporal logic formulae. Derivatives provide an elegant solution for problems of language membership [14], pattern matching [13, 16] and automaton construction [1, 5, 6] and have been observed to be naturally suitable for monitoring behaviors of systems [12, 15]. The original notion of the derivative that we recall in Sect. 2 is based on discrete time and requires a careful adaptation to dense time. Moreover, as we will explain, matching is more complex than acceptance (of the word or its prefixes) and this has some implications on associating derivatives with rewrite rules.
In Sect. 3 we modify the definition of signals, one of the commonlyused formalisms to express timed behaviors, so as to lift the theory of derivatives to the timed setting. Signals (and sequences) are traditionally defined to start at time zero and when two signals are concatenated as in \(w=u\cdot v\), the second argument v is shifted forward in time, to start at the end of u. In contrast, we define signals in absolute time, each having its own fixed starting point. In this setting concatenation becomes a partial function, defined only when the domains of definition of the two signals fit. We also introduce a special place holder symbol \(\checkmark \) and define extended signals where all letters in some prefix have been replaced by this symbol.
We then adapt timed regular expressions to represent sets of extended signals using the absolute time semantics. The regular expressions of [3, 4, 17] are obtained as a syntactic subclass denoting “pure” \(\checkmark \)free signals, used for the initial specification. The more general expressions are used to represent intermediate stages during the incremental computation of the match set.
In Sect. 4 we introduce our main technical contribution: the definition and computation of derivatives of leftreduced timed regular expressions with respect to a constant signal of arbitrary duration and all its factors. We apply this result to solve the problem of online timed pattern matching in Sect. 5 where we observe an input signal consisting of a finite concatenation of constant signals. We give a complete example of a run of our algorithm and briefly mention our implementation and its performance.
2 Preliminaries
Definition 1
It is of course not a coincidence that this procedure resembles the reading of the word by an automaton where derivatives correspond to states and those that contain \(\epsilon \) correspond to accepting states. Hence we can report membership in \(\llbracket \varphi \rrbracket \) of w as well as the membership of all its prefixes. We can do it incrementally as new letters arrive.
Pattern matching using derivatives for \(w=abcbc\) and \(\varphi = a^{*}\cdot (b\cdot c)^{*}\). Entry (i, j) represents the derivative with respect to w[i, j]. Derivatives containing \(\epsilon \) are shaded with green. The state of an online matching algorithm after reading j symbols is represented in column j.
In dense time, the analogue of the arrival of a new letter is the arrival of a constant segment of the signal \(w[t_1,t_2]\). When this occurs, the state of the algorithm should be updated to capture all derivatives by segments of the form \(w[t,t_2]\) for \(t<t_2\) and all matches ending in some \(t<t_2\) should be extracted. The technique for representing and manipulating such an uncountable number of derivative together with their corresponding time segments is the main contribution of this paper.
3 Signals, Timed Languages and Expressions
We consider an alphabet \(\varSigma =\mathbb {B}^m\) which is the set of valuations of a set of propositional variables \(P=\{p_1\ldots ,p_m\}\). We define signals not as free floating objects but anchor them in absolute time.
Definition 2
We use \(w[t, t']\) to denote the restriction of w to an interval \([t, t') \subseteq dom (w)\) and let \(Sub (w) = \{ w[t,t']\ \ \tau _{1}(w)\le t < t' \le \tau _{2}(w)\}\) be the set of subsignals (factors, segments) of w. Concatenation is restricted to signals that meet, that is, one ends where the other starts.
Definition 3
The empty signal \(\epsilon \) is the neutral element for concatenation: \(\epsilon \cdot w = w\cdot \epsilon = w\). The set of signals thus defined can be made a monoid by making concatenation total by introducing a new element \(\bot \) and letting \(w_1 \cdot w_2=\bot \) when the signals do not meet. The newly introduced element is an absorbing zero satisfying \(\bot \cdot w = w\cdot \bot = \bot \).
The variability (logical length) of a signal w is the minimal n such that w can be written as \(w = w_{1}\cdot w_{2}\cdots w_{n}\) where each \(w_{i}\) is a constant signal. We use notations \(\varSigma ^{(*)}\), \(\varSigma ^{(+)}\) and \(\varSigma ^{(n)}\) to denote the set of all signals, nonempty signals and signals of variability n, respectively. In particular, \(\varSigma ^{(1)}\) is the set of all constant signals. Sets of signals are referred to as signal languages on which Boolean operations as well as concatenation and star are defined naturally. Finally we extend the time restriction operation of [4] which constrains the duration of signals, to apply also to their time domains. The language \(^{K}_{J}\langle \mathcal {L}\rangle _{I}\) where I, J, K are intervals of nonnegative reals, is a subset of \(\mathcal {L}\) consisting of signals with duration in I, beginning in \(t_1\in J\) and ending in \(t_2\in K\). We omit the corresponding interval when there is no restriction on beginning, ending or duration.
Definition 4
(Extended Signals). An extended signal over alphabet \(\varSigma \) is a function \(w:[t,t')\rightarrow \varSigma _\checkmark \). An extended signal w is leftreduced if \(w\in \checkmark ^{(*)}\cdot \varSigma ^{(*)}\). A leftreduced signal w is pure if \(w\in \varSigma ^{(*)}\) and reduced if \(w\in \checkmark ^{(*)}\).
We use initial Greek letters to denote reduced signals and hence a leftreduced signal w will be written as \(w = \alpha \cdot v\) where \(\alpha \) is a reduced signal and v is a pure signal.
Definition 5
We use operation \(\delta _u(\mathcal {L})\) in a similar way \(D_u(\mathcal {L})\) is used in the classical setting but with one important difference. When \(v=D_u(w)\) the length of the word is reduced, that is, \(v=wu\), while when \(v=\delta _u(w)\) the domains (and hence durations) of v and w are the same. Consequently, unlike the classical case where membership of w in \(\mathcal {L}\) amounts to \(\epsilon \in D_w(\mathcal {L})\), here the membership is equivalent to \(\gamma \in \delta _w(\mathcal {L})\) where \(\gamma \) is a reduced signal of the same domain as w. It is not difficult to check that \(\delta _{u_{1}\cdot u_{2}}(\mathcal {L}) = \delta _{u_{2}}(\delta _{u_{1}}(\mathcal {L}))\) and sometimes we denote by \(\delta _{S}\) the left reduction with respect to a set of signals.
Example 1
We now introduce timed regular expressions to describe sets of signals and extended signals using the absolute time semantics. Note that the intersection operator, which is considered a syntactic sugar in the classical theory, adds expressiveness in the timed setting [4].
Definition 6
The syntax in Definition 6 allows to define sets including extended signals with arbitrary interleavings of letters and \(\checkmark \). Below we define three syntactic classes of expressions. The first class, called pure (or original) timed regular expressions, corresponds almost the same syntax of expressions seen in [3, 4, 17]. Pure expressions are \(\checkmark \)free and do not place any restriction on the absolute beginning and ending values over their subexpressions. The second class is reduced timed regular expressions which is formed using the \(\checkmark \) symbol only. Lastly we have leftreduced timed regular expressions, obtained as compositions of reduced and pure expressions satisfying some conditions.
Definition 7
Trivially any reduced expression \(\psi \) and any pure expression \(\varphi \) represent reduced and pure signal languages such that \(\llbracket \psi \rrbracket \subseteq \checkmark ^{(*)}\) and \(\llbracket \varphi \rrbracket \subseteq \varSigma ^{(*)}\). For leftreduced expressions we do not allow concatenation and star operations on arbitrary leftreduced expressions as in Definition 7 because leftreduced languages are not closed under concatenation. By doing that we have the following result.
Proposition 1
The language \(\llbracket \varphi \rrbracket \) of a leftreduced timed regular expression \(\varphi \) is an extended signal language such that \(\llbracket \varphi \rrbracket \subseteq \checkmark ^{(*)}\cdot \varSigma ^{(*)}\).
Proof
For the concatenation \(\varphi _{1}\cdot \varphi _{2}\) we have two possibilities: (1) \(\llbracket \varphi _{1}\rrbracket \subset \checkmark ^{(*)}\cdot \varSigma ^{(*)}\) and \(\llbracket \varphi _{2}\rrbracket \subset \varSigma ^{(*)}\); (2) \(\llbracket \varphi _{1}\rrbracket \subset \checkmark ^{(*)}\) and \(\llbracket \varphi _{2}\rrbracket \subset \checkmark ^{(*)}\cdot \varSigma ^{(*)}\). For both possibilities, we have \(\llbracket \varphi _{1}\cdot \varphi _{2}\rrbracket = \llbracket \varphi _{1}\rrbracket \cdot \llbracket \varphi _{2}\rrbracket \subset \checkmark ^{(*)}\cdot \varSigma ^{(*)}\). Other cases are straightforward by following the definitions.
4 Derivatives of LeftReduced Timed Regular Expressions
We now introduce, semantically and syntactically, a derivative operation for leftreduced signal languages and expressions based on the left reduction operation. Since our goal is to solve the dense time matching problem, we have to operate on sets of signals and define derivatives more symbolically. Therefore we define the derivative \(\varDelta _{v}\) to correspond to the left reduction with respect to all factors of v.
Definition 8
As mentioned previously, reduced signals will provide the output of our matching procedure. Their existence will be the witness of a match and their time domains will indicate its position in the signal.
Definition 9
The following result shows that \(\text {xt}\) can be computed syntactically for leftreduced timed regular expressions.
Theorem 1
Proof
Example 2
Consider a leftreduced expression \(\varphi := \big \langle \ ^{[0,3]}_{[0,3]}\langle \checkmark \rangle _{[0,3]}\cdot p^{*} \big \rangle _{[0,2]}\). Applying Theorem 1 we extract from \(\varphi \) a reduced expression \(\psi \) such that \(\psi = \big \langle \ ^{[0,3]}_{[0,3]}\langle \checkmark \rangle _{[0,3]} \big \rangle _{[0,2]}\). Expression \(\psi \) can be simplified further to \(^{[0,3]}_{[0,3]}\langle \checkmark \rangle _{[0,2]}\).
We now state our main result concerning derivatives of leftreduced timed regular expressions.
Theorem 2
Proof

For \(\varphi = \varnothing \), \(\varphi = \epsilon \) and \(\varphi = \checkmark \) : for all cases \(\alpha uw \notin \llbracket \varphi \rrbracket \) therefore \(\varDelta _{v}(\varphi ) = \varnothing \).
 For \(\varphi = p\) : It needs that \(\alpha = \epsilon \) and \(u\in \llbracket p \rrbracket \). Then, \(\alpha uw \in \llbracket p \rrbracket \) can be satisfied if either \(w = \epsilon \) or \(w\in \llbracket p \rrbracket \). By applying definitions, we getwhere the expression \(\varGamma \) is \(^{[t,t']}_{[t,t']}\langle \checkmark \rangle _{[0,t't]}\). Hence, we have \(\varDelta _{v}(p) = \varGamma \vee \varGamma \cdot p\) if \(u\in \llbracket p \rrbracket \), otherwise \(\varDelta _{v}(p) = \varnothing \). The condition \(u\in \llbracket p \rrbracket \) can be easily checked by testing \(a\;{\models }\;p\).$$\begin{aligned} \begin{array}{rcl} \varDelta _{v}(p)&{} = &{} \{\ \gamma \ \ u\in \llbracket p \rrbracket \text { and } (u, \gamma )\in \text {RSub}(v)\}\ \cup \\ &{} &{} \{\ \gamma w\ \ u\in \llbracket p \rrbracket ,\ w\in \llbracket p \rrbracket \text { and } (u, \gamma )\in \text {RSub}(v) \}\\ &{} = &{} \varGamma \vee \varGamma \cdot \{ w\ \ w\in \llbracket p \rrbracket \}\\ &{} = &{} \varGamma \vee \varGamma \cdot p \end{array} \end{aligned}$$
 For \(\varphi = \varphi _{1}\cdot \varphi _{2}\) : \(\alpha uw \in \llbracket \varphi _{1}\cdot \varphi _{2} \rrbracket \) should be satisfied. There are three possibilities to split \(\alpha u w\) in dense time:
 \(\centerdot \) It can be split up into \(\alpha uw_{1}\in \llbracket \varphi _{1}\rrbracket \) and \(w_{2}\in \llbracket \varphi _{2}\rrbracket \).$$\begin{aligned} \begin{array}{rcl} \varDelta _{v}(\varphi ) &{} = &{} \{ \alpha \gamma w_{1}w_{2}\ \ \alpha u w_{1}\in \llbracket \varphi _{1}\rrbracket ,\ w_{2}\in \llbracket \varphi _{2}\rrbracket \text { and } (u, \gamma )\in \text {RSub}(v)\}\\ &{} = &{} \{ \alpha \gamma w_{1}\ \ \alpha u w_{1}\in \llbracket \varphi _{1} \rrbracket \text { and } (u, \gamma )\in \text {RSub}(v)\}\cdot \{ w_{2}\ \ w_{2}\in \llbracket \varphi _{2}\rrbracket \}\\ &{} = &{} \varDelta _{v}(\varphi _{1})\cdot \varphi _{2}\\ \end{array} \end{aligned}$$
 \(\centerdot \) It can be split up into \(\alpha _{1}\in \llbracket \varphi _{1}\rrbracket \) and \(\alpha _{2}uw\in \llbracket \varphi _{2}\rrbracket \).$$\begin{aligned} \begin{array}{rcl} \varDelta _{v}(\varphi ) &{} = &{} \{ \alpha _{1}\alpha _{2}\gamma w\ \ \alpha _{1}\in \llbracket \varphi _{1}\rrbracket ,\ \alpha _{2} u w\in \llbracket \varphi _{2}\rrbracket \text { and } (u, \gamma )\in \text {RSub}(v)\}\\ &{} = &{} \{ \alpha _{1}\ \ \alpha _{1}\in \llbracket \varphi _{1} \rrbracket \}\cdot \{ \alpha _{2}\gamma w\ \ \alpha _{2}uw\in \llbracket \varphi _{2}\rrbracket \text { and } (u, \gamma )\in \text {RSub}(v)\}\\ &{} = &{} \text {xt}(\varphi _{1})\cdot \varDelta _{v}(\varphi _{2})\\ \end{array} \end{aligned}$$
 \(\centerdot \) It can be split up into \(\alpha u_{1}\in \llbracket \varphi _{1}\rrbracket \) and \(u_{2}w\in \llbracket \varphi _{2}\rrbracket \). For this case, it is required by definitions that \(\varphi _{1}\) is a leftreduced expression and \(\varphi _{2}\) is a pure expression. This is the most involved case requiring to split reducing signals.$$\begin{aligned} {\begin{array}{rcl} \varDelta _{v}(\varphi ) &{} = &{} \{ \alpha \gamma _{1}\gamma _{2} w\ \ \alpha u_{1}\in \llbracket \varphi _{1}\rrbracket ,\ u_{2}w\in \llbracket \varphi _{2}\rrbracket \text { and } (u_{1}u_{2}, \gamma _{1}\gamma _{2})\in \text {RSub}(v)\}\\ &{} = &{} \{ \alpha \gamma _{1}\gamma _{2} w\ \ \alpha u_{1}\in \llbracket \varphi _{1}\rrbracket ,\ u_{2}w\in \llbracket \varphi _{2}\rrbracket ,\ (u_{1}, \gamma _{1})\in \text {RSub}(v),\\ &{} &{}\quad (u_{2}, \gamma _{2})\in \text {RSub}(v) \text { and } (u_{1}, \gamma _{1}) \text { meets } (u_{2}, \gamma _{2})\}\\ &{} = &{} \{ \alpha \gamma _{1}\ \ \alpha u_{1}\in \llbracket \varphi _{1} \rrbracket \text { and } (u_{1}, \gamma _{1})\in \text {RSub}(v)\}\cdot \\ &{} &{} \quad \{\gamma _{2}w\ \ u_{2}w\in \llbracket \varphi _{2} \rrbracket \text { and } (u_{2}, \gamma _{2})\in \text {RSub}(v)\}\\ &{} = &{} \text {xt}(\varDelta _{v}(\varphi _{1}))\cdot \varDelta _{v}(\varphi _{2})\\ \end{array}} \end{aligned}$$
Thus \(\varDelta _{v}(\varphi _{1}\cdot \varphi _{2})\) can be found by the disjunction of these three cases. Then, by rearranging the last two cases, we obtain the equality claimed in the theorem.

 For \(\varphi = \psi ^{*}\): assume without loss of generality \(\epsilon \not \in \psi \). Then$$\begin{aligned} \begin{array}{rcl} \varDelta _{v}(\psi ^{*}) &{} = &{} \varDelta _{v}(\epsilon ) \vee \varDelta _{v}(\psi \cdot \psi ^{*})\\ &{} = &{} \varDelta _{v}(\psi )\cdot \psi ^{*}\ \vee \ \text {xt}(\psi )\cdot \varDelta _{v}(\psi ^{*})\ \vee \ \text {xt}(\varDelta _{v}(\psi ))\cdot \varDelta _{v}(\psi ^{*})\\ &{} = &{} \varDelta _{v}(\psi )\cdot \psi ^{*}\ \vee \ \text {xt}(\varDelta _{v}(\psi ))\cdot \varDelta _{v}(\psi ^{*})\\ &{} = &{} [\epsilon \ \vee \ X\ \vee \ X^{2}\ \vee \dots \vee \ X^{\infty }]\cdot \varDelta _{v}(\psi )\cdot \psi ^{*} \text { where } X =\text {xt}(\varDelta _{v}(\psi )) \\ &{} = &{} \text {xt}(\varDelta _{v}(\psi ))^{*}\cdot \varDelta _{v}(\psi )\cdot \psi ^{*} \\ \end{array} \end{aligned}$$

Time restriction and Boolean operations follow definitions straightforwardly.
Corollary 1
The derivative \(\varDelta _{v}(\varphi )\) of a leftreduced timed regular expression \(\varphi \) with respect to a constant signal v is a leftreduced timed regular expression.
Proof
Theorem 2 shows that only finite number of regular operations is required to find the derivative and these equations satisfy requirements in Definition 7.
Lemma 1
Proof
5 Application to Online Timed Pattern Matching
Definition 10
Theorem 3
Proof
Following Definition 10 and Lemma 1 we know the state \(\psi _{j}\) represents a reduced language \(\delta _S(\varphi )\) of \(\varphi \) with respect to a set of signals S satisfying \(s\in \text {Sub}(w)\) and \(\tau _{2}(s)\in \text {dom}(w_{j})\). A reduced signal \(\alpha \) in \(\delta _S(\varphi )\) indicates the existence of a signal \(s\in S\) such that \(\tau (s)=\tau (\alpha )\) and \(s\in \llbracket \varphi \rrbracket \), thus s is a match. Then we can find the match set \(\mathcal {M}_{j}\) by extracting all reduced signals from the state \(\psi _{j}\).
 1.
Extract \(\varphi \) to see if the empty word is a match.
 2.For \(1 \le j \le n\) repeat:
 (a)
Update the state of the matching \(\psi _{j}\) by deriving the previous state \(\psi _{j1}\) with respect to \(w_{j}\) and adding a new derivation \(\varDelta _{w_{j}}(\varphi )\) to the state for matches starting in segment j.
 (b)
Extract \(\psi _{j}\) to get matches ending in segment j.
 (a)
Timed pattern matching using derivatives for \(w=w_{1}w_{2}w_{3}\) and \(\varphi = \langle p\cdot q \rangle _{I}\). Entries represent the derivative with respect to \(w_{i..j}\). Reduced expressions, indicating matched segments, are shaded with green. (\(I=[4,7]\), \(\varGamma _{1} =\ ^{[0,3]}_{[0,3]} \langle \checkmark \rangle _{[0,3]}\), \(\varGamma _{2} =\ ^{[3,8]}_{[3,8]} \langle \checkmark \rangle _{[0,5]}\) and \(\varGamma _{3} =\ ^{[8,10]}_{[8,10]} \langle \checkmark \rangle _{[0,2]}\)).
Execution times/Memory usage (in seconds/megabytes)
Test Patterns  Offline Algorithm Input Size  Online Algorithm Input Size  

100 K  500 K  1 M  100 K  500 K  1 M  
p  0.06/17  0.27/24  0.51/33  6.74/14  29.16/14  57.87/14 
\(p\cdot q\)  0.08/21  0.42/46  0.74/77  8.74/14  42.55/14  81.67/14 
\(\langle p\cdot q \cdot \langle p\cdot q \cdot p\rangle _{I}\cdot q \cdot p\rangle _{J}\)  0.23/28  1.09/77  2.14/140  28.07/14  130.96/14  270.45/14 
\((\langle p\cdot q \rangle _{I}\cdot r) \wedge (p\cdot \langle q\cdot r \rangle _{J})\)  0.13/23  0.50/51  1.00/86  15.09/15  75.19/15  148.18/15 
\(p\cdot (q \cdot r)^{*}\)  0.11/20  0.49/37  0.96/60  11.53/15  52.87/15  110.58/15 
6 Conclusions
The contribution of the paper is both theoretical and practical. From a theoretical standpoint we have tackled the difficult problem of exporting the concept of derivatives from discrete to timed behaviors, languages and expressions. To this end we introduced a new approach to handle signals in absolute time, yielding a new type of monoid with interesting properties that by itself is worth investigating in the future. We have shown that such derivatives can be computed syntactically using leftreduced timed regular expressions and that all the matches of the expressions in the signal can be extracted from this representation.
We have used these results to implement a novel procedure for online pattern matching for timed behavior that can be used to monitor systems in real time and detect occurrences of complex patterns. Our procedure consumes a constant segment from the input signal and reports a set of matches ending in that segment before processing the next segment. The algorithm can be applied, of course, to the discrete case where words are viewed as signals that can change their values only at integer times. Despite the overhead, our algorithm might be advantageous for words that have long periods of stuttering if a delay in the detection of matching can be tolerated.
We believe that this procedure has a lot of potential applications in detecting temporal patterns at different time scales. It can be used, for example to detect patterns in music as in [8], in cardiac behavior or in speech. To this end the expression should be extended with predicates over real numbers [7] as in the passage from MTL to STL (signal temporal logic) [11]. Other potential application domains could be the detection of congestions in traffic or in communication network and the analysis of execution logs of organizations information systems or web servers, for example to detect internet robots or customers who are about to abandon our web site.
Footnotes
 1.
To keep the survey within a reasonable size and avoid tedious repetitions, the description here is not fully rigorous, using the same notation for the semantic notion of a left quotient, which is unique for every language and word, and the syntactic notion of a derivative of a regular expression. The derivation of the minimal automaton from a regular expression, for example, requires additional rewrite rules to detect equivalence between different regular expressions.
Notes
Acknowledgement
This work was partially supported by the French ANR projects EQINOCS and CADMIDIA and benefitted from useful comments made by anonymous referees.
References
 1.Antimirov, V.M.: Partial derivatives of regular expressions and finite automaton constructions. Theor. Comput. Sci. 155(2), 291–319 (1996)MathSciNetCrossRefzbMATHGoogle Scholar
 2.Antimirov, V.M., Mosses, P.D.: Rewriting extended regular expressions. Theor. Comput. Sci. 143(1), 51–72 (1995)MathSciNetCrossRefzbMATHGoogle Scholar
 3.Asarin, E., Caspi, P., Maler, O.: A Kleene theorem for timed automata. In: Logic in Computer Science (LICS), pp. 160–171 (1997)Google Scholar
 4.Asarin, E., Caspi, P., Maler, O.: Timed regular expressions. J. ACM 49(2), 172–206 (2002)MathSciNetCrossRefzbMATHGoogle Scholar
 5.Berry, G., Sethi, R.: From regular expressions to deterministic automata. Theor. Comput. Sci. 48(3), 117–126 (1986)MathSciNetCrossRefzbMATHGoogle Scholar
 6.Brzozowski, J.A.: Derivatives of regular expressions. J. ACM 11(4), 481–494 (1964)MathSciNetCrossRefzbMATHGoogle Scholar
 7.Ferrère, T., Maler, O., Ničković, D., Ulus, D.: Measuring with timed patterns. In: Kroening, D., Păsăreanu, C.S. (eds.) CAV 2015. LNCS, vol. 9207, pp. 322–337. Springer, Heidelberg (2015)CrossRefGoogle Scholar
 8.Giavitto, J.L., Echeveste, J.: Realtime matching of antescofo temporal patterns. In: Principles and Practice of Declarative Programming (PPDP), pp. 93–104 (2014)Google Scholar
 9.Havlicek, J., Little, S.: Realtime regular expressions for analog and mixedsignal assertions. In: Formal Methods in ComputerAided Design (FMCAD), pp. 155–162 (2011)Google Scholar
 10.Koymans, R.: Specifying realtime properties with metric temporal logic. RealTime Syst. 2(4), 255–299 (1990)CrossRefGoogle Scholar
 11.Maler, O., Nickovic, D., Pnueli, A.: Checking temporal properties of discrete, timed and continuous behaviors. In: Avron, A., Dershowitz, N., Rabinovich, A. (eds.) Pillars of Computer Science. LNCS, vol. 4800, pp. 475–505. Springer, Heidelberg (2008)CrossRefGoogle Scholar
 12.MorinAllory, K., Borrione, D.: Online monitoring of properties built on regular expressions. In: Forum on specification and Design Languages, (FDL), pp. 249–255 (2006)Google Scholar
 13.Owens, S., Reppy, J.H., Turon, A.: Regularexpression derivatives reexamined. J. Funct. Program. 19(2), 173–190 (2009)MathSciNetCrossRefzbMATHGoogle Scholar
 14.Rosu, G., Viswanathan, M.: Testing extended regular language membership incrementally by rewriting. In: Rewriting Techniques and Applications (RTA), pp. 499–514 (2003)Google Scholar
 15.Sen, K., Rosu, G.: Generating optimal monitors for extended regular expressions. Electron. Notes Theor. Comput. Sci. 89(2), 226–245 (2003)CrossRefGoogle Scholar
 16.Sulzmann, M., van Steenhoven, P.: A flexible and efficient ML lexer tool based on extended regular expression submatching. In: Cohen, A. (ed.) CC 2014 (ETAPS). LNCS, vol. 8409, pp. 174–191. Springer, Heidelberg (2014)CrossRefGoogle Scholar
 17.Ulus, D., Ferrère, T., Asarin, E., Maler, O.: Timed pattern matching. In: Legay, A., Bozga, M. (eds.) FORMATS 2014. LNCS, vol. 8711, pp. 222–236. Springer, Heidelberg (2014)Google Scholar