{'fraction_non_alphanumeric': 0.04890198389314476, 'fraction_numerical': 0.00983696719701434, 'mean_word_length': 3.768856083030462, 'pattern_counts': {'":': 0, '<': 8, '<?xml version=': 0, '>': 11, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 59, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Symbolic Register Automata for Complex Event Recognition and Forecasting

We propose an automaton model which is a combination of symbolic and register automata, i.e., we enrich symbolic automata with memory. We call such automata Symbolic Register Automata (SRA). SRA extend the expressive power of symbolic automata, by allowing Boolean formulas to be applied not only to the last element read from the input string, but to multiple elements, stored in their registers. SRA also extend register automata, by allowing arbitrary Boolean formulas, besides equality predicates. We study the closure properties of SRA under union, intersection, concatenation, Kleene closure, complement and determinization and show that SRA, contrary to symbolic automata, are not in general closed under complement and they are not determinizable. However, they are closed under these operations when a window operator, quintessential in Complex Event Recognition, is used. We show how SRA can be used in Complex Event Recognition in order to detect patterns upon streams of events, using our framework that provides declarative and compositional semantics, and that allows for a systematic treatment of such automata. We also show how the behavior of SRA, as they consume streams of events, can be given a probabilistic description with the help of prediction suffix trees. This allows us to go one step beyond Complex Event Recognition to Complex Event Forecasting, where, besides detecting complex patterns, we can also efficiently forecast their occurrence.


Introduction
A Complex Event Recognition (CER) system takes as input a stream of events, along with a set of patterns, defining relations among the input events, and detects instances of pattern satisfaction, thus producing an output stream of complex events [1,2,3]. Typically, an event has the structure of a tuple of values which might be numerical or categorical. Since time is of critical importance for CEP, a temporal formalism is used in order to define the patterns to be detected. Such a pattern imposes temporal (and possibly atemporal) constraints on the input events, which, if satisfied, lead to the detection of a complex event. Atemporal constraints may be "local", applying only to the last event read from the input stream. For example, in streams from temperature sensors, the constraint that the temperature of the last event is higher than some constant threshold would constitute such a local constraint. Alternatively, these constraints might involve multiple events of the pattern, e.g., the constraint that the temperature of the last event is higher than that of the previous event. The input to a CER system thus consists of two main components: a stream of events, also called simple derived events (SDEs); and a set of patterns that define relations among the SDEs. Instances of pattern satisfaction are called Complex Events (CEs). The output of the system is another stream, composed of the detected CEs. CEs must often be detected with very low latency, which, in certain cases, may even be in the order of a few milliseconds [2,4,5].
Automata are of particular interest for the field of CER, because they provide a natural way of handling sequences. As a result, the usual operators of regular expressions, concatenation, union and Kleene-star, have often been given an implicit temporal interpretation in CER. For example, the concatenation of two events is said to occur whenever the second event is read by an automaton after the first one, i.e., whenever the timestamp of the second event is greater than the timestamp of the first (assuming the input events are temporally ordered). On the other hand, atemporal constraints are not easy to define using classical automata, since they either work without memory or, even if they do include a memory structure, e.g., as with push-down automata, they can only work with a finite alphabet of input symbols. For this reason, the CER community has proposed several extensions of classical automata. These extended automata have the ability to store input events and later retrieve them in order to evaluate whether a constraint is satisfied [6,7,3]. They resemble both register automata [8], through their ability to store events, and symbolic automata [9], through the use of predicates on their transitions. They differ from symbolic automata in that predicates apply to multiple events, retrieved from the memory structure that holds previous events. They differ from register automata in that predicates may be more complex than that of (in)equality.
One issue with these automata is that their properties have not been systematically investigated, as is the case with models derived directly from the field of languages and automata (see [10] for a discussion about the weaknesses of automaton models in CER). Moreover, they sometimes need to impose restrictions on the use of regular expression operators in a pattern, e.g., nesting of Kleenestar operators is not allowed. A recently proposed formal framework for CER attempts to address these issues [10]. Its advantage is that it provides a logic for CER patterns, with simple denotational and compositional semantics, but without imposing severe restrictions on the use of operators. An automaton model is also proposed which may be conceived as a variation of symbolic transducers [9]. However, this automaton model can only handle "local" constraints, i.e., the formulas on their transitions are unary and thus are applied only to the last event read.
We propose an automaton model that is a combination of symbolic and register automata. It has the ability to store events and its transitions have guards in the form of n-ary conditions. These conditions may be applied both to the last event and to past events that have been stored. Conditions on multiple events are crucial in CER because they allow us to express many patterns of interest, e.g., an increasing trend in the speed of a vehicle. We call such automata Symbolic Register Automata (SRA). SRA extend the expressive power of symbolic and register automata, by allowing for more complex patterns to be defined and detected on a stream of events. We also present a language with which we can define patterns for complex events that can then be translated to SRA. We call such patterns Symbolic Regular Expressions with Memory (SREM ), as an extension of the work presented in [11], where Regular Expression with Memory (REM ) are defined and investigated. REM are extensions of classical regular expressions with which we allow some of the terminal symbols of an expression to be stored and later be compared for (in)equality. SREM allow for more complex conditions to be used, besides those of (in)equality.
We then show how SREM and SRA may be used in order to perform Complex Event Forecasting (CEF). Our solution allows a user to define a pattern for a complex event in the form of a SREM . It then constructs a probabilistic model for such a pattern in order to forecast, on the basis of an event stream, if and when a complex event is expected to occur. We use prediction suffix trees [12,13] to learn a probabilistic model for the pattern and the SRA corresponding to this pattern. We have already presented how symbolic automata without registers may be combined with prediction suffix trees for the purpose of CEF [14]. We show here when and how symbolic automata with memory can be combined with prediction suffix trees for the same purpose. Prediction suffix trees fall under the class of the so-called variable-order Markov models. They are Markov models whose order (how deep into the past they can look for dependencies) can be increased beyond what is computationally possible with full-order models. They can do this by avoiding a full enumeration of every possible dependency and focusing only on "meaningful" dependencies. Efficient and early CEF would thus allow analysts to take proactive action when critical situations are expected to happen, e.g., to alert maritime authorities for the possible collision of vessels at sea.
The contributions of the paper may be summarized as follows: • We present a language for CER, Symbolic Regular Expressions with Memory (SREM ).
• We present a computational model for patterns written in SREM , Symbolic Register Automata (SRA), whose main feature is that it allows for relating multiple events in a pattern. Constraints with multiple events are essential in CER, since they are required in order to capture many patterns of interest, e.g., an increasing or decreasing trend in stock prices. ...
• We show that SRA and SREM are equivalent, i.e., they accept the same set of languages.
• We study the closure properties of SRA (and SREM ). We show that, in the general case, they are closed under the most usual operators (union, intersection, concatenation and Kleene-star), but not under complement and determinization. Failure of closure under complement implies that negation cannot be arbitrarily (i.e., in a compositional manner) used in CER patterns. The negative result about determinization implies that certain techniques requiring deterministic automata, like the ones we will describe later for event forecasting, are not applicable.
• We show that, by using windows, SRA are able to retain their nice closure properties, i.e., they remain closed under complement and determinization. Windows are an indispensable operator in CER because, among others, they limit the search space when attempting to find matches for a pattern.
• We show how SRA with windows can be combined with Prediction Suffix Trees in order to perform CEF, thus extending our previous work from symbolic automata to symbolic register automata [14].
All proofs and complete algorithms may be found in the Appendix, Section 10. Please, note that the results of this paper are presented with CER in mind. However, we need to stress that they are not restricted to CER. They are general results, applicable to any strings and not just to streams of events. In fact, one may treat CER as a special case of string processing. Thus, our contributions lie both in the more specific field of CER and in the more general one of formal languages and automata theory.
Example 1.1. We now introduce an example which will be used throughout the paper to provide intuition (borrowed from [10]). The example is that of a set of sensors taking temperature and humidity measurements, monitoring an area for the possible eruption of fires. A stream is a sequence of input events, where each such event is a tuple of the form (type, id , value). The first attribute (type) is the type of measurement: H for humidity and T for temperature. The second one (id ) is an integer identifier, unique for each sensor. It has a finite set of possible values. Finally, the third one (value) is the real-valued measurement from a possibly infinite set of values. Table 1 shows an example of such a stream. We assume that events are temporally ordered and their order is implicitly provided through the index.
The structure of the paper is as follows. In Section 2 we present the state-of-the-art in automata theory with respect to automaton models that can store elements and models that can use more complex conditions on their transitions than simple equality. In Section 3 we discuss extensively the grammar and the semantics of SREM . Next, in Section 4 we define SRA and the languages that they recognize. In Section 5 we show that SRA and SREM are equivalent. We show that SRA and SREM are closed under union, intersection, concatenation and Kleene-star, but not under complement and determinization. We also define windowed SREM and SRA and show that windows make SRA and SREM closed under complement and determinization. In Section 6, we discuss how SRA can be used for CER, whereas Section 7 briefly discusses some complexity issues. Subsequently, Section 8 discusses how SRA can be given a probabilistic description through the use of variable-order Markov models in order to perform CEF. We conclude with Section 9 where we summarize our contributions and discuss possible avenues for future work.

Related Work
Because of their ability to naturally handle sequences of characters, automata have been extensively adopted in CER, where they are adapted in order to handle streams composed of tuples. Typical cases of CER systems that employ automata are the Chronicle Recognition System [15,16], Cayuga [6], TESLA [17] and SASE [7,18]. There also exist systems that do not employ automata as their computational model, e.g., there are logic-based systems [19] or systems that use trees [20], but the standard operators of concatenation, union and Kleene-star are quite common and they may be considered as a reasonable set of core operators for CER. For an overview of CER languages, see [1], and for a general review of CER systems, see [3].
However, current CER systems do not have the full expressive power of regular expressions, e.g., SASE does not allow for nesting Kleene-star operators. Moreover, due to the various approaches implementing the basic operators and extensions in their own way, there is a lack of a common ground that could act as a basis for systematically understanding the properties of these automaton models. The abundance of different CER systems, employing various computational models and using various formalisms has recently led to some attempts at providing a unifying framework [10,21]. Specifically, in [10], a set of core CER operators is identified, a formal framework is proposed that provides denotational semantics for CER patterns, and a computational model is described for capturing such patterns.
Outside the field of CER, research on automata has evolved towards various directions. Besides the well-known push-down automata that can store elements from a finite set to a stack, there have appeared other automaton models with memory, such as register automata, pebble automata and data automata [8,22,23]. For a review, see [24]. Such models are especially useful when the input alphabet cannot be assumed to be finite, as is often the case with CER. Register automata (initially called finite-memory automata) constitute one of the earliest such proposals [8]. At each transition, a register automaton may choose to store its current input (more precisely, the current input's data payload) to one of a finite set of registers. A transition is followed if the current input is equal with the contents of some register. With register automata, it is possible to recognize strings constructed from an infinite alphabet, through the use of (in)equality comparisons among the data carried by the current input and the data stored in the registers. However, register automata do not always have nice closure properties, e.g., they are not closed under determinization For an extensive study of register automata, see [11,25]. We build on the framework presented in [11,25] in order to construct register automata with the ability to handle "arbitrary" structures, besides those containing only (in)equality relations.
Another model that is of interest for CER is the symbolic automaton, which allows CER patterns to apply constraints on the attributes of events. Automata that have predicates on their transitions were already proposed in [26]. This initial idea has recently been expanded and more fully investigated in symbolic automata [27,28,9]. In this automaton model, transitions are equipped with formulas constructed from a Boolean algebra. A transition is followed if its formula, applied to the current input, evaluates to true. The work presented in [10,29] may also be categorized under this class of "unary" symbolic automata (or transducers, to be more precise). Contrary to register automata, symbolic automata have nice closure properties, but their formulas are unary and thus can only be applied to a single element from the input string.
This is one limitation that we address in this paper. We propose an automaton model, called Symbolic Register Automata (SRA), whose transitions can apply n-ary formulas/conditions (with n>1) on multiple elements. SRA are thus more expressive than symbolic and register automata, thus being suitable for practical CER applications, while, at the same time, their properties can be systematically investigated, as in standard automata theory. In fact, our model subsumes these two automaton models as special cases.
We also show how this new automaton model can be given a probabilistic description in order to perform forecasting, i.e., predict the occurrence of a complex event before it is actually detected by the automaton. However, forecasting has not received much attention in the field of CER, despite the fact that it is an active research topic in various related research areas, such as time-series forecasting [30], sequence prediction [31,12,32,33], temporal mining [34,35,36,37] and event sequence prediction and point-of-interest recommendations through neural networks [38,39]. These methods are powerful in predicting the next numerical value(s) in a time-series or the next input event(s) in a sequence of events, but they suffer from limitations that render them unsuitable for CEF. In CEF we are interested in both numerical and categorical values, related through complex patterns and involving multiple variables. Such patterns require a language to be defined, much like SQL in databases. Our goal is to forecast the occurrence of such complex events defined via patterns and not input events. Input event forecasting is actually not very useful for CER, since the majority of input events are ignored, without contributing to the detection of complex events. The number of complex events is typically orders of magnitude lower than that of input events.
Some conceptual proposals have acknowledged the need for CEF though [40,41,42]. In what follows, we briefly present the relatively few previous concrete attempts at CEF. The first such attempt at CEF was presented in [43], where a variant of regular expressions and automata was used to define complex event patterns, along with Markov chains. Each automaton state was mapped to a Markov chain state. Symbolic automata and Markov chains were again used in [44,45]. The problem with these approaches is that they are essentially unable to encode higher-order dependencies, since highorder Markov chains may lead to a combinatorial explosion of the number of states. In [46], complex events were defined through transitions systems and Hidden Markov Models (HMM) were used to construct a probabilistic model. The observable variable of the HMM corresponded to the states of the transition system. HMMs are in general more powerful than Markov chains, but, in practice, the may be hard to train ( [31,47]) and require elaborate domain modeling, since mapping a pattern to a HMM is not straightforward. In contrast, our approach constructs seamlessly a probabilistic model from a given CE pattern (declaratively defined). Knowledge graphs were used in in [48] to encode events and their timing relationships. Stochastic gradient descent was employed to learn the weights of the graph's edges that determine how important an event is with respect to another target event. However, this approach falls in the category of input event forecasting, as it does not target complex events.

A Grammar for Symbolic Regular Expressions with Memory
Before presenting SRA, we first present a high-level formalism for defining CER patterns. We extend the work presented in [11], where the notion of regular expressions with memory (REM ) was introduced. These regular expressions can store some terminal symbols in order to compare them later against a new input element for (in)equality. One important limitation of REM with respect to CER is that they can handle only (in)equality relations. In this section, we extend REM so as to endow them with the capacity to use relations from "arbitrary" structures. We call these extended REM Symbolic Regular Expressions with Memory (SREM ).
First, in Section 3.1 we repeat some basic definitions from logic theory. We also describe how we can adapt them and simplify them to suit our needs. Next, in Section 3.2 we precisely define the notion of conditions. In SREM , conditions will act in a manner equivalent to that of terminal symbols in classical regular expressions. The difference is of course that conditions are essentially logic formulas that can reference both the current element read from a string/stream and possibly some past elements. Finally, in Section 3.3 we provide a precise definition for SREM and their semantics.

Formulas and Models
In this section, we follow the notation and notions presented in [49]. The first notion that we need is that of a V-structure. A V-structure essentially describes a domain along with the operations that can be performed on the elements of this domain and their interpretation.
A vocabulary V is a set of function, relation and constant symbols. A V-structure is an underlying set U, called a universe, and an interpretation of V. An interpretation assigns an element of U to each constant in V, a function from U n to U to each n-ary function in V and a subset of U n to each n-ary relation in V. We can also define an interpretation of V by assigning each c i to an element of U, e.g., c 1 to (T, 1,22), c 2 to (T, 1, 24), etc. R may also be interpreted as R(x, y) := x.id = y.id , i.e., this binary relation contains all pairs of U which have the same id . For example, ((T, 1,22), (H, 1, 70)) ∈ R and ((T, 1, 22), (T, 2, 33)) / ∈ R. If there are more (even infinite) tuples in a stream/string, then we would also need more constants (even infinite).
We extend the terminology from classical regular expressions to define characters, strings and languages. Elements of U are called characters and finite sequences of characters are called strings. A set of strings L constructed from elements of U (L ⊆ U * , where * denotes Kleene-star) is called a language over U. We can also define streams as follows. A stream S is an infinite sequence S = t 1 , t 2 , · · · , where each t i is a character (t i ∈ U). By S 1..k we denote the sub-string of S composed of the first k elements of S. S m..k denotes the slice of S starting from the m th and ending at the k th element.
We now define the syntax and semantics of formulas that can be constructed from the constants, relations and functions of a V-structure. We begin with the definition of terms.

Definition 3.3. (Term [49])
A term is defined inductively as follows: • Every constant is a term.
• If f is an m-ary function and t 1 , · · · , t m are terms, then f (t 1 , · · · , t m ) is also a term.
Using terms, relations and the usual Boolean constructs of conjunction, disjunction and negation, we can define formulas. Definition 3.4. (Formula [49]) Let t i be terms. A formula is defined as follows: • If P is an n-ary relation, then P (t 1 , · · · , t n ) is a formula (an atomic formula).
• If φ is a formula, ¬φ is also a formula.
• If φ 1 and φ 2 are formulas, φ 1 ∨ φ 2 is also a formula. Definition 3.5. (V-formula [49]) If V is a vocabulary, then a formula in which every function, relation and constant is in V is called a V-formula. Notice that in typical definitions of terms and formulas (as found in [49]) variables are also present. A variable is also a term. Variables are also used in existential and universal quantifiers to construct formulas. In our case, we will not be using variables in the above sense (instead, as explained below, we will use variables to refer to registers). Thus, existential and universal formulas will not be used. In principle, they could be used, but their use would be counter-intuitive. At every new event, we need to check whether this event satisfies some properties, possibly in relation to previous events. A universal or existential formula would need to check every event (variables would refer to events), both past and future, to see if all of them or at least one of them (from the universe U) satisfy a given property. Since we will not be using variables, there is also no notion of free variables in formulas (variables occurring in formulas that are not quantified). Thus, every formula is also a sentence, since sentences are formulas without free variables. In what follows, we will thus not differentiate between formulas and sentences.
We can now define the semantics of a formula with respect to a V-structure.
Let M be a V-structure and φ a V-formula. We define M |= φ (M models φ) as follows: • If φ is atomic, i.e. φ = P (t 1 , · · · , t m ), then M |= P (t 1 , · · · , t m ) iff the tuple (a 1 , · · · , a m ) is in the subset of U m assigned to P , where a i are the elements of U assigned to the terms t i .

Conditions
Based on the above definitions, we will now define conditions over registers. These will essentially be the n-ary guards on the transitions of SRA.

Definition 3.9. (Condition)
Let M be a V-structure always equipped with the unary relation for which it holds that u ∈ , ∀u ∈ U, i.e., this relation holds for all elements of the universe U. Let R = {r 1 , · · · , r k } be variables denoting the registers and ∼ a special variable denoting an automaton's head which reads new elements. The "contents" of the head always correspond to the most recent element. We call them register variables. A condition is essentially a V-formula, as defined above (Definition 3.4), where, instead of terms, we use register variables. A condition is defined by the following grammar: • is a condition.
• ¬φ is a condition, if φ is a condition.
Since terms now refer to registers, we need a way to access the contents of these registers. We will assume that each register has the capacity to store exactly one element from U. The notion of valuations provides us with a way to access the contents of registers.

Definition 3.10. (Valuation)
A valuation on R = {r 1 , · · · , r k } is a partial function v : R → U. The set of all valuations on R is denoted by F (r 1 , · · · , r k ). v[r i ← u] denotes the valuation where we replace the content of r i with a new element u: where W ⊆ R, denotes the valuation obtained by replacing the contents of all registers in W with u. We say that a valuation v is compatible with a condition φ if, for every register variable r i that appears in φ, v(r i ) is defined.
A valuation v is essentially a function with which we can retrieve the contents of any register. We will also use the notation v(r i ) = to denote the fact that register r i is empty, i.e., we extend the range of v to U ∪ { }. We also extend the domain of v to R ∪ {∼}. By v(∼) we will denote the "contents" of the automaton's head, i.e., the last element read from the string. We can now define the semantics of conditions, similarly to the way we defined models of Vformulas in Definition 3.7. The difference is that the arguments to relations are no longer elements assigned to terms but elements stored in registers, as retrieved by a given valuation.

Definition 3.11. (Semantics of conditions)
Let M be a V-structure, u ∈ U an element of the universe of M and v ∈ F (r 1 , · · · , r k ) a valuation. We say that a condition φ is satisfied by (u, v), denoted by (u, v) |= φ, iff one of the following holds: • φ := , i.e., (u, v) |= for every element and valuation.

Symbolic Regular Expressions with Memory
We are now in a position to define Symbolic Regular Expressions with Memory SREM . We achieve this by combining conditions via the standard regular operators. Conditions act as terminal "symbols", as the base case from which we construct more complex expressions. Definition 3.12. (Symbolic regular expression with memory (SREM )) A symbolic regular expression with memory over a V-structure M and a set of register variables R = {r 1 , · · · , r k } is inductively defined as follows: 1. and ∅ are SREM .
2. If φ is a condition (as in Definition 3.9), then φ is a SREM .
3. If φ is a condition, then φ ↓ r i is a SREM . This is the case where we need to store the current element read from the automaton's head to register r i . 4. If e 1 and e 2 are SREM , then e 1 + e 2 is also a SREM . This corresponds to disjunction.
5. If e 1 and e 2 are SREM , then e 1 · e 2 is also a SREM . This corresponds to concatenation.
6. If e is a SREM , then e * is also a SREM . This corresponds to Kleene-star.
In order to define the semantics of SREM , we need to define precisely how the contents of the registers may change. We thus need to define how a SREM , starting from a given valuation v and reading a given string S, reaches another valuation v . Let e be a SREM over a V-structure M and a set of register variables R = {r 1 , · · · , r k }, S a string constructed from elements of the universe of M and v, v ∈ F (r 1 , · · · , r k ). We define the relation (e, S, v) v as follows (a textual explanation is provided after the formal definition): In the first case, we have an SREM . It may reach another valuation only if it reads an string and this new valuation is the same as the initial one, i.e., the registers do not change. In the second case where we have a condition φ = , we move to a new valuation only if the condition is satisfied with the current element and the given register contents. Again, the registers do not change. The third case is similar to the second, with the important difference that the register r i needs to change and to store the current element. For the fourth case (concatenation), we need to be able to break the initial string into two sub-strings such that the first one reaches a certain valuation and the second one can start from this new valuation and reach another one. The fifth case is a disjunction. Finally, the sixth case implies that we must be able to break the initial string into multiple sub-strings such that each one of these substring can reach a valuation and the next one can start from this valuation and reach another one.
Based on the above definition, we may now define the language that a SREM accepts (as in [11]). The language of a SREM contains all the strings with which we can reach a valuation, starting from the empty valuation, where all registers are empty.
where we assume that a) TypeIsT (x) := x.type = T , b) TypeIsH (x) := x.type = H and c) EqualId (x, y) := x.id = y.id . If we feed the string/stream of Table 1 to e 1 , then we will have the following. We will initially read the first element (T, 1,22). Since its type is T , we will move on and store (T, 1, 22) to register r 1 , i.e., we will move from the empty valuation where v(r 1 ) = to v , where v (r 1 ) = (T, 1,22). Then, the sub-expression ( ) * lets us skip any number of elements. We can thus skip the second and third elements without changing the register contents. Now, upon reading the fourth element (H, 1, 70), there are two options. Either skip it again to read the fifth element or try to move on by checking the sub-expression (TypeIsH (∼) ∧ EqualId (∼, r 1 )). This condition is actually satisfied, since the type of this element is indeed H and its id is equal to the id of the element store in r 1 . Thus, S 1..4 is indeed accepted by e 1 . With a similar reasoning we can see that the same is also true for S 1..5 .

Symbolic Register Automata
In order to capture SREM , we propose Symbolic Register Automata (SRA), an automaton model equipped with memory and logical conditions on its transitions. The basic idea is the following. We add a set of registers R to an automaton in order to be able to store elements from the string/stream that will be used later in n-ary conditions. Each register can store at most one element. In order to evaluate whether to follow a transition or not, each transition is equipped with a guard, in the form of a condition. If the condition evaluates to true, then the transition is followed. Since a condition might be n-ary, with n>1, the values passed to its arguments during evaluation may be either the current element or the contents of some registers, i.e., some past elements. In other words, the transition is also equipped with a register selection, i.e., a tuple of registers. Before evaluation, the automaton reads the contents of those registers, passes them as arguments to the condition and the condition is evaluated. Additionally, if, during a run of the automaton, a transition is followed, then the transition has the option to write the element that triggered it to some of the automaton's registers. These are called its write registers, i.e., the registers whose contents may be changed by the transition. We also Figure 1: SRA corresponding to Expression (2).
allow for -transitions, as in classical automata, i.e., transitions that are followed without consuming any elements and without altering the contents of the registers.
We now formally define SRA. To aid understanding, we present three separate definitions: one for the automaton itself, one for its configurations and one for its runs. • q s ∈ Q the start state, • Q f ⊆ Q the set of final states, • R = (r 1 , · · · , r k ) a finite set of registers and • ∆ the set of transitions.
A transition δ ∈ ∆ is a tuple (q, φ, W, q ), also written as q, φ ↓ W → q , where • q, q ∈ Q, • φ is a condition, as defined in Definition 3.9 or φ = and • W ∈ 2 R are the write registers.
We will use the dot notation to refer to elements of tuples. For example, if A is a SRA, then A.Q is the set of its states. For a transition δ, we will also use the notation δ.source and δ.target to refer to its source and target states respectively. Example 4.2. As an example, consider the SRA of Figure 1. Each transition is represented as φ ↓ W , where φ is its condition and W its set of write registers (or simply r i if only a single register is written). W may also be an empty set, implying that no register is written. In this case, we avoid writing W on the transition (see, for example, the transition from q 1 to q f in Figure 1). The definitions for the conditions of the transitions are presented in a separate box, above the SRA. Note that the arguments of the conditions correspond to registers, through the register selection. Take the transition from q s to q 1 as an example. It takes the last event consumed from the stream (∼) and passes it as argument to the unary formula φ 1 . If φ 1 evaluates to true, it writes this last event to register r 1 , displayed as a dashed square in Figure 1. On the other hand, the transition from q 1 to q f uses both the current event and the event stored in r 1 ((∼, r 1 )) and passes them to the binary formula φ 2 . The condition (in the self-loop of q 1 ) is a unary condition that always evaluates to true and allows us to skip any number of events. The SRA of Figure 1 captures SREM (2).
We can describe formally the rules for the behavior of a SRA through the notion of configuration: • j is the index of the next event/character to be consumed, • q is the current state of A and • v the current valuation, i.e., the current contents of A's registers.
We say that c = [j , q , v ] is a successor of c iff one of the following holds: , if this is an transition, we move to the target state without changing the index or the registers' contents.
, if the condition is satisfied according to the current event and the registers' contents and there are no write registers, we move to the target state, we increase the index by 1 and we leave the registers untouched.
if the condition is satisfied according to the current event and the registers' contents and there are write registers, we move to the target state, we increase the index by 1 and we replace the contents of all write registers (all r i ∈ W ) with the current element from the string.
We denote a succession by if we need to refer to the transition as well. For the initial configuration, before any elements have been consumed, we assume that j = 1, q = q s and v(r i ) = , ∀r i ∈ R. In order to move to a successor configuration, we need a transition whose condition evaluates to true, when applied to ∼, if it is unary, or to ∼ and the contents of its register selection, if it is n-ary. If this is the case, we move one position ahead in the stream and update the contents of this transition's write registers, if any, with the event that was read. If the transition is an -transition, we do not move the stream pointer and do not update the registers, but only move to the next state.
The actual behavior of a SRA upon reading a stream is captured by the notion of the run: Definition 4.4. (Run of SRA over string/stream) A run of a SRA A over a stream S = t 1 , · · · , t n is a sequence of successor configurations [1, (e) Configuration after reading t 4 . Figure 2: A run of the SRA of Figure 1, while consuming the first four events from the stream of Table 1. Triggered transitions are shown in red and the current state of the SRA in dark gray. The dashed box represents a register. The contents of the register at each configuration are shown inside the dashed box. Inside the dotted boxes, the run is shown.
Example 4.5. A run of the SRA of Figure 1, while consuming the first four events from the stream of Table 1, is the following: Transition subscripts in this example refer to states of the SRA, e.g., δ s,s is the transition from the start state to itself, δ s,1 is the transition from the start state to q 1 , etc. See also Figure 2. Run (3) is not the only run, since the SRA could have followed other transitions with the same input, e.g., moving directly from q s to q 1 . Another possible (and non-accepting) run would be the one where the SRA always remains in q 1 after its first transition.
Finally, we can define the language of a SRA as the set of strings for which the SRA has an accepting run, starting from an empty configuration.

Definition 4.6. (Language recognized by SRA)
We say that a SRA A accepts a string S iff there exists an accepting run = [1, The set of all strings accepted by A is called the language recognized by A and is denoted by L(A).

Properties of Symbolic Register Automata
We now study the properties of SRA. First, we prove the equivalence of SRA and SREM . We then show that SRA and SREM are closed under union, intersection, concatenation and Kleene-start but not under complement and determinization. We can thus construct SREM and SRA by using arbitrarily (in whatever order and depth is required) the four basic operators of union, intersection, concatenation and Kleene-star. However, the negative result about complement suggests that the use of negation in CER patterns cannot be equally arbitrary. Moreover, deterministic SRA cannot be used in cases where this might be required, as in CEF. We will discuss in Section 8 why determinization is important for CEF. If, however, we use an extra window operator, effectively limiting the length of strings accepted by a SRA, we can then show that closure under complement and determinization is also possible.

Equivalence of SREM and SRA
We first prove that, for every SREM there exists an equivalent SRA. The proof is constructive, similar to that for classical automata. For the inverse direction, i.e. converting a SRA to an equivalent SREM , we use the notion of generalized SRA. These are SRA which have complete SREM on their transitions. By incrementally removing states from the SRA, we are finally left with two states and the SREM which connects them is the SREM we are looking for.
We now show how, for each SREM we can construct an equivalent SRA. Equivalence between an expression e and a SRA A means that they recognize the same language, i.e., L(e) = L(A). See Definitions 3.14 and 4.6.

Proof:
The complete SRA construction process and proof may be found in Appendix 10.1.
Example 5.2. Here, we present an example, to give the intuition. Let With this expression, we want to monitor sensors for possible failures. We want to detect cases where a sensor records temperatures outside some range of values (first line of SREM (4)) and continues to transmit measurements (second line), so that we are alerted to the fact that new measurements might not be trustworthy. The last condition is a binary formula, applied to both ∼ and r 1 . Figure 3 shows the process for constructing the SRA which is equivalent to SREM (4). The algorithm is compositional, starting from the base cases e:=φ or e:=φ ↓ W . The three regular expression operators (concatenation, disjunction, Kleene-star) are handled in a manner almost identical as for classical automata. The subtlety here concerns the handling of registers. The simplest solution is to gather from the very start all registers mentioned in any sub-expressions of the original SREM e, i.e. any registers in the register selection of any transitions and any write registers. We first create those registers and then start the construction of the sub-automata. Note that some registers may be mentioned in multiple sub-expressions (e.g., in one that writes to it and then in one that reads its contents). We only add such registers once. We treat the registers as a set with no repetitions.
For the example of Figure 3, only one register is mentioned, r 1 . We start by creating this register. Then, we move on to the terminal sub-expressions. There are three basic sub-expressions and three basic automata are constructed: from q s,1 to q f,1 , from q s,2 to q f,2 and from q s,3 to q f,3 . See Figure 3a. To the first two transitions, we add the relevant unary conditions, e.g., we add To the third transition, we add the relevant binary condition φ 3 (x, y) := (x.type = T ∧ x.id = y.id ). The + operator is handled by joining the SRA of the disjuncts through new states and -transitions. See Figure 3b. The concatenation operator is handled by connecting the SRA of its sub-expressions through an -transition, without adding any new states. See Figure 3c. Iteration, not applicable in this example, is handled by joining the final state of the original automaton to its start state through an -transition.
We can also prove the inverse theorem, i.e., that every SRA can be converted to a SREM . To do so, however, we will need two lemmas. The first is the standard lemma about elimination, stating that we can always eliminate all transitions from a SRA to get an equivalent SRA with no transitions. The next lemma that we will require concerns the ability of SRA to write to multiple registers at the same time. The write registers of a transition δ in Definition 4.1, δ.W , might not be a singleton. On the other hand, according to Definition 3.12, each terminal sub-expression in a SREM may write to at most one register. We can prove though that being able to write to multiple registers at the same time does not add any expressive power to SRA. Every SRA which can write to multiple registers can be converted to a SRA whose transitions can write to at most one register.
, if there exists a transition that can write to multiple registers. A SRA A is called a single-register SRA if for all transitions δ ∈ A.∆ it holds that |δ.W | ≤ 1, i.e., if each transition can write to at most one register. We are now in a position to prove that every SRA can be converted to a SREM .

Closure Properties of SREM/SRA
We now study the closure properties of SRA under union, intersection, concatenation, Kleene-star, complement and determinization. We first provide the definition for deterministic SRA. Informally, a SRA is said to be deterministic if, at any time, with the same input event, it can follow no more than one transition. The formal definition is as follows: In other words, from all the outgoing transitions from a given state q at most one of them can be triggered on any element u and valuation/register contents v. By definition, for a deterministic SRA, at most one run may exist for every string/stream.
We now give the definition for closure under union, intersection, concatenation, Kleene-star, complement and determinization: We say that SRA are closed under: i.e., a string S is accepted by A iff it is accepted either by A 1 or by A 2 .
• intersection if, for every SRA A 1 and A 2 , there exists a SRA A such that L(A) = L(A 1 ) ∩ L(A 2 ), i.e., a string S is accepted by A iff it is accepted by both A 1 and A 2 .
• concatenation if, for every SRA A 1 and A 2 , there exists a SRA A such that L(A) = L(A 1 ) · L(A 2 ), i.e., S is accepted by A iff it can be broken into two sub-strings S = S 1 · S 2 such that S 1 is accepted by A 1 and S 2 by A 2 .
• Kleene-star if, for every SRA A, there exists a SRA A * such that L(A * ) = (L(A)) * , where L * = i≥0 L i , i.e., S is accepted by A * iff it can be broken into S = S 1 · S 2 · · · · such that each S i is accepted by A.
• complement if, for every SRA A, there exists a SRA A c such that for every string S it holds that S ∈ L(A) ⇔ S / ∈ L(A c ).
• determinization if, for every SRA A, there exists a dSRA A D such that L(A) = L(A d ).
We thus have the following for union, intersection, concatenation and Kleene-star: Theorem 5.9. SRA and SREM are closed under union, intersection, concatenation and Kleene-star.
Proof: See Appendix 10.5 for complete proofs. For union, concatenation and Kleene-star the proof is essentially the proof for converting SREM to SRA (and we have already proven that SRA and SREM are equivalent). For intersection, we construct a new SRA can thus be constructed from four basic operators (union, intersection, concatenation and Kleene-star) in a compositional manner, providing substantial flexibility and expressive power for CER applications. However, as is the case for register automata [8], SRA are not closed under complement, something which could pose difficulties for handling negation, i.e., the ability to state that a sub-pattern should not happen for the whole pattern to be detected.
SRA are also not closed under determinization, a result which might seem discouraging. In the next section, we show that there exists a sub-class of SREM for which a translation to deterministic SRA is indeed possible. This is achieved if we apply a windowing operator and limit the length of strings accepted by SREM and SRA.

Windowed SREM/SRA
We can overcome the negative results about complement and determinization by using windows in SREM and SRA. In general, CER systems are not expected to remember every past event of a stream and produce matches involving events that are very distant. On the contrary, it is usually the case that CER patterns include an operator that limits the search space of input events, through the notion of windowing. This observation motivates the introduction of windowing in SREM .
Let e be a SREM over a V-structure M and a set of register variables R = {r 1 , · · · , r k }, S a string constructed from elements of the universe of M and v, v ∈ F (r 1 , · · · , r k ). A windowed SREM (wSREM ) is an expression of the form e := e [1..w] , where w ∈ N 1 . We define the relation (e , S, v) v as follows: (e, S, v) v and |S| ≤ w.
The windowing operator does not add any expressive power to SREM . We could use the index of an event in the stream as an event attribute and then add binary conditions in an expression which ensure that the difference between the index of the last event read and the first is no greater that w. It is more convenient, however, to have an explicit operator for windowing.
We first show how we can construct a so-called "unrolled SRA" from a windowed expression: Lemma 5.13. For every windowed SREM there exists an equivalent unrolled SRA without any loops, i.e., a SRA where each state may be visited at most once.

Proof:
The full proof and the complete construction algorithm are presented in Appendix 10.9.
.w] Output: Deterministic SRA A e equivalent to e 1 A e, ← ConstructSRA(e); 2 A e ← EliminateEpsilon(A e, ); 3 enumerate all walks of A e of length up to w; // Now unroll Ae. 4 join walks through disjunction; 5 collapse common prefixes; Example 5.14. Here, we provide only the general outline of the algorithm and an example. Consider, e.g., the following SREM : It can skip any number of events with the first sub-expression ( ) * . Then it expects to find an event with type T and stores it to register r 1 (sub-expression TypeIsT (∼) ↓ r 1 ). The third sub-expression is again ( ) * , meaning that, after seeing a T event, we are allowed to skip events. Finally, with the last sub-expression (TypeIsH (∼) ∧ EqualId (∼, r 1 )), if some event after the T event is of type H and they have the same identifier, then the string is accepted, provided that its length is also at most w. Figure 4b shows the steps taken for constructing the equivalent unrolled SRA for this expression. A simplified version of the unrolling algorithm is shown in Algorithm 1.
The construction algorithm first produces a SRA as usual, without taking the window operator into account (see line 1 of Algorithm 1). For our example, the result would be the SRA of Figure  4a (please, note that the automaton of Figure 4a is slightly different than that of Figure 1 due to the presence of the first ( ) * sub-expression). Then the algorithm eliminates any -transitions (line 2). The next step is to use this SRA in order to create the equivalent unrolled SRA (uSRA). The rationale behind this step is that the window constraint essentially imposes an upper bound on the number of registers that would be required for a deterministic SRA. For our example, if w=3, then we know that we will need at least one register, if a T event is immediately followed by an H event. We will also need at most two registers, if two consecutive T events appear before an H event. The function of the uSRA is to create the number of registers that will be needed, through traversing the original SRA. Algorithm 1 does this by enumerating all the walks of length up to w on the SRA graph, by unrolling any cycles. Lines 3 -5 of Algorithm 1 show this process in a simplified manner. The uSRA for our example is shown in Figure 4b for w=3. The actual algorithm does not perform an exhaustive enumeration, but incrementally creates the uSRA, by using the initial SRA as a generator of walks. Every time we expand a walk, we add a new transition, a new state and possibly a new register, as clones of the original transition, state and register. In our example, we start by creating a clone of q s in Figure 4a, also named q s in Figure 4b. From the start state of the initial SRA we have two options. Either loop in q s through the transition or move to q 1 through the transition with the φ 1 condition. We can thus expand q s of the uSRA with two new transitions: from q s to q t and from q s to q 1 in Figure  4b. We keep expanding the SRA this way until we reach final states and without exceeding w. As a result, the final uSRA has the form of a tree, whose walks and runs are of length up to w.
A uSRA then allows us to capture windowed expressions. Note though that the algorithm we presented above, due to the unrolling operation, can result in a combinatorial explosion of the number of states of the dSRA, especially for large values of w. Its purpose here was mainly to establish Lemma 5.13.
Having a uSRA makes it easy to subsequently construct a dSRA: Theorem 5.15. For every windowed SREM there exists an equivalent deterministic SRA.

Proof:
The proof for determinization is presented in Appendix 10.10. It is constructive and the determinization algorithm is based on the powerset construction of the states of the non-deterministic SRA. It is similar to the algorithm for symbolic automata [27,9]. It does not add or remove any registers. It initially constructs the powerset of the states of the uSRA. The members of this powerset will be the states of the dSRA. It then tries to make each such new state, say q d , deterministic, by creating transitions with mutually exclusive conditions when they have the same output. The construction of these mutually exclusive conditions is done by gathering the conditions of all the transitions that have as their source a member of q d . Out of these conditions, the set of minterms is created, i.e., the mutually (5) after unrolling cycles, for w = 3 (whole SRA, black and light gray states) and w = 2 (top 3 states in black).  exclusive conjuncts constructed from the initial conditions, where each conjunct is a condition in its original or its negated form. A transition is then created for each minterm, with q d being the source. Then, only one transition can be triggered, since these minterms are mutually exclusive.
Example 5.16. As an example, Figure 4c shows the result of converting the uSRA of Figure 4b to a dSRA. We have simplified somewhat the conditions of each transition due to the presence of the predicates in some of them. For example, the minterm φ 1 ∧¬ for the start state is unsatisfiable and can be ignored while φ 1 ∧ may be simplified to φ 1 . The figure shows only part of the dSRA to avoid clutter. Note that some of the rightmost states may be further expanded. For example, state {q t,1 , q 1,t } (top right) can be expanded. With the minterm φ 2 (∼, r 1 ) ∧ ¬φ 2 (∼, r 2 ), it would go to the final state {q 1,t,2 } (not shown in the figure).
Being able to derive a deterministic SRA is important for Complex Event Forecasting (CEF), since, as we will show, determinization is an important intermediate step in this task. A deterministic SRA essentially provides us with the "symbols" with which we populate a prediction suffix tree, the structure that captures the statistical properties of an input event stream.
We may now prove, as a corollary, that windowed SRA are also closed under complement: Proof: See Appendix 10.11.

Streaming SRA for Complex Event Recognition
We have thus far described how SREM and SRA can be applied to bounded strings that are known in their totality before recognition. A string is given to a SRA and an answer is expected about whether the whole string belongs to the automaton's language or not. However, in CER/F we are required to handle continuously updated streams of events and detect instances of SREM satisfaction as soon as they appear in a stream. For example, the automaton of the classical regular expression a · b would accept only the string a, b. In a streaming setting, we would like the automaton to report a match every time this string appears in a stream. For the stream a, b, c, a, b, c, we would thus expect two matches to be reported, one after the second symbol and one after the fifth (assuming that we are interested only in contiguous matches). Slight modifications are required so that SREM and SRA may work in a streaming setting (the discussion in this section develops along the lines presented in our previous work [14], with the difference that here we are concerned with symbolic automata with memory). First, we need to make sure that the automaton can start its recognition after every new element. If we have a classical regular expression R, we can achieve this by applying on the stream the expression Σ * · R, where Σ is the automaton's (classical) alphabet. For example, if we apply R := {a, b, c} * · (a · b) on the stream a, b, c, a, b, c, the corresponding automaton would indeed reach its final state after reading the second and the fifth symbols. In our case, events come in the form of tuples with both numerical and categorical values. Using database systems terminology we can speak of tuples from relations of a database schema [10]. These tuples constitute the universe U of a V-structure M. A stream S then has the form of an infinite sequence S = t 1 , t 2 , · · · , where t i ∈ U. Our goal is to report the indices i at which a complex event is detected.
More precisely, if S 1..k = · · · , t k−1 , t k is the prefix of S up to the index k, we say that an instance of a SREM e is detected at k iff there exists a suffix S m..k of S 1..k such that S m..k ∈ L(e). In order to detect complex events of a SREM e on a stream, we use a streaming version of SREM and SRA. Using e s = * · e we can detect complex events of e while reading a stream S, since a stream segment S m..k belongs to the language of e iff the prefix S 1..k belongs to the language of e s . The prefix * lets us skip any number of events from the stream and start recognition at any index m, 1 ≤ m ≤ k.
Proposition 6.2. If S = t 1 , t 2 , · · · is a stream of elements from a universe U of a V-structure M, where t i ∈ U and e is a SREM over M, then, for every S m..k , S m..k ∈ L(e) iff S 1..k ∈ L(e s ) (and S 1..k ∈ L(A es )).
Note that sSREM and sSRA are just special cases of SREM and SRA respectively. Therefore, every result that holds for SREM and SRA also holds for sSREM and sSRA as well.

Notes on Complexity
In the theory of formal languages it is customary to present complexity results for various decision problems, most commonly for the problem of non-emptiness (whether an expression or automaton accepts at least one string), that of membership (deciding whether a given string belongs to the language of an expression/automaton) and that of universality (deciding whether a given expression/automaton accepts every possible string). We briefly discuss here these problems for the case of SREM and SRA.
The complexity of these problems for SREM and SRA depends heavily on the nature of the conditions used as terminal expressions in SREM and as transition guards in SRA, e.g., the EqualId (∼, r 1 ) condition in SREM (5). This, in turn, depends on the complexity of deciding whether a given element from the universe U of a V-structure M belongs to a relation R from M. Since we have not imposed until now any restrictions on such relations, the complexity of the aforementioned decision problems can be "arbitrarily" high and thus we cannot provide specific bounds. If, for example, the problem of evaluating a relation R is NP-complete and this relation is used in a SREM /SRA condition, this then implies that the problem of membership immediately becomes at least NP-complete. In fact, if the problem of deciding whether an element from U belongs to a relation R is undecidable, then the membership problem becomes also undecidable.
We can, however, provide some rough bounds by looking at the complexity of these problems for the case of register automata (see [11]). Register automata are a special case of SRA, where the only allowed relations are the binary relations of equality and inequality. We assume that these relations may be evaluated in constant time. For the problem of universality, we know that it is undecidable for register automata. We can thus infer that it remains so for SRA as well. On the other hand, the problem of non-emptiness is decidable but PSPACE-complete. The same problem for SRA is thus PSPACE-complete. Finally, the problem of membership is NP-complete. Therefore, it is also at least NP-complete for SRA. Note that membership is the most important problem for the purposes of CER/F, since in CER/F we continuously try to check whether a string (a suffix of the input stream) belongs to the language of a pattern's automaton. In general, if we assume that the problem of membership in all relations R is decidable in constant time, then the complexity of the decision problems for SRA coincides with that for register automata.
If we focus our attention even further on windowed SRA, as is the case in CER/F, then we can estimate more precisely the complexity of processing a single event from a stream. This is the most important operation for CER/F. A windowed SRA can first be determinized (offline) to obtain a dSRA. Assume that the resulting dSRA A has k registers and c conditions/minterms. We also assume that evaluating a condition requires constant time and that accessing a register also takes constant time. In the worst case, after a new element/event arrives, we need to evaluate all of the conditions/minterms on the c outgoing transitions of the current state to determine which one of them is triggered. We may also need to access all of the k registers in order to evaluate the conditions. Therefore, the complexity of updating the state of the dSRA A is O(c + k) (assuming that each register is accessed only once and its contents are provided to every condition which references that register).

Complex Event Forecasting with Markov Models
We now show how we can use the framework of SREM and SRA to perform Complex Event Forecasting (CEF). The main idea behind our forecasting method is the following: Given a pattern e in the form of a SREM , we first construct an automaton. In order to perform event forecasting, we translate the SRA to an equivalent deterministic SRA. This dSRA can then be used to learn a probabilistic model, typically a Markov model, that encodes dependencies among the events in an input stream. Note that deterministic SRA are important because they allow us, as we will show, to produce a stream of "symbols" from the initial stream of events. By using deterministic SRA, we can map each input event to a single symbol and then use this derived stream of symbols to learn a Markov model. With non-deterministic SRA each element/event from the string/stream may trigger multiple transitions and thus such a mapping is not possible. The probabilistic model is learned from a portion of the input stream which acts as a training dataset and it is then used to derive forecasts about the expected occurrence of the complex event encoded by the automaton. After learning a model, we need to estimate the so-called waiting-time distributions for each state of our automaton. These distributions let us know the probability of reaching a final state from any other automaton state in k events from now. These distributions are then used to estimate forecasts, which generally have the form of an interval within which a complex event has a high probability of occurring.
We discern three cases and present them in order of increasing complexity: • We have only unary conditions applied to the last event and an arbitrary (finite or infinite) universe. In this case, we do not need registers.
• We have n-ary conditions (with n ≥ 1) and a finite universe. In this case, registers are helpful, but may not be necessary. If we have a register automaton A and a finite universe U, we can always create an automaton A U with states A.Q × U and appropriate transitions so that A U is equivalent to A but has no registers. Its states can implicitly remember past elements.
• The most complex case is when we have n-ary conditions and an infinite universe, as is typically assumed in CER/F. Registers are necessary in this case.

SREM with unary conditions
As a first step, we assume that the given SREM contains only unary conditions. The universe in this case may be either finite or infinite. We have already presented how this case can be handled in our previous work [14]. We will present here only a high-level overview of our method and then discuss how it can be adjusted in order to accommodate the other two cases. Before discussing how a dSRA can be described by a Markov model, we first discuss a useful result, which bears on the importance of being able to use deterministic automata. It can be shown that a dSRA always has an equivalent deterministic classical automaton, through a simple isomorphic mapping, retaining the exact same structure for the automaton and simply changing the conditions on the transitions with symbols [50]. This result is important for two reasons: a) it allows us to use methods developed for classical automata without having to always prove that they are indeed applicable to symbolic automata as well, and b) it will help us in simplifying our notation, since we can use the standard notation of symbols instead of predicates. This result implies that, for every run followed by a dSRA A s by consuming a symbolic string (or stream of events) S, the run that the equivalent classical automaton A c follows by consuming the induced string S is also = [1, A c follows the same copied/renamed states and the same copied/relabeled transitions. We can then use symbols and strings (lowercase letters to denote symbols), as in classical theories of automata, bearing in mind that, in our case, each symbol always corresponds to a condition. Details may be found in [14].
This equivalent deterministic classical automaton can be used to convert a string/stream of elements/events to a string/stream of symbols. Since each element may trigger only a single transition, the initial string of elements may be mapped to a string of symbols. Each transition δ i from the initial run corresponds to a transition δ i from run . Since each transition from corresponds to a single symbol, we can map the whole stream of input events to a single string of symbols. This means that we can use techniques developed in the context of deterministic classical automata and apply them to our case. One such class of techniques concerns the question of how we can build a probabilistic model that captures the statistical properties of the streams to be processed by an automaton. Such a model would allow us to make inferences about the automaton's expected behavior as it reads event streams.
We have proposed the use of a variable-order Markov model (VMM) [31,12,13,32,33]. Compared to fixed-order Markov models, VMMs allow us to increase their order m (how many events they can remember) to higher values and thus capture longer-term dependencies, which can lead to a better accuracy.
The idea behind VMMs is the following: let Σ denote an alphabet, σ ∈ Σ a symbol from that alphabet and s ∈ Σ m a string of length m of symbols from that alphabet. The aim is to derive a predictorP from the training data such that the average log-loss on a test sequence S 1..k is minimized. The loss is given by l(P , S 1.
. Minimizing the log-loss is equivalent to maximizing the likelihoodP (S 1. . The average log-loss may also be viewed as a measure of the average compression rate achieved on the test sequence [31]. The mean (or expected) log-loss (−E P {logP (S 1..k )}) is minimized if the derived predictorP is indeed the actual distribution P of the source emitting sequences.
For fixed-order Markov models, the predictorP is derived through the estimation of conditional distributionsP (σ | s), with m constant and equal to the assumed order of the Markov model (σ is a single symbol and s a string of length m). VMMs, on the other hand, relax the assumption of m being fixed. The length of the "context" s may vary, up to a maximum order m, according to the statistics of the training dataset. By looking deeper into the past only when it is statistically meaningful, VMMs can capture both short-and long-term dependencies.
We use Prediction Suffix Trees (PST ), as described in [12,13], as our VMM of choice. Assuming that we have derived an initial predictorP (by scanning the training dataset and estimating various empirical conditional probabilities), the learning algorithm in [12] starts with a tree having only a single node, corresponding to the empty string . Then, it decides whether to add a new context/node s by checking whether it is "meaningful enough" to expand to s. This is achieved by checking whether there exists a significant difference between the conditional probability of a symbol σ given s and the same probability given the shorter context suffix (s) (suffix (s) is the longest suffix of s different than s). A detailed description of how we use PST to perform forecasting may be found in [14].
Our goal is to use the PST in order to to calculate the so-called waiting-time distribution for every state q of the automaton A. The waiting-time distribution is the distribution of the index n, given by the waiting-time variable Q\A.Q f for i = n and Y n ∈ A.Q f . Thus, waiting-time distributions give us the probability to reach a final state from a given state q in n transitions from now. Example 8.1. We provide here the intuition through an example. Figure 5a shows an example of a deterministic automaton. Note that we use symbols on the transitions, which, as explained, essentially correspond to conditions. Figure 5b shows a PST which could be constructed from the automaton of Figure 5a and a given training dataset, with m = 3. This PST is read as follows. Consider its left-most node, aa, (0.75, 0.25). This means that the probability of encountering an a symbol, given that the last two symbols are aa, is 0.75. The probability of seeing b, on the other hand, is 0.25. The order of this node is 2. It has not been further expanded to yet another deeper level, because it was estimated that such an expansion would be statistically insignificant. For example, the probability P (a | baa) might still be very close to 0.75 (e.g., 0.747). If the same is true for P (a | aaa), then this means that the probability of seeing a is not significantly affected by expanding to contexts of length 3. If a similar statistical insignificance can be established for the probability of b, then it does not make sense to expand the node, since its children would not provide us with more information. Figure 5c illustrates how we can estimate the probability for any future sequence of states of the dSRA A of Figure 5a, using the distributions of the PST T of Figure 5b and thus how we can calculate the waiting-time distributions. We first assume that, as the system processes events from the input stream, besides feeding them to A, it also stores them in a buffer that holds the m most recent events, where m is equal to the maximum order of the PST T . After updating the buffer with a new event, the system traverses T according to the contents of the buffer and arrives at a leaf l of T . Let us now assume that, after consuming the last event, A is in state 1 in Figure 5a and T has reached its left-most node, aa, (0.75, 0.25) in Figure 5b. This is shown as the left-most node also in Figure  5c. Each node in this figure has two elements: the first one is the state of A and the second the node of T , starting with {1, aa} as our current "configuration". Each node has two outgoing edges, one for a and one for b, indicating what might happen next and with what probability. For example, from the left-most node of Figure 5c, we know that, according to T , we might see a with probability 0.75 and b with probability 0.25. If we do encounter b, then A will move to state 2 and T will reach leaf b, (0.5, 0.5). This is shown in Figure 5c as the white node {2, b}. This node has a double border to indicate that A has reached a final state.
In a similar manner, we can keep expanding this tree into the future and use it to estimate the waiting-time distribution for its node {1, aa}, i.e., the distribution for state 1 of the automaton of Figure 5a when we know that the last two read symbols are aa. In order to estimate the probability of reaching a final state for the first time in k transitions, we first find all the paths of length k which start from the original node and end in a final state without including another final state. In our example of Figure 5c, if k = 1, then the path from {1, aa} to {2, b} is such a path and its probability is 0.25. Thus, P (W {1,aa} = 1) = 0.25. For k = 2, the path with the purple nodes leads to a final state after 2 transitions. Its probability is 0.75 * 0.25 = 0.1875, i.e., the product of the probabilities on the path edges. Thus, P (W {1,aa} = 2) = 0.1875. If there were more such alternative paths, we would have to add their probabilities.
We can use the waiting-time distributions to produce various kinds of forecasts. In the simplest case, we can perform regression forecasting where we select the future point with the highest probability and return this point as a forecast. Alternatively, we may also perform classification forecasting, if our goal is to determine how likely it is that a CE will occur within the next w input events. We can sum the probabilities of the first w points of a distribution and if this sum exceeds a given threshold we emit a "positive" forecast, meaning that a CE is indeed expected to occur; otherwise a "negative" forecast is emitted, meaning that no CE is expected.

SREM with n-ary conditions on a finite universe
Thus far, we have described how we can perform CEF when we only have unary conditions and a finite or infinite universe. In this case, we create the deterministic automaton and use it to generate a stream of symbols with which we can learn a PST . Note that, when we only have unary conditions and thus no need for registers, SRA are in essence equivalent to symbolic automata. Symbolic automata are determinizable and closed under complement, without requiring a window. Thus, the method  described above for forecasting applies to every SRA with unary conditions, regardless of whether a windowing operator is present. The next case is when we have a finite universe and n-ary conditions, where n ≥ 1. We can follow the same process as described above, with one important difference. Since the universe U is finite, we can directly map each element of U to a symbol. Therefore, the PST T can be constructed directly from the elements of U. In practice, however, if the cardinality of U is high and we have a windowed SREM , it might be preferable to use the conditions of the dSRA A, if their number is significantly lower. A PST with too many symbols can quickly become hard to manage as we increase its order m and it is thus advisable to avoid increasing recklessly the size of its alphabet. We can then map (T, 1, low ) to a, (T, 1, high) to b, etc. However, if we have an automaton that only checks whether a measurement comes from the same sensor as a measurement stored in a register, like EqualId (∼, r 1 ), then we do not need 8 symbols. We can use only a and b, with a corresponding to EqualId (∼, r 1 ) and b to ¬EqualId (∼, r 1 ). The automaton is able to convert a stream/string S constructed from U to a stream/string of a and b symbols, which can then be used to construct a PST .

SREM with n-ary conditions on a infinite universe
Finally, the most general case is when we have an infinite universe and n-ary conditions. In this case, the applicability of our method is necessarily restricted to windowed SREM and SRA. We can construct a deterministic SRA (which, by definition, has only a single run) from the windowed SREM and use this dSRA to generate a (single) sequence of symbols from a training dataset. This sequence can then be used to learn a PST . Then, the dSRA and the PST can be combined, as already described above, to estimate the waiting-time distributions and the forecasts. Example 8.3. As an example, Figure 6 shows the deterministic classical automaton that can be constructed for SREM (2) and the dSRA of Figure 4c (note that Figure 4c and thus Figure 6 do not depict automata in their totality, but only part of them). Assume that we use the stream of Table 1 as a training dataset. We feed it to the automaton of Figure 6. Upon reading the first input event, (T, 1, 22), transition a is triggered. Since the automaton is deterministic, this is the only triggered transition. Thus, (T, 1, 22) is mapped to a and the automaton moves to state {q t , q 1 }. With the second event, (T, 1, 24), transition f is triggered. Thus, (T, 1, 24) is mapped to f . We repeat this process until the whole stream of events has been mapped to a stream of symbols, S = a, f, · · · . S may now be used to learn a PST of a given maximum order. This PST , along with the automaton of Figure 6, can be used to estimate the waiting-time distributions, as in the example of Figure 5c. Figure 6: Classical deterministic automaton corresponding to SREM (2).

Summary & Future Work
We presented an automaton model, SRA, that can act as a computational model for patterns with n-ary conditions (n ≥ 1), which are quintessential for practical CER/F applications. SRA thus extend the expressive power of symbolic automata. They also extend the expressive power of register automata, through the use of conditions that are more complex than (in)equality predicates. SRA have nice compositional properties, without imposing severe restrictions on the use of operators. Most of the standard operators in CER, such as concatenation/sequence, union/disjunction, intersection/conjunction and Kleene-star/iteration, may be used freely. This is not the case though for complement/negation. We showed that complement may be used and determinization is also possible, if a window operator is used, a very common feature in CER. We briefly discussed the complexity of the problems of nonemptiness, membership and universality. Although the problem of membership in general is at least NP-complete, in cases where we can use windowed, deterministic SRA, the cost of updating the state of such an automaton after reading a single element is linear in the number of registers and conditions. We then described how prediction suffix trees may be used to provide a probabilistic description for the behavior of SRA. Prediction suffix trees can look deep into the past and make accurate inferences about the future behavior of SRA, thus allowing us to forecast when a complex event is expected to occur. As a next step, we intend to implement the proposed framework for CER/F, extending our opensource engine, Wayeb 1 , which currently supports only unary conditions. We also intend to investigate in the future the possibility of providing more precise complexity results for SREM and SRA, both from the point of view of formal languages and from the point of view of CER/F, where some extra constraints may exist. For example, besides updating the state of an automaton after reading a new element, we may also need to take into account the time required to report the input events contributing to the detection of a complex event (for more details about this kind of complexity, please consult [10,51], where a model for evaluating efficiency in CER is presented, along with complexity results for symbolic transducers without memory). In the future, we intend to investigate the complexity of decision problems for SRA from this point of view.
For a SREM e and valuations v, v , let L(e, v, v ) denote all strings S such that (e, S, v) v . Similarly, for a SRA A, let L(A, v, v ) denote all the strings S = t 1 , · · · , t n such that there exists an accepting run [1, For every possible SREM e, we will construct a corresponding SRA A and then prove either that L(e) = L(A) or that L(e, v, v ) = L (A, v, v ). The latter implies that L(e, , v ) = L(A, , v ) for some valuation v or equivalently L(e) = L(A), which is our goal. The proof is inductive. We prove directly the base cases for the simple expressions e := ∅, e := , e := φ = R(x 1 , · · · , x n ) and e := φ = R(x 1 , · · · , x n ) ↓ w. For the complex expression e := e 1 · e 2 , e := e 1 + e 2 and e = e * , we use as an inductive hypothesis that our target result hods for the sub-expressions and then prove that it also holds for the top expression. For example, for e := e 1 · e 2 , we assume that We must be careful, however, with the valuations. If, for example, v applies to the SRA A, does it also apply to the sub-automaton A 1 , if A and A 1 have different registers? We can avoid this problem and make all valuations compatible (i.e., having the same domain as functions) by fixing the registers for all expressions and sub-expressions. We can estimate the registers that we need for a top expression e by scanning its conditions and write operations. Let reg(e) be a function applied to a SREM e. We define it as follows: if e = e 1 · e 2 reg(e 1 ) ∪ reg(e 2 ) if e = e 1 + e 2 reg(e 1 ) if e = (e 1 ) * For our proofs that follow, we first apply this function to the top expression e to obtain R top = reg(e) and we use R top as the set of registers for all automata and sub-automata. All valuations can thus be compared without any difficulties, since they will have the same domain R top . Assume e := φ = R(x 1 , · · · , x n ), where φ is a condition and all x i belong to a set of register variables {r 1 , · · · , r k }. We construct the following SRA A = (Q, q s , Q f , R, ∆), where Figure 7b.
We first prove S ∈ L(e, v, v ) ⇒ S ∈ L(A, v, v ) for a string S. It is obvious that S must be composed of a single element, i.e., S = t 1 . Since S = t 1 is accepted by e starting from the valuation v, this means that (φ, S, v) v , with v = v, according to the second case of Definition 3.13. Thus (t 1 , v) |= φ. This then implies that the second case in the definition of a successor configuration (see q s start q f φ := R(x 1 , · · · , x n ) ↓ ∅ (b) Base case of a single condition, e := φ = R(x 1 , · · · , x n ). Assume e := φ = R(x 1 , · · · , x n ) ↓ w, where φ is a condition, all x i belong to a set of register variables {r 1 , · · · , r k } and w a write register (not necessarily one of r i ). We construct the Figure 7c.
The proof is essentially the same as that for the previous case. The only difference is that we need to use the third case from the definition of successor configurations (Definition 4.3). This means that v = v[w ← t 1 ]. If w ∈ R, then t 1 is stored in w and v (w) = t 1 . Otherwise, v remains the same as v.
Assume e := e 1 · e 2 , where e 1 and e 2 are SREM . We first construct A 1 and A 2 , the SRA for e 1 and e 2 respectively. We construct the following Figure 7d. We thus simply connect A 1 and A 2 with an transition. Notice that A 1 .R and A 2 .R may overlap. Their union retains only one copy of each register, if a register appears in both of them.
We first prove S ∈ L(e, v, v ) ⇒ S ∈ L(A, v, v ) for a string S. Since S ∈ L(e, v, v ), S can be broken into two sub-strings S 1 and S 2 such that S = S 1 · S 2 , (e 1 , S 1 , v) v and (e 2 , S 2 , v ) v . This is equivalent to S 1 ∈ L(e 1 , v, v ) and S 2 ∈ L(e 2 , v , v ). From the induction hypothesis (i.e., that what we want to prove holds for the sub-expressions e 1 , e 2 and their automata A 1 , A 2 ) it follows that S 1 ∈ L(A 1 , v, v ) and S 2 ∈ L(A 2 , v , v ). Notice that if A 1 and A 2 have different sets of registers, we can always expand A 1 .R and A 2 .R to their union, without affecting in any way the behavior of the automata. Now, let l 1 = |S 1 | and l 2 = |S 2 |. From S 1 ∈ L(A 1 , v, v ) it follows that there exists an accepting run 1 of A 1 over S 1 such that 1 = [1, A 1 .q s , v] → · · · → [l 1 + 1, A 1 .q f , v ]. Similarly, from S 2 ∈ L(A 2 , v , v ) it follows that there exists an accepting run 2 of A 2 over S 2 such that Let's construct a run by connecting 1 and 2 with an transition: We can see that this is indeed an accepting run of A. Thus S ∈ L(A, v, v ).
The inverse direction, S ∈ L(A, v, v ) ⇒ S ∈ L(e, v, v ), can be proven in a similar manner. Since S ∈ L(A, v, v ), there exists an accepting run of A over S. By the construction of A, however, this run must be in the form = 1 → 2 with 1 being an accepting run of A 1 over a string S 1 and 2 an accepting run of A 2 over S 2 , where S = S 1 · S 2 . We then use the induction hypothesis to prove that S 1 ∈ L(e 1 , v, v ) and S 2 ∈ L(e 2 , v , v ) and finally that S ∈ L(e, v, v ).
Assume e := e 1 + e 2 , where e 1 and e 2 are SREM . We first construct A 1 and A 2 , the SRA for e 1 and e 2 respectively. We construct the following Figure 7e. We thus create a new state, q s , acting as the start state and connect it through transitions to the start states of A 1 and A 2 . We also create a new final state and connect to it the final states of A 1 and A 2 . Again, A 1 .R and A 2 .R may overlap. Their union retains only one copy of each register, if a register appears in both of them.
It is easy to prove that implies that e 1 is accepted by A 1 . It is thus also accepted by A. Similarly if (e 2 , S, v) v for A 2 .
The inverse direction has a similar proof.
Assume e := e * , where e is a SREM . We construct a new SRA A as shown in Figure 7f. We first construct the SRA for e, A. We create a new final and a new start state. We connect the new start state to the old start and to the new final. We connect the old final to the new final and the old start. R is again R top .
We first prove that S ∈ L(e, v, v ) ⇒ S ∈ L(A, v, v ) for a string S. Since S ∈ L(e, v, v ), S = S 1 ·S such that (e, S 1 , v) v and (e * , S , v ) v . Equivalently, this implies that (e, S 1 , v) v 1 and (e, S 2 , v 1 ) v 2 and (e, S 3 , v 2 ) v 3 etc until (e, S n , v n−1 ) v n , where v n = v . We can then construct the run = 1 → 2 → · · · → n . It is easy to see that is an accepting run of A . Similarly for the inverse direction.

Proof:
We first give the algorithm. See Algorithm 2. Note that in this algorithm, the function Enclose is the usual function for -enclosure in standard automata theory and we will not repeat it here (see [52]). Suffice it to say that, when applied to a state q (or set of states {q i }), it returns all the states we can reach from q (or all q i ) by following only -transitions. It is also worth noting that the algorithm does not create the power-set of states and then connects them through transitions. It creates those subsets it needs by "forward-looking" for what is necessary, but it is equivalent to the power-set construction algorithm. We will prove that S ∈ L(A ) ⇔ S ∈ L(A / ∈ ) for a string S. We first prove the direction S ∈ L(A ) ⇒ S ∈ L(A / ∈ ). The other direction can be proven similarly. Let denote an accepting run of A over S, where k = |S| is the length of S.
sub-run k+1 Let / ∈ denote a run of A / ∈ over S.
/ ∈ necessarily follows k transitions, since it does not have any -transitions. On the other hand, may follow more than k transitions (j ≥ k), because several transitions may intervene between "actual", non-transitions, as shown in Run 7. The number of non-transitions is still k. is thus necessarily composed of k "sub-runs", where the first configuration of each sub-run is reached via a non-transition, followed by a sequence of 0 or more transitions. Each line in Run 7 is such a sub-run. We can also split / ∈ in sub-runs, but in this case each such sub-run will be simply composed of a single configuration. See Run 8.
We will prove the following. For each sub-run i of , it holds that: 1. q / ∈,i ∈ q ,i . In fact, q / ∈,i = Enclosure(q ,i ).
2. v ,i = v / ∈,i , i.e., A and A / ∈ have the same register contents at each i.
We can prove this inductively. We assume that the above claims hold for i and then we can show that they must necessarily hold for i + 1. Since they are obviously true for i = 1, they are then true for i = k + 1 as well. Thus, q / ∈,k+1 ∈ Q / ∈,f and / ∈ is an accepting run as well. First, notice that in each sub-run i of , v ,i remains the same, since transitions never modify the contents of the registers. Thus, in , v ,i = v ,i . It is also obviously true that i = i, since transitions do not read elements from S and thus the automaton's head does not move. The only thing that could possibly change is q ,i , so that, in general, q ,i = q ,i . Therefore, in Run 7, we move from sub-run i to sub-run i + 1 by jumping from q ,i to q ,i+1 . This implies that δ φ,i , connecting q ,i to q ,i+1 , is triggered when the contents of the register are those of v ,i = v ,i . Now, q ,i belongs to the enclosure of q ,i . Otherwise, it would be impossible to reach it from q ,i by following only transitions. From the induction hypothesis we know that q / ∈,i must be the enclosure of q ,i . From the construction algorithm for A / ∈ (Algorithm 2) we also know that the transition δ ,i also exists in A / ∈ , with q / ∈,i its source. δ / ∈,i is has the same condition and references the same registers as δ ,i . Since δ ,i is triggered with v ,i , δ / ∈,i must also be triggered because v / ∈ = v ,i (by the induction hypothesis) and thus v / ∈ = v ,i . From the construction algorithm, we can see that q / ∈,i+1 will be the enclosure of q ,i+1 The state q e in Algorithm 2 is q ,i in Run 7, while state p in the algorithm is state q ,i+1 in . p / ∈ is the thus the enclosure of q ,i+1 . Thus there exists q / ∈,i+1 which we can reach from q / ∈,i and which is the enclosure of q ,i . The second part of the induction hypothesis is obviously true for i + 1, i.e., v ,i+1 = v / ∈,i+1 , since exactly the same registers are modified in exactly the same way by δ ,i and δ / ∈,i . Therefore, q ,k+1 ∈ q / ∈,k+1 which implies that q / ∈,k+1 ∈ Q / ∈,f and thus / ∈ is an accepting run of A / ∈ over S.

Proof:
The proof is constructive. We construct a new single-register SRA and show that it has the same language as the multi-register SRA. The new SRA, A sr , has the same number of registers as A mr .
The main difference is that A sr has more states than A mr . See [8] for a similar proof about register automata. Let A mr = (Q mr , q mr,s , Q mr,f , R mr , ∆ mr ) and A sr = (Q sr , q sr,s , Q sr,f , R sr , ∆ sr ) denote the multi-and single-register SRA respectively. Let w = |R mr | = |R sr | denote the number of registers (the same for A mr and A sr ). Let p = (p 1 , · · · , p w ) ∈ (2 Rmr ) w : w k=1 = R mr and p i ∩ p j = ∅ for i = j. In other words, each p i is a subset of R mr and the union of all p i gives us R mr . Therefore, p denotes a partition of R mr . For example, if R mr = {r 1 , r 2 , r 3 , r 4 }, a possible partition would be p = ({r 1 , r 3 }, {r 2 }, {r 4 }, ∅). Let P Rmr = {p | p is a partition of R mr } denote the set of all possible partitions of R mr .
The general idea is that we want to establish a correspondence between the registers of A mr and those of A sr . If all the registers in R mr have different contents, then each one of them may correspond to a unique register in R sr . However, since a transition in A mr may write to multiple registers, at some point in a run of A mr , some of its registers will have the same contents. For example, if R mr = {r 1 , r 2 , r 3 , r 4 }, a transition may write to r 1 and r 3 at the same time. In this case then, the registers of R mr may be partitioned as follows, according to which of them have the same contents: p = ({r 1 , r 3 }, {r 2 }, {r 4 }, ∅). Now, we could map each register of R rs to one of the p i in p. Repeated values in R mr would then exist as single values in R rs . The next issue would then be how we could actually track in a run of A mr the registers that have the same value(s). We could actually achieve this by combining the states of A mr with every possible partition.
For A sr we would then have: • Q sr = Q mr × P Rmr , where × indicates the Cartesian product.
• The set of transitions ∆ sr is defined as follows: -For every δ mr ∈ ∆ mr : δ mr = q mr , → q mr , i.e., for every transition of A mr , we add the transitions δ sr = (q mr , p), → (q mr , p), one for each p ∈ P Rmr .
-For every δ mr ∈ ∆ mr : δ mr = q mr , φ mr → q mr , i.e., for every non-transition of A mr that does not write to any registers, we do the following. Let R φ denote the set of registers referenced/accessed by φ mr . For every p ∈ P Rmr we add a transition δ sr = (q mr , p), φ sr → (q mr , p). φ sr is the same as φ mr with the following difference. Each r mr,i ∈ R φ (i.e., each register referenced by φ mr ) is replaced in the condition by r sr,j ∈ R sr , where j is such that r mr,i ∈ p j . For example, if p = (p 1 , p 2 , p 3 , p 4 ) = ({r mr,1 , r mr,3 }, {r mr,2 }, {r mr,4 }, ∅) and φ mr = φ(r mr,4 ), then, φ sr = φ(r sr,3 ), since r mr,4 ∈ p 3 . Notice that only one such j exists because p is a partition and, by definition, the different sets of a partition do not have common elements.
We want to show that L(A mr ) = L(A sr ). First, assume that S ∈ L(A mr ) for a string S. We will show that S ∈ L(A sr ). Let mr be an accepting run of A mr over S: mr =[1, q mr,1 = q mr,s , v mr,1 = ] Let sr be a run of A sr over S: We need to show that q sr,l+1 ∈ Q sr,f . We can prove this inductively. As our induction hypothesis, we assume that q sr,i = (q, p), where 1. q = q mr,i and 2. p = (p i,1 , · · · , p i,w ) such that for all 1 ≤ k ≤ w (i.e., all registers of A sr ) v sr,i (r sr,k ) = v mr,i (r mr,k ) for all r mr,k ∈ p i,k .
In other words, at the i th configuration in sr , we have reached a state q sr,i . The first element of this state must be q mr,i , i.e., the state at the i th configuration of mr . The second element must be a partition (of the registers of A mr ). The contents of the first register of A sr , r sr,1 , must be equal to the contents of the registers of the first set in the partition, the contents of the second register r st,2 equal to those of the second set, etc. For example, if p = (p i,1 , p i,2 , p i,3 , p i,4 ) = ({r mr,1 , r mr,3 }, {r mr,2 }, {r mr,4 }, ∅), then the contents of r sr,1 must be the same as those of r mr,1 and r mr,3 . Similarly, the contents of r sr,2 and r mr,2 must be the same. Similarly for r sr,3 and r mr,4 . We must then show that, if the induction hypothesis holds for the i th configuration, it also holds for the (i + 1) th one. First, assume that δ mr,i = q mr,i , → q mr,i+1 . Then, from the construction of A sr , we know that there exists δ sr ∈ ∆ sr such that δ sr = (q mr,i , p), → (q mr,i+1 , p). The first part of the induction hypothesis then still holds because we can move to a state whose first element is q mr,i+1 . The second part of the hypothesis also holds because p remains the same and we already know that this part holds for p from the hypothesis itself. Now, assume that δ mr,i = q mr,i , φ mr → q mr,i+1 , with φ mr = . Then, from the construction of A sr , we know that there exists δ sr ∈ ∆ sr such that δ sr = (q mr,i , p), φ sr → (q mr,i+1 , p) and the condition φ sr is triggered. We can prove the latter claim about φ sr by noticing that φ mr is triggered. Now, from the construction, φ sr is the same as φ mr with its arguments/registers appropriately replaced, as described above. Without loss of generality, assume that φ mr references all of its registers (if this is not the case, we can always construct an equivalent condition that references all registers, but does not actually access any of the redundant ones). We can write it as follows: φ mr = φ(r mr,1 , · · · , r mr,w ) φ sr can be written as follows: φ sr = φ(r sr,i 1 , · · · , r mr,iw ) where i 1 is such that r mr,1 ∈ p i 1 , i.e., i 1 is the partition set from p where r mr,1 belongs. Similarly for i 2 , etc. For example, if R mr = {r mr,1 , r mr,2 , r mr,3 , r mr,4 } and p = (p 1 , p 2 , p 3 , p 4 ) = ({r mr,1 , r mr,3 }, {r mr,2 }, {r mr,4 }, ∅) then φ mr = φ(r mr,1 , r mr,2 , r mr,3 , r mr,4 ) and φ sr = φ(r sr,1 , r sr,2 , r sr,1 , r sr,3 ) From the induction hypothesis, we know, however, that v mr,i (r mr,j ) = v sr,i (r sr,i j ). Therefore, φ mr and φ sr essentially have the same arguments. Since φ sr is also triggered, the first part of the induction hypothesis holds for (i + 1) as well. The second part also holds since p again remains the same. Finally, assume that δ mr,i = q mr,i , φ mr ↓ R w → q mr,i+1 , with φ mr = and R w = ∅. Then, from the construction of A sr , we know that there exists δ sr ∈ ∆ sr such that δ sr = (q mr,i , p), φ sr ↓ r rs,k → (q mr,i+1 , p ) and the condition φ sr is triggered. The proof for φ sr being triggered is the same as in the previous case. We additionally need to prove the second part of the induction hypothesis, since p now becomes p . In other words, we need to prove for p that the contents of a register j of A sr are the same as those of the registers of A mr contained in the j th set in the partition p . Indeed, this is the case. From the construction, we know that the partition set p k (reminder: r sr,k is the write register in δ sr ) becomes p k = p k ∪ R w . Since p k ⊂ R w , this means that p k = R w . Thus the hypothesis still holds for p k , since r sr,k and all registers in R w will have the same value. The hypothesis also holds for k = k. Since p k = p k \ R w and the hypothesis holds for p, this means that p k had registers with the same contents before the writing to R w . If we remove from p k the changed registers to obtain p k , then p k will still have registers with the same contents after the writing to R w . Additionally, since r sr,k was not changed, it will still have the same contents as the registers in p k .
We know that the hypothesis holds for i = 1 in the runs mr and sr , because q sr,s = (q mr,s , p s ), with p s = (R mr , ∅, · · · , ∅). The first part of the hypothesis obviously holds. The second part also holds since all registers are empty in both runs at the beginning. Therefore, the hypothesis holds for i = 2, i = 3, etc. sr is thus an accepting run of A sr over S.
We have proven that S ∈ L(A mr ) ⇒ S ∈ L(A sr ). The inverse direction, i.e., S ∈ L(A sr ) ⇒ S ∈ L(A mr ), can be proven similarly. We first assume that there is an accepting run sr of A sr over S and then show, in a similar manner, that there exists an accepting runf= mr of A mr over S.

Proof:
The proof develops along lines similar to the corresponding proof for classical and register automata [53,11]. It uses a generalized version of SRA, denoted by gSRA. These are SRA whose transitions are not equipped with a single condition, but with a whole SREM . For example, the ) → q f . The single transition δ can read two characters at the same time, apply φ 1 on the first one, store this character in r 1 and then apply φ 2 on the second character and the contents of r 1 . We assume that all transitions have been eliminated and that the SRA is single-register (and if not, it has been converted to one, as shown in Appendix 10.3). We also demand that a) gSRA have a single start state with no incoming transitions and with outgoing transitions to every other state, b) they have a single final state with no outgoing transitions and with incoming transitions from every other state, c) there is an arrow connecting any two other states. We say that a gSRA A g accepts a string S if S = S 1 · S 2 · · · · · S k and there exists a run = [1, where the state of the first configuration is the start state of A g (q 1 = A g .q s ), the state of the last configuration is its final state (q k+1 = A g .q f ) and for each i there exists a transition δ of A g such that δ = q i , e i → q i+1 and We first convert the initial SRA A to a gSRA A g as follows. We add a new start state and connect it to the old start state with an transition. We also connect with such a transition the old final state to a new final state. It there are multiple transitions between any two states, we combine them into a single transition whose condition will be the union of the conditions of the previous transitions (we can do this since we are allowed to have SREM on the transitions now). Finally, if there exist states that are not connected to each other, we connect them with ∅ transitions (making sure that we do not add incoming transitions to the start state or outgoing transitions to the final state). This procedure will produce a gSRA A g which will be equivalent in terms of its language to the original SRA A.
The basic idea is to start removing states from A g , one at a time, without affecting the language it accepts. This procedure is repeated until we are left with 2 states. At this point, the gSRA will have one start and one final state, connected with a single transition. The SREM on this transition is finally returned as the SREM corresponding to the initial SRA A. The critical step in this process is of course the one where a state is removed. We must ensure that any repairs we make to the remaining transitions do not affect the automaton's language. We first select a state to remove, q rip . This can be any state, except for the start or the final states. We then check all pairs of states q i and q j . We need to make sure that the new automaton will be able to move from q i to q j with exactly the same strings as when q rip was present. We thus have to modify the SREM on the transition from q i to q j . The modification is the following. Assume, that, in the old automaton, before the removal, the following hold: • q i , e 1 → q rip .
Notice that such transitions exist for every pair q i and q j , since, by definition, transitions exist between all pairs of states. Then, after removing q rip , the SREM on the transition from q i to q j becomes (e 1 · (e 2 ) * · e 3 ) + e 4 . See Algorithm 3.
We now need to prove that A g with n states (A g,n ) and A g with n−1 states (A g,n−1 ), as constructed from A g,n via Algorithm 3, are equivalent, i.e., that S ∈ L(A g,n , v, v ) ⇔ S ∈ L(A g,n−1 , v, v ). If we can prove this, then the last step of the recursion of Algorithm 3 (Line 2) will give us an automaton that is equivalent to our initial SRA A. Moreover, the SREM on the single transition of this gSRA is obviously the desired SREM .
First, assume that S ∈ L(A g,n , v, v ). Then, there exists an accepting run of A g,n Now, assume that q i = q rip for all q i of , including, of course, the start and final states. We claim that this run would also be an accepting run for A g,n−1 . To prove this, notice that between any two successive configurations [i, q i , v i ] → [j, q j , v j ] appearing in , there exists a transition that is triggered between q i and q j . Let e 4 denote the SREM on this transition. In A g,n−1 the SREM on this transition would become (e 1 · (e 2 ) * · e 3 ) + e 4 . Thus, it would also be triggered, due to the presence of the term e 4 , assuming the same valuation v i . We can inductively prove, based on the length of the run, that this holds for any two successive configurations. It obviously holds for the first and second configurations, since we start with empty registers and thus the same valuation. As a result, v 2 would also be the same. Inductively, we can prove the same for v 3 , etc. The other case is when q i = q rip for some i (or multiple is) in . We would then have in a sequence of successive configurations like the following: We claim that, if we remove from all configurations with q rip , then the remaining configurations would form an accepting run of A g,n−1 . To prove this, notice that the transition from q i to q rip in would happen through the e 1 SREM . Then, every loop (if any) from q rip to itself would occur because of the e 2 SREM . Finally, the jump from q rip to q l would happen through e 3 . Thus, the move from q i to q l would happen via e 1 · (e 2 ) * · e 3 . But this is exactly one of the disjuncts on the transition from q i to q l in A g,n−1 . We can therefore remove all consecutive configurations with q rip from . If there are multiple such sequences in , we can repeat the same process as many times as necessary.
We have thus proven that S ∈ L(A g,n , v, v ) ⇒ S ∈ L(A g,n−1 , v, v ) Conversely, assume that S ∈ L(A g,n−1 , v, v ). There is then an accepting run of A g,n−1 . The move between each sequence of successive configurations, from state q i to q j , happens either due to e 4 or due to e 1 · (e 2 ) * · e 3 . In the former case, we can retain this move as is in a new run for A g,n .
In the latter case, we can insert between the configurations of q i and q j a sequence of configurations with q rip , as already described previously. Thus, S ∈ L(A g,n−1 , v, v ) ⇒ S ∈ L(A g,n , v, v ). This completes our proof.

Proof:
For union, concatenation and Kleene-star the proof is essentially the proof for converting SREM to SRA. For concatenation, if we have SRA A 1 and A 2 we construct A as in Figure 7d. For union, we construct the SRA as in Figure 7e. For Kleene-star, we construct the SRA as in Figure 7f. The only difference in these constructions is that we now assume, without loss of generality, that the A 1 .R ∩ A 2 .R = ∅, i.e., that A 1 and A 2 have different sets of registers and that the automaton A constructed from A 1 and A 2 retains all registers of both A 1 and A 2 . For example, if we have two SRA A 1 and A 2 and we want to construct a SRA A such that L(A) = L(A 1 ) · L(A 2 ) then we connect A 1 's final state to A 2 's start state via an transition. It is easy to see that if S 1 ∈ L(A 1 ) and S 2 ∈ L(A 2 ) then S = S 1 · S 2 ∈ L(A). S 1 will force A to move to A 1 s final state (both A and A 1 start with empty registers). Subsequently, A will jump to A 2 's start state and then S 2 will force A to go to A 2 's final state which is A's final state, since A 2 's registers in A are empty when A 2 starts reading S 2 .
• For each q = (q 1 , q 2 ) ∈ Q we add a transition δ to q = (q 1 , q 2 ) ∈ Q if there exists a transition δ 1 from q 1 to q 1 in A 1 and a transition δ 2 from q 2 to q 2 in A 2 . The condition of δ is φ = δ 1 .φ ∧ δ 2 .φ. The write registers of δ are W = δ 1 .W ∪ δ 2 .W (notice that, if δ 1 .W = ∅ and δ 2 .W = ∅, this creates a multi-register SRA, even if A 1 and A 2 are single-register). Thus, It is evident that, if a string S is accepted by both A 1 and A 2 , it is also accepted by A. If A is not accepted either by A 1 or A 2 , then it is not accepted by A. Therefore, L(A) = L(A 1 ) ∩ L(A 2 ).
Since SRA and SREM are equivalent, SREM are also closed under union, intersection, concatenation and Kleene-star.

Proof:
The proof is by a counter example. Let A denote the SRA of Figure 8. This SRA reads strings composed of tuples. Each tuple contains an attribute called type, taking values from a finite or infinite φ(r 1 ) :=∼ .type = v(r 1 ).type Figure 8: SRA accepting strings which have the same type in two elements. Notice that ∼ denotes the current event (last event read from the string). Figure 9: SRA accepting all strings containing an a element followed by a b element, whose identifiers are the same.
alphabet. The symbol ∼ simply denotes the current element of the string, i.e., the last element read from it. Therefore, A accepts strings in which there are two elements with the same type, regardless of the length of S. Assume that there exists a SRA A c which accepts only when A does not accept. In other words, A c accepts all strings S whose elements all have a different type. Let k = |A c .R| be the number of registers of A c . Let |S| = k + m, where m > 1, be the length of a string S whose elements all have different types. However, A c cannot possibly exist. At the end of S, as A c is ready to read the last element of S, it must have stored all of the previous k + m − 1 elements of S. But A has only k registers, whereas k + m − 1 > k, since m > 1. Thus, A c cannot exist.

Proof of Theorem 5.11
Theorem 10.7. SRA are not closed under determinization.

Proof:
The proof is again by a counter example. Let A denote the SRA of Figure 9. This SRA reads strings composed of tuples. Each tuple contains an attribute, called type, taking values from a finite or infinite alphabet. It also contains another tuple, called id , taking integer values. A thus accepts strings S that contain an a followed by a b, whose ids are equal, regardless of the length of S. Assume there exist a dSRA A d with k registers which is equivalent to A. Let be a string given to A d . After reading S 1 = (a, 1), A d must store it in a register r 1 in order to be able to compare it when (b, 2) arrives. Let S = (a, 1)(a, 3)(b, 2) After reading S 1 = (a, 1), A d must store it in the register r 1 , since A d is deterministic and follows a single run. Thus, it must have the exact same behavior after reading s 1 and S 1 . But we must also store S 2 = (a, 3) after reading it. Additionally, S 2 must be stored in a different register r 2 . We cannot overwrite r 1 . If we did this and S 1 were (a, 2), then we would not be able to match (a, 2) to S 3 = (b, 2) and S = (a, 2)(a, 3)(b, 2) would not be accepted. Now, let S = (a, · · · )(a, · · · ) · · · (a, · · · ) k+1 elements With a similar reasoning, all of the first k + 1 elements of S must be stored after reading them. But this is a contradiction, as A d can store at most k different elements. Therefore, there does not exist a dSRA which is equivalent to A.

Structural Properties of SRA
In the proofs that follow, we will need to refer to some structural properties of SRA. We present them here. Without loss of generality, we assume that each state of a SRA is accessible from its start state. Inaccessible states can always be removed without affecting the behavior of an automaton. Therefore, a SRA, in terms of its structure, can be viewed as a weakly connected directed graph. The usual notions of walks and trails from graph theory also apply for a SRA. However, since we are interested in walks and trails from its start state, and in order to avoid introducing new notation and terminology, in what follows, we will stick to the already introduced terms. We will talk about states, instead of nodes/vertices, and about transitions, instead of edges.
A is a sequence of transitions w =< δ 1 , · · · , δ k >, such that: We say that such a walk is of length k. By W A we denote the set of all walks over A and by W A,q , we denote the set of walks over A that end in state q, i.e., W A,q = {w : w ∈ W A ∧ δ k .target = q}. Definition 10.9. (Trail over SRA) A trail t over a SRA A is a walk w =< δ 1 , · · · , δ k > over A, such that: If T A is the set of all trails over A, T A,q is the set of all trails ending in state q, i.e., T A,q = {t : t ∈ T A ∧ δ k .target = q}.
In other words, a trail is a walk without state revisits (and, as a consequence, without transition revisits).

Proof:
The proof is by induction on the length of the walk. The proposition trivially holds for walks of length k = 1. For walks of length k + 1, if w is already a trail, then the proposition holds for k + 1. If w is not a trail, then a state is visited at least twice. Removing all transitions between these two visits results in a walk for which, by the induction hypothesis, the proposition already holds. Therefore, it holds for the complete walk too.
We give a detailed proof by induction on the length of the walk.
• Base case for k = 1. If w =< δ 1 > is a walk to q, then, t =< δ 1 > is also a trail to q, since q = q s .
is a walk of length k + 1 (where we use a slightly different notation to explicitly show the visited states).
-If w is already a trail, then the proposition holds for k + 1.
-If w is not a trail, then a state is visited at least twice. Assume that it is q i , visited again as q j , i.e., q i = q j . Remove from w all transitions δ l , i ≤ l < j. Then we get Notice that w is indeed a walk, since all its transitions are valid, including the one that stitches together the two sub-walks (q j δ j → q j+1 ). Moreover, its length is at most k, since we removed at least one transition. Therefore, by the induction hypothesis, there exists a trail t to q k+2 , contained in w . But t is also contained in w. Therefore, t is a trail to q k+2 contained in w and the proposition holds for walks of length k + 1 as well.
Definition 10.11. (Register appearance in a trail) We say that a register r appears in a trail if there exists at least one transition δ in the trail such that r ∈ δ.W .
In other words, a trail must write to r to say that it appears in it.
Notice that a run of A over a stream S induces a walk over A.
is a run of a SRA A, then w =< δ 1 , · · · , δ n−1 > is the walk induced by .
10.9. Proof of Lemma 5.13 Theorem 10.13. For every windowed SREM there exists an equivalent unrolled SRA without any loops, i.e., a SRA where each state may be visited at most once.
.w] . Algorithm 4 shows how we can construct A ew . The basic idea is that we first construct as usual the SRA A e for the sub-expression e (and eliminate -transitions). We can then use A e to enumerate all the possible walks of A e of length up to w and then join them in a single SRA through disjunction. Essentially, we need to remove cycles from every walk of A e by "unrolling" them as many times as necessary, without the length of the walk exceeding w. This "unrolling" operation is performed by the (recursive) Algorithm 5. Because of this "unrolling", a state of A e may appear multiple times as a state in A ew . We keep track of which states of A ew correspond to states of A e through the function CopyOfQ in the algorithm. For example, if q e is a state of A e , q ew a state of A ew and CopyOfQ(q ew ) = q e , this means that q ew was created as a copy of q e (and multiple states of A ew may be copies of the same state of A e , i.e., CopyOfQ is a surjective but not an injective function). We do the same for the registers as well, through the function CopyOfR. The algorithm avoids an explicit enumeration, by gradually building the automaton as needed, through an incremental expansion. Of course, walks that do not end in a final state may be removed, either after the construction or online, whenever a non-final state cannot be expanded.
The lemma is a direct consequence of the construction algorithm. First, note that, by the construction algorithm, there is a one-to-one mapping (bijective function) between the walks/runs of A ew and the walks/runs of A e of length up to w. We can show that if e is a run of A e of length up to w over a string S ( e has at most w transitions), then the corresponding run ew of A ew is indeed a run and if Proposition 10.14. There exists a run of A e over a string S of length up to w e = [1, q e,1 = A e .q s , v e,1 ] iff there exists a run ew of A ew such that: • CopyOfQ(q ew,i ) = q e,i • v e,i (r e ) = v ew,i (r ew ), if CopyOfR(r ew ) = r e and r ew appears last among the registers that are copies of r e in ew .
We say that a register r appears in a run at position i if r ∈ δ i .W , i.e., if the i th transition writes to r. We say that a register r ew , where CopyOfR(r ew ) = r e , appears last if no other copies of r e appear after r ew in a run. The notion of a register's (last) appearance also applies for walks of A ew , since A ew is a directed acyclic graph, as can be seen by Algorithms 6 and 7 (they always expand "forward" the SRA, without creating any cycles and without converging any paths).

Proof:
The proof is by induction on the length of the runs k, with k ≤ w. We prove only one direction (assume a run e exists). The other is similar.
Base case: k = 0. For both SRA, only the start state and the initial configuration with all registers empty is possible. Thus, v e,i = v ew,i = for all registers. By Algorithm 6 (line 2), we know that CopyOf (q ew,s ) = q e,s .
Case for 0 < k + 1 ≤ w, assuming the proposition holds for k. Let e,k+1 = · · · [k, q e,k , v e,k ] δ e,k → [k + 1, q e,k+1 , v e,k+1 ] and ew,k+1 = · · · [k, q ew,k , v ew,k ] be the runs of A e and A ew respectively of length k + 1 over the same k + 1 elements of a string S. We know that e,k+1 is an actual run and we need to construct ew,k+1 , knowing, by the induction hypothesis, that there is an actual run up to q ew,i+k . Now, by the construction algorithm, we can see that if δ e,k is a transition of A e from q e,k to q e,k+1 , there exists a transition δ ew,k with the same condition from q ew,k to a q ew,k+1 such that CopyOfQ(q ew,k+1 ) = q e,k+1 . Moreover, if δ e,k is triggered, so does δ ew,k , because the registers in the register selection of δ ew,k are copies of the corresponding registers in δ e,k .φ.rs. By the induction hypothesis, we know that the contents of the registers in δ e,k .φ.rs will be equal to the contents of their corresponding registers in ew that appear last. But these are exactly the registers in δ ew,k .φ.rs (see line 22 in Algorithm 7). We can also see that the part of the proposition concerning the valuations v also holds. If δ e,k .W = {r e } and δ ew,k .W = {r ew }, then we know, by the construction algorithm (line 18), that CopyOfR(r ew ) = r e and r ew will be the last appearance of a copy of r e in ew,k+1 . Thus the proposition holds for 0 < k + 1 ≤ w as well.
The above proposition must necessarily hold for accepting runs as well. Therefore, A e accepts the same language as A ew .
We also note that w must be a number greater than (or equal to) the minimum length of the walks induced by the accepting runs of A e (which is something that can be computed by the structure of the expression). Although this is not a formal requirement, if it is not satisfied, then A ew won't detect any matches.

Proof:
The process for constructing a deterministic SRA (dSRA) from a windowed SREM is shown in Algorithm 8. It first constructs a non-deterministic SRA (nSRA) and then uses the power set of this nSRA's states to construct the dSRA. For each state q d of the dSRA, it gathers all the conditions from the outgoing transitions of the states of the nSRA q n (q n ∈ q d ), it creates the (mutually exclusive) minterms of these conditions, i.e., the set of maximal satisfiable Boolean combinations of the conditions. It then creates transitions, based on these minterms. Please, note that we use the ability of a transition to write to more than one registers. So, from now on, δ.W will be a set that is not necessarily a singleton. This allows us to retain the same set of registers, i.e., the set of registers R will be the same for the nSRA and the dSRA. A new transition created for the dSRA may write to multiple registers, if it "encodes" multiple transitions of the nSRA, which may write to different registers. It is also obvious that the resulting SRA is deterministic, since the various minterms out of every state are mutually exclusive, i.e., at most one may be triggered. Intuitively, having a windowed SRA allows us to construct a deterministic SRA with as many registers as necessary. Therefore, it is always possible to have available all past w elements. This is not possible in the counter-example of Section 10.7, where we showed that SRA are not in general determinizable.
First, we will prove the following proposition: are the runs of A n and A d respectively, then, • q n,i ∈ q d,i ∀i : 1 ≤ i ≤ k • if r ∈ A d .R appears in n , then it appears in d • v n,i (r) = v d,i (r) for every r that appears in n (and d ) We say that a register r appears in a run at position i if r ∈ δ i .W .

Proof:
We will prove only direction (the other is similar). Assume there exists a run n . We will prove that there exists a run d by induction on the length k of the run. Base case: k = 0. Then n = [1, q n,1 , ] = [1, q n,s , ]. The run d = [1, q d,s , ] is indeed a run of the dSRA that satisfies the proposition, since q n,s ∈ q d,s = {q n,s } (by the construction algorithm, line 22), all registers are empty and no registers appear in the runs.
Case k > 0. Assume the proposition holds for k. We will prove it holds for k + 1 as well. Let n,k+1 = · · · [k, q n,k , v n,k ] be the possible runs that can follow a run n,k after the nSRA reads the (k + 1) th tuple. Notice that, typically, since A n is non-deterministic, there might be multiple runs n,k and each such run can spawn its own multiple runs n,k+1 . The same reasoning that we present below applies to all these n,k . We need to find a run of the dSRA like: By the induction hypothesis, we know that q n,k ∈ q d,k . By the construction Algorithm 8, we then know that, if φ j n,k = δ j n,k .φ is the condition of a transition that takes the non-deterministic run to q j n,k+1 , then there exists a transition δ d,k in the dSRA from q d,k whose condition will be a minterm, containing all the φ n,k in their positive form and all other possible conditions in their negated form.
Moreover, the target of that transition, q d,k+1 , contains all q j n,k+1 . More formally, q d,k+1 = m j=1 q j n,k+1 . As an example, see Figure 10. Figure 10a depicts part of a nSRA. Figure 10b depicts part of the dSRA that woyld be constructed from that of Figure 10a. The construction algorithm would create the state {q 2 , q 4 }, the minterms from the conditions of all the outgoing transitions of q 2 and q 4 and then attempt to determine which minterm would move the dSRA to which subset of {q 2 , q 3 , q 5 }. The results is shown in Figure 10b. Now, assume that a run of the nSRA has reached q 1 via one run and q 4 via another run, i.e. q n,k = q 1 in Eq. (9) for the first of these runs and q n,k = q 4 for the second. Assume also that both φ 1 and φ 2 are triggered after reading the (k + 1) th element, but not φ 3 . This means that the nSRA would move to q 2 and q 3 . In Eq. (9), this would mean that m = 2 and that δ 1 n,k .φ = φ 1 and δ 2 n,k .φ = φ 2 . But in the dSRA there is a transition that simulates this move of the nSRA. The minterm φ 1 ∧φ 2 ∧(¬φ 3 ) moves the dSRA to {q 2 , q 3 }. It contains δ 1 n,k .φ and δ 2 n,k .φ in their positive form and all other conditions (here only φ 3 ) in their negated form. With a similar reasoning, we see that the dSRA can simulate the nSRA for every other possible combination of {φ 1 , φ 2 , φ 3 }. (a) nSRA. What we have proven thus far is a structural similarity between nSRA and dSRA. We also need to prove that δ d,k applies as well, i.e., that the minterm on this transition is triggered exactly when its positive conjuncts are triggered. To prove this, we need to show that the contents of the registers that a condition φ of the nSRA accesses are the same that this φ accesses in the dSRA when participating in a minterm.
As we said, the condition on δ d,k is a conjunct (minterm), where all φ j n,k appear in their positive form and all other conditions in their negated form. But note that the conditions in negated form are those that were not triggered in n,k+1 when reading the (k + 1) th tuple. Additionally, the arguments passed to each of the conditions of the minterm are the same (registers) as those passed to them in the non-deterministic run (by the construction algorithm, line 11). To make this point clearer, consider the following simple example of a minterm: φ = φ 1 (r 1,1 , · · · , r 1,k ) ∧ ¬φ 2 (r 2,1 , · · · , r 2,l ) ∧ φ 3 (r 3,1 , · · · , r 3,m ) This means that φ 1 (r 1,1 , · · · , r 1,k ), with the exact same registers as arguments, will be the formula of a transition of the nSRAthat was triggered. Similarly for φ 3 . With respect to φ 2 , it will be the condition of a transition that was not triggered. If we can show that the contents of those registers are the same in the runs of the nSRA and dSRA when reading the last tuple, then this will mean that δ d,k .φ is indeed triggered. But this is the case by the induction hypothesis (v n,k (r) = v d,k (r)), since all these registers appear in the run n,k up to q n,k .
The second part of the proposition also holds, since, by the construction, δ d,k will write to all the registers that the various δ j n,k write (see line 19 in the determinization algorithm). The third part also holds. This is the part that actually ensures that the contents of the registers are the same. First, note that a register can appear only once in a run of A n , because of its tree-like structure. Second, by the construction, we know that δ d,k .W = m j=1 δ j n,k .W (see again line 19 in the algorithm). Therefore, we know that δ d,k will write only to registers that had not appeared before in the run of the nSRA and will leave every other register that had appeared unaffected. This observation is critical. We could not claim the same for non-windowed SRA, as in Figure 9. If we attempted to determinize this nSRA, without unrolling its cycles, the resulting SRA could overwrite r 1 . Now, since δ d,k and all the δ j n,k write the same element and δ d,k does not affect any previously appearing registers, the proposition holds.
Since the above proposition holds for accepting runs as well, we can conclude that there exists an accepting run of A n iff there exists an accepting run of A d . According to the above proposition, the union of the last states over all n is equal to the last state of d . Thus, if n reaches a final state, then the last state of d will contain this final state and hence be itself a final state. Conversely, if d reaches a final state of A d , it means that this state contains a final state of A n . Then, there must exist a n that reached this final state.

Proof:
Let A be a windowed SRA. We first determinize it to obtain A d . Although A d is deterministic, it might still be incomplete, i.e., there might be states from which it might be impossible to move to another state. This may happen if it is possible that the conditions on all of the outgoing transitions of such a state are not triggered. As in classical automata, such a behavior implies that the string provided to the automaton is not accepted by it.
We can make A d complete by adding a so-called "dead" state q dead (non-final) to A d . See Algorithm 9. For each state q of A d , we then gather all the conditions on its outgoing transitions. Let Φ denote this set of conditions. We can then create the conjunction of all the negated conditions in Φ: φ dead := (¬φ 1 ) ∧ (¬φ 2 ) ∧ · · · ∧ (¬φ n ), where φ i ∈ Φ and n i=1 φ i = Φ. We then add a transition from q to q dead with φ dead as its condition and ∅ as its write registers. If we do this for every state q ∈ A d .Q, we will have created a SRA that is equivalent to A d , since transitions to q dead are only triggered if none of the other conditions in Φ are triggered. If there exists a condition φ i that is triggered, the new automaton will behave exactly as A d and if no φ is triggered it will go to q dead . Now, if we add a self-loop transition on q dead with as its condition, we also ensure that the new automaton will always stay in q dead once it enters it. q dead thus acts as a sink state. This new automaton A d,c will therefore be equivalent to A d and it will also be both deterministic and complete.
The final move is to flip all the states of A d,c , i.e., make all of its final states non-final and all of its non-final states final, to obtain an automaton A complement . This then ensures that if a string S is accepted by A (or A d ), it will not be accepted by A complement and if it is accepted by A complement it will not be accepted by A. This is indeed possible because A (and A complement ) is deterministic and complete. Therefore, for every string S, there exists exactly one run of A (and A complement ) over S. If A, after reading S, reaches a final state, A complement necessarily reaches a non-final state and vice versa. Therefore, for every windowed SRA A we can indeed construct a SRA which accepts the complement of the language of A.
Notice that this trick of flipping the states would not be possible if A were non-deterministic. To see this, assume that A is non-deterministic and at the end of S it reaches states q 1 and q 2 , where q 1 is non-final and q 2 is final. This means that S is accepted by A. If we flip the states of the nondeterministic A to get its complement A complement , we would again reach q 1 and q 2 , where, in this case, q 1 is final and q 2 is non-final. A complement would thus again accept S, which is not the desired behavior for A complement .
10.12. Proof of Proposition 6.2 Proposition 10.18. If S = t 1 , t 2 , · · · is a stream of elements from a universe U of a V-structure M, where t i ∈ U, and e is a SREM over M, then, for every S m..k , S m..k ∈ L(e) iff S 1..k ∈ L(e s ) (and S 1..k ∈ L(A es )).