Alternating Automata Modulo First Order Theories

Many results in automata theory rely on the finite alphabet hypothesis, which guarantees, in some cases, the existence of determinization, complementation and inclusion checking methods. However, this hypothesis prevents the use of automata as models of real-time systems or even simple programs, whose input and output are data values ranging over very large domains, typically viewed as infinite mathematical abstractions.

Traditional attempts to generalize classical Rabin-Scott automata to infinite alphabets, such as timed automata [1] and finite-memory automata [16] face the complement closure problem: there exist automata for which the complement language cannot be recognized by an automaton in the same class. This makes it impossible to encode a language inclusion problem \({\mathcal L}({A}) \subseteq {\mathcal L}({B})\) as the emptiness of an automaton recognizing the language \({\mathcal L}({A}) \cap {\mathcal L}^c({B})\), where \({\mathcal L}^c({B})\) denotes the complement of \({\mathcal L}({B})\).

Even for finite alphabets, complementation of finite-state automata faces inherent exponential blowup, due to nondeterminism. However, if we allow universal nondeterminism, in addition to the classical existential nondeterminism, complementation is possible is linear time. Having both existential and universal nondeterminism defines the alternating automata model [4]. A finite-alphabet alternating automaton is described by a set of transition rules \(q \xrightarrow {{\scriptscriptstyle a}}_{{\scriptstyle }} \phi \), where q is a state, a is an input symbol and \(\phi \) is a boolean formula, whose propositional variables denote successor states.

Our Contribution. We extend alternating automata to infinite data alphabets, by defining a model of computation in which all boolean operations, including complementation, can be done in linear time. The control states are given by k-ary predicate symbols \(q(y_1,\ldots ,y_k)\), the input consists of an event a from a finite alphabet and a tuple of data variables \(x_1,\ldots ,x_n\), ranging over an infinite domain, and transitions are of the form \(q(y_1,\ldots ,y_k) \xrightarrow {{\scriptscriptstyle a(x_1,\ldots ,x_n)}}_{{\scriptstyle }} \phi (x_1, \ldots , x_n, y_1, \ldots , y_k)\), where \(\phi \) is a formula in the first-order theory of the data domain. In this model, the arguments of a predicate atom \(q(y_1,\ldots ,y_k)\) represent the values of the internal variables associated with the state. Together with the input values \(x_1,\ldots ,x_n\), these values define the next configurations, but remain invisible in the input sequence.

The tight coupling of internal values and control states, by means of uninterpreted predicate symbols, allows for linear-time complementation just as in the case of classical propositional alternating automata. Complementation is, moreover, possible when the transition formulae contain first-order quantifiers, generating infinitely-branching execution trees. The price to be paid for this expressivity is that emptiness of first-order alternating automata is undecidable, even for the simplest data theory of equality [6].

The main contribution of this paper is an effective emptiness checking semi-algorithm for first-order alternating automata, in the spirit of the IMPACT lazy annotation procedure, originally developed for checking safety of nondeterministic integer programs [20, 21]. In a nutshell, a lazy annotation procedure unfolds an automaton A trying to find an execution that recognizes a word from \({\mathcal L}({A})\). If a path that reaches a final state does not correspond to a concrete run of the automaton, the positions on the path are labeled with interpolants from the proof of infeasibility, thus marking this path and all continuations as infeasible for future searches. Termination of lazy annotation procedures is not guaranteed, but having a suitable coverage relation between the nodes of the search tree may ensure convergence of many real-life examples. However, applying lazy annotation to first-order alternating automata faces two nontrivial problems:

We use first-order alternating automata to develop practical semi-algorithms for a number of known undecidable problems, such as: inclusion of regular timed languages [1], inclusion of quasi-regular languages recognized by finite-memory automata [16] and emptiness of predicate automata, a subclass of first-order alternating automata used to verify parameterized concurrent programs [6, 7].

Related Work. Recognizers for languages over infinite alphabets have found various applications, ranging from Unicode text recognition [5] to runtime program monitoring [2]. Extending finite automata to infinite alphabets has been considered in the context of symbolic alternating finite automata (s-AFA), whose transitions are labeled with guards taken from a decidable theory of the data domain [5]. As in our model, s-AFA are closed under union, intersection and complement and emptiness is decidable, due to the lack of registers. However, s-AFA are strictly less expressive than our model, because comparing data at different positions in the input word is not possible.

Constrained Horn clauses (CHC) are a branching computation model widespread in program verification [9]. The main difference between alternating and bottom-up branching computations is that, in an alternating model, all branches of the computation must synchronize on the same input word. With this in mind, it is possible to express emptiness of first-order alternating automata as the existence of solutions of a CHC over a higher-order theory of data, extended with algebraic data types (lists). The effectiveness of such an encoding depends on the effectiveness of interpolation and witness term generation for theories of algebraic data types [11].

The alternating automata model presented in this paper extends the alternating automata with variables ranging over infinite data considered in [14]. There all variables were required to be observable in the input. We overcome this restriction by allowing internal (invisible) variables. Another closely related work [13] considers an inclusion between an asynchronous product of automata \(A_1 \times \ldots \times A_n\), extended with data variables, and a monitor automaton B. The semi-algorithm defined there was based on the assumption that all variables of the observer B must be declared in the automata \(A_1, \ldots , A_n\) under check. This limitation can now be bypassed, since the inclusion problem can be encoded as emptiness of a first-order alternating automaton and, moreover, the emptiness checking semi-algorithm can handle invisible variables.

The work probably closest to ours concerns the model of predicate automata (PA) [6, 7, 17], used in the verification of parameterized concurrent programs with shared memory. In this model, the alphabet consists of pairs of program statements and thread identifiers and is considered infinite because the number of threads is unbounded. Since thread identifiers can only be compared for equality, the data theory in PA is the theory of equality. Even with this simplification, the emptiness problem is undecidable when either the predicates have arity greater than one [6] or use quantified transition rules [17]. Checking emptiness of quantifier-free PA is possible semi-algorithmically, by explicitly enumerating reachable configurations and checking coverage by looking for permutations of argument values. However, no semi-algorithm has been given for quantified PA. Dealing with quantified transition rules is one of our contributions.

Let \(\varSigma \) be a finite alphabet \(\varSigma \) of input events. Given a finite set of variables \(X \subseteq \mathsf {Var}\), we denote by \(X \mapsto \mathbb {D}\) the set of valuations of the variables X and \(\varSigma [X] = \varSigma \times (X \mapsto \mathbb {D})\) be the possibly infinite set of data symbols \((a,\nu )\), where a is an input symbol and \(\nu \) is a valuation. A data word (simply called word in the following) is a finite sequence \(w=(a_1,\nu _1)(a_2,\nu _2) \ldots (a_n,\nu _n)\) of data symbols. Given a word w, we denote by its sequence of input events and by \({w}_\mathbb {D}\) the valuation associating each time-stamped variable \({x}^{\scriptscriptstyle {({i})}}\), where \(x \in \mathsf {Var}\), the value \(\nu _i(x)\), for all \(i\in [1,n]\). We denote by \(\varepsilon \) the empty sequence, by \(\varSigma ^*\) the set of finite input sequences and by \(\varSigma [X]^*\) the set of finite data words over the variables X.

A first-order alternating automaton is a tuple \(\mathcal {A}= \langle \varSigma ,X,Q,\iota ,F,\varDelta \rangle \), where \(\varSigma \) is a finite set of input events, X is a finite set of input variables, Q is a finite set of predicates denoting control states, \(\iota \in \mathsf {Form}^+(Q,\emptyset )\) is a sentence defining initial configurations, \(F \subseteq Q\) is the set of predicates denoting final states and \(\varDelta \) is a set of transition rules. A transition rule is of the form \(q(y_1,\ldots ,y_{\#(q)}) \xrightarrow {{\scriptscriptstyle a(X)}}_{{\scriptstyle }} \psi \), where \(q \in Q\) is a predicate, \(a \in \varSigma \) is an input event and \(\psi \in \mathsf {Form}^+(Q,X \cup \{ y_1,\ldots ,y_{\#(q)} \})\) is a positive formula, where \(X\,\cap \,\{ y_1,\ldots ,y_{\#(q)} \} = \emptyset \). Without loss of generality, we consider, for each predicate \(q \in Q\) and each input event \(a \in \varSigma \), at most one such rule, as two or more rules can be joined using disjunction. The quantifiers occurring in the right-hand side formula of a transition rule are called transition quantifiers. The size of \(\mathcal {A}\) is \({|{\mathcal {A}}|}\) .

The semantics of first-order alternating automata is analogous to the semantics of propositional alternating automata, with rules of the form \(q \xrightarrow {{\scriptscriptstyle a}}_{{\scriptstyle }} \phi \), where q is a propositional variable and \(\phi \) a positive boolean combination of propositional variables. For instance, \(q_0 \xrightarrow {{\scriptscriptstyle a}}_{{\scriptstyle }} (q_1 \wedge q_2) \vee q_3\) means that the automaton can choose to transition in either both \(q_1\) and \(q_2\) or in \(q_3\) alone. This leads to defining transitions as the minimal models of the right hand side of a rule¹. The original definition of alternating automata [4] works around this problem and considers boolean valuations instead of formulae. In contrast, a finite description of a first-order alternating automaton cannot be given in terms of interpretations, as a first-order formula may have infinitely many models, corresponding to infinitely many initial or successor states occurring within an execution step.

Given an uninterpreted predicate symbol \(q \in Q\) and data values \(d_1,\ldots ,d_{\#(q)} \in \mathbb {D}\), the tuple \((q, d_1,\ldots ,d_{\#(q)})\) is called a configuration, sometimes written \(q(d_1,\ldots ,d_{\#(q)})\), when no confusion arises. A configuration is final if \(q \in F\). An interpretation \(\mathcal {I}\) corresponds to a set of configurations , called a cube. This notation is lifted to sets of configurations in the usual way.

An execution \(\mathcal {T}\) over w, starting with c, is accepting if and only if all paths in \(\mathcal {T}\) have the same length and the frontier of each tree \(T \in \mathcal {T}\) is labeled with final configurations. If \(\mathcal {A}\) has an accepting execution over w starting with a cube \(c \in \mathsf {c}({\mathbf{[\![}\iota \mathbf{]\!]}^\mu })\), then \(\mathcal {A}\) accepts w and let \({\mathcal L}({\mathcal {A}})\) be the set of words accepted by \(\mathcal {A}\). For example, consider the automaton \(\mathcal {A}= \langle \{ a \}, \{ x \}, \{ q_0,q_1,q_2,q_f \}, q_0(0), \{ q_f \}, \varDelta \rangle \), where \(\varDelta \) is the set: \(q_0(y) \xrightarrow {{\scriptscriptstyle a(x)}}_{{\scriptstyle }} q_1(y+x) \wedge q_2(y-x)\), \(q_1(y) \xrightarrow {{\scriptscriptstyle a(x)}}_{{\scriptstyle }} q_1(y+x) \vee (y > 0 \wedge q_f)\) and \(q_2(y) \xrightarrow {{\scriptscriptstyle a(x)}}_{{\scriptstyle }} q_2(y-x) \vee (y > 0 \wedge q_f)\). A possible execution tree of this automaton is the following:

The execution tree is not accepting, since its frontier is not labeled with final configurations everywhere. Incidentally, here we have \({\mathcal L}({\mathcal {A}}) = \emptyset \), which is proved by our tool in \(\sim \!0.5\) s on an average machine.

In the rest of this paper, we are concerned with the following problems:

For technical reasons, we address the following problem next: given an automaton \(\mathcal {A}\) and an input sequence \(\alpha \in \varSigma ^*\), does there exists a word \(w \in {\mathcal L}({\mathcal {A}})\) such that \({w}_\varSigma = \alpha \) ? By solving this problem first, we develop the machinery required to prove that first-order alternating automata are closed under complement and, further, set up the ground for developping a practical semi-algorithm for the emptiness problem.

The emptiness problem is undecidable even for automata with predicates of arity two, whose transition rules use only equalities and disequalities, having no transition quantifiers [6]. Since even such simple classes of alternating automata have no general decision procedure for emptiness, we use an abstraction-refinement semi-algorithm based on lazy annotation [20, 21]. In a nutshell, a lazy annotation procedure systematically explores the set of finite input event sequences searching for an accepting execution. For an input sequence, if the path formula is satisfiable, we compute a word in the language of the automaton, from the model of the path formula. Otherwise, i.e. the sequence is spurious, the search backtracks and each position in the sequence is annotated with an interpolant, thus marking the sequence as infeasible. The semi-algorithm uses moreover a coverage relation between sequences, ensuring that the continuations of already covered sequences are never explored. Sometimes this coverage relation provides a sound termination argument, in case when the automaton is empty.

For two input event sequences \(\alpha , \beta \in \varSigma ^*\), we say that \(\alpha \) is a prefix of \(\beta \), written \(\alpha \preceq \beta \), if \(\alpha =\beta \gamma \) for some sequence \(\gamma \in \varSigma ^*\). A set S of sequences is prefix-closed if for each \(\alpha \in S\), if \(\beta \preceq \alpha \) then \(\beta \in S\), and complete if for each \(\alpha \in S\), there exists \(a \in \varSigma \) such that \(\alpha a \in S\) if and only if \(\alpha b \in S\) for all \(b \in \varSigma \). A prefix-closed set is the backbone of a tree whose edges are labeled with input events. If the set is, moreover, complete, then every node of the tree has either zero successors, in which case it is called a leaf, or it has a successor edge labeled with a for each input event \(a \in \varSigma \).

Lazy annotation semi-algorithms [20, 21] build unfoldings of automata trying to discover counterexamples for emptiness. If the automaton \(\mathcal {A}\) in question is non-empty, a systematic enumeration of the input event sequences² from \(\varSigma ^*\) will suffice to discover a word \(w \in {\mathcal L}({\mathcal {A}})\), provided that the first-order theory of the data domain \(\mathbb {D}\) is decidable (Lemma 2). However, if \({\mathcal L}({\mathcal {A}}) = \emptyset \), the enumeration of input event sequences may, in principle, run forever. The typical way of fighting this divergence problem is to define a coverage relation between the nodes of the unfolding tree.

A lazy annotation semi-algorithm will stop and report emptiness provided that it succeeds in building a closed and safe unfolding of the automaton. Notice that, by Definition 3, for any three nodes of an unfolding U, say \(\alpha ,\beta ,\gamma \in \mathrm {dom}(U)\), if \(\alpha \prec \beta \) and \(\alpha \sqsubseteq \gamma \), then \(\beta \sqsubseteq \gamma \) as well. As we show next (Theorem 2), there is no need to expand covered nodes, because, intuitively, there exists a word \(w \in {\mathcal L}({\mathcal {A}})\) such that \(\alpha \preceq {w}_\varSigma \) and \(\alpha \sqsubseteq \gamma \) only if there exists another word \(u \in {\mathcal L}({\mathcal {A}})\) such that \(\gamma \preceq {u}_\varSigma \). Hence, exploring only those input event sequences that are continuations of \(\gamma \) (and ignoring those of \(\alpha \)) suffices in order to find a counterexample for emptiness, if one exists.

An unfolding node \(\alpha \in \mathrm {dom}(U)\) is said to be spurious if and only if \(\varUpsilon ({\alpha })\) is unsatisfiable. In this case, we change (refine) the labels of (some of the) prefixes of \(\alpha \) (and that of \(\alpha \)), such that \(U(\alpha )\) becomes \(\bot \), thus indicating that there is no real execution of the automaton along that input event sequence. As a result of the change of labels, if a node \(\gamma \preceq \alpha \) used to cover another node from \(\mathrm {dom}(U)\), it might not cover it with the new label. Therefore, the coverage relation has to be recomputed after each refinement of the labeling. The semi-algorithm stops when (and if) a safe complete unfolding has been found.

We describe the semi-algorithm used to check emptiness of first-order alternating automata. The execution of Algorithm 1 consists of three phases, corresponding to the Close, Refine and Expand of the original IMPACT procedure [20]. Let n be a node removed from the worklist at line 2 and let \(\alpha (n)\) be the input sequence labeling the path from the root node to n. If \(\overline{\varUpsilon }({\alpha (n)})\) is satisfiable, the sequence \(\alpha (n)\) is feasible, in which case a model of \(\overline{\varUpsilon }({\alpha (n)})\) is obtained and a word \(w \in L(\mathcal {A})\) is returned. Otherwise, \(\alpha (n)\) is an infeasible input sequence and the procedure enters the refinement phase (lines 9–19). The GLI for \(\alpha (n)\) is used to strenghten the labels of all the ancestors of n, by conjoining the formulae of the interpolant, changed according to Lemma 7, to the existing labels.

In this process, the nodes on the path between \(\mathtt {r}\) and n, including n, might become eligible for coverage, therefore we attempt to close each ancestor of n that is impacted by the refinement (line 19). Observe that, in this case the call to must uncover each node which is covered by a successor of n (line 30 of the function). This is required because, due to the over-approximation of the sets of reachable configurations, the covering relation is not transitive, as explained in [20]. If adds a covering edge \((n_i,m)\) to \(\lhd \), it does not have to be called for the successors of \(n_i\) on this path, which is handled via the boolean flag b. Finally, if n is still uncovered (it has not been previously covered during the refinement phase) we expand n (lines 21–25) by creating a new node for each successor s via the input event \(a \in \varSigma \) and inserting it into the worklist.

Typically, when checking the unreachability of a set of program configurations, the interpolants used to annotate the unfolded control structure are assertions about the values of the program variables in a given control state, at a certain step of an execution [20]. Because we consider alternating computation trees (forests), we must distinguish between (i) locality of interpolants w.r.t. a given control state (control locality) and (ii) locality w.r.t. a given time stamp (time locality). In logical terms, control-local interpolants are formulae involving a single predicate symbol, whereas time-local interpolants involve only predicates \({q}^{\scriptscriptstyle {({i})}}\) and variables \({x}^{\scriptscriptstyle {({i})}}\), for a single \(i \ge 0\). When considering alternating executions, control-local interpolants are not always enough to prove emptiness, because of the synchronization of several branches of the computation on the same input word. For this reason, the interpolants considered in this paper will never be control-local and we shall use the term local to denote time-local interpolants, with no free variables.

First, let us give the formal definition of the class of interpolants we shall work with. Given a formula \(\phi \), the vocabulary of \(\phi \), denoted \(\mathrm {V}({\phi })\) is the set of predicate symbols \(q \in {Q}^{\scriptscriptstyle {({i})}}\) and variables \(x \in {X}^{\scriptscriptstyle {({i})}}\), occurring in \(\phi \), for some \(i\ge 0\). For a term t, its vocabulary \(\mathrm {V}({t})\) is the set of variables that occur in t. Observe that quantified variables and the interpreted function symbols of the data theory³ do not belong to the vocabulary of a formula. By \(\mathrm {P}^{+}(\phi )\) [\(\mathrm {P}^{-}(\phi )\)] we denote the set of predicate symbols that occur in \(\phi \) under an even [odd] number of negations.

In the rest of this section, fix an automaton \(\mathcal {A}= \langle \varSigma ,X,Q,\iota ,F,\varDelta \rangle \). The following definition generalizes interpolants from unsatisfiable conjunctions to input sequences:

The following proposition states the existence of local GLI for the theories in which Lyndon’s Interpolation Theorem holds.

A problematic point of the above proposition is that the existence of Lyndon interpolants (Definition 4) is proved in principle, but the proof is non-constructive. In other words, the proof of Proposition 1 does not yield an algorithm for computing GLIs, for the following reason. Building an interpolant for an unsatisfiable conjunction of formulae \(\phi \wedge \psi \) is typically the job of the decision procedure that proves the unsatisfiability and, in general, there is no such procedure, when \(\phi \) and \(\psi \) contain predicates and have non-trivial quantifier alternation. In this case, some provers use instantiation heuristics for the universal quantifiers that are sufficient for proving unsatisfiability, however these heuristics are not always suitable for interpolant generation. Consequently, from now on, we assume the existence of an effective Lyndon interpolation procedure only for decidable theories, such as the quantifier-free linear (integer) arithmetic with uninterpreted functions (UFLIA, UFLRA, etc.) [26].

This is where the predicate-free path formulae (defined in Sect. 2.1) come into play. Recall that, for a given event sequence \(\alpha \), the automaton \(\mathcal {A}\) accepts a word w such that \({w}_\varSigma = \alpha \) if and only if \(\overline{\varUpsilon }({\alpha })\) is satisfiable (Lemma 5). Assuming further that the equality and interpreted predicates (e.g. inequalities for integers) atoms from the transition rules of \(\mathcal {A}\) belong to a decidable first-order theory, such as Presburger arithmetic, Lemma 5 gives us an effective way of checking emptiness of \(\mathcal {A}\), relative to a given event sequence. However, this method does not cope well with lazy annotation, because there is no way to extract, from the unsatisfiability proof of \(\overline{\varUpsilon }({\alpha })\), the interpolants needed to annotate \(\alpha \). This is because (I) the formula \(\overline{\varUpsilon }({\alpha })\), obtained by repeated substitutions loses track of the steps of the execution, and (II) quantifiers that occur nested in \(\overline{\varUpsilon }({\alpha })\) make it difficult to write \(\overline{\varUpsilon }({\alpha })\) as an unsatisfiable quantifier-free conjunction of formulae from which interpolants are extracted (Definition 4).

The solution we adopt for the first issue (I) consists in partially recovering the time-stamped structure of the acceptance formula \(\varUpsilon ({\alpha })\) using the formula \(\widehat{\varUpsilon }({\alpha })\), in which only transition quantifiers occur. The second issue (II) is solved under the additional assuption that the theory of the data domain \(\mathbb {D}\) has witness-producing quantifier elimination. More precisely, we assume that, for each formula \(\exists x~.~\phi (x)\), there exists an effectively computable term \(\tau \), in which x does not occur, such that \(\exists x~.~\phi \) and \(\phi [\tau /x]\) are equisatisfiable. These terms, called witness terms in the following, are actual definitions of the Skolem function symbols from the following folklore theorem:

Examples of witness-producing quantifier elimination procedures can be found in the literature for e.g. linear integer (real) arithmetic (LIA,LRA), Presburger arithmetic and boolean algebra of sets and Presburger cardinality constraints (BAPA) [18].

Under the assumption that witness terms can be effectively built, we describe the generation of a non-local GLI for a given input event sequence \(\alpha = a_1 \ldots a_n\). First, we generate successively the acceptance formula \(\varUpsilon ({\alpha })\) and its equisatisfiable forms \(\widehat{\varUpsilon }({\alpha }) = Q_1x_1 \ldots Q_mx_m~.~\widehat{\varPhi }\) and \(\overline{\varUpsilon }({\alpha }) = Q_1x_1 \ldots Q_mx_m~.~\overline{\varPhi }\), both written in prenex form, with matrices \(\widehat{\varPhi }\) and \(\overline{\varPhi }\), respectively. Because we assumed that the first order theory of \(\mathbb {D}\) has quantifier elimination, the satisfiability problem for \(\overline{\varUpsilon }({\alpha })\) is decidable. If \(\overline{\varUpsilon }({\alpha })\) is satisfiable, we build a counterexample for emptiness w such that \({w}_\varSigma =\alpha \) and \({w}_\mathbb {D}\) is a satisfying assignment for \(\overline{\varUpsilon }({\alpha })\). Otherwise, \(\overline{\varUpsilon }({\alpha })\) is unsatisfiable and there exist witness terms \(\tau _{i_1} \ldots \tau _{i_\ell }\), where \(\{ i_1, \ldots , i_\ell \} = \{ j \in [1,m] \mid Q_j = \forall \}\), such that \(\overline{\varPhi }[\tau _{i_1}/x_{i_1}, \ldots , \tau _{i_\ell }/x_{i_\ell }]\) is unsatisfiable (Theorem 3). Then it turns out that the formula \(\widehat{\varPhi }[\tau _{i_1}/x_{i_1}, \ldots , \tau _{i_\ell }/x_{i_\ell }]\), obtained analogously from the matrix of \(\widehat{\varUpsilon }({\alpha })\), is unsatisfiable as well (Lemma 6 below). Because this latter formula is structured as a conjunction of formulae \({\iota }^{\scriptscriptstyle {({0})}} \wedge \phi _1 \ldots \wedge \phi _n \wedge \psi \), where \(\mathrm {V}({\phi _k}) \cap {Q}^{\scriptscriptstyle {({\le n})}} \subseteq {Q}^{\scriptscriptstyle {({k-1})}} \cup {Q}^{\scriptscriptstyle {({k})}}\) and \(\mathrm {V}({\psi }) \cap {Q}^{\scriptscriptstyle {({\le n})}} \subseteq {Q}^{\scriptscriptstyle {({n})}}\), it is now possible to use an existing interpolation procedure for the quantifier-free theory of \(\mathbb {D}\), extended with uninterpreted function symbols, to compute a (not necessarily local) GLI \((I_0, \ldots , I_n)\) such that \(\mathrm {V}({I_k}) \cap {Q}^{\scriptscriptstyle {({\le n})}} \subseteq {Q}^{\scriptscriptstyle {({k})}}\), for all \(k \in [n]\).

We formalize and prove the correctness for the above construction of non-local GLI. A function \(\xi : \mathbf{\mathbb {N}}\rightarrow \mathbf{\mathbb {N}}\) is monotonic iff for each \(n < m\) we have \(\xi (n) \le \xi (m)\) and finite-range iff for each \(n \in \mathbf{\mathbb {N}}\) the set \(\{ m \mid \xi (m)=n \}\) is finite. If \(\xi \) is finite-range, we denote by \(\xi _{\max }^{-1}(n) \in \mathbf{\mathbb {N}}\) the maximal value m such that \(\xi (m)=n\).

Consequently, under two assumptions about the first-order theory of the data domain, namely (i) witness-producing quantifier elimination, and (ii) Lyndon interpolation for the quantifier-free fragment with uninterpreted functions, we developed a generic method that produces GLIs for unfeasible input event sequences. Moreover, each formula in the interpolant refers only to the current predicate symbols, the current and past input variables and the existentially quantified transition variables introduced at the previous steps. The remaining questions are how to use these GLIs to label the sequences in the unfolding of an automaton (Definition 2) and compute coverage (Definition 3) between nodes of the unfolding.

We have implemented a version of the IMPACT semi-algorithm [20] in a prototype tool, avaliable online [8]. The tool is written in Java and uses the Z3 SMT solver [27], via the JavaSMT interface [15], for spuriousness and coverage queries and also for interpolant generation. Table 1 reports the size of the input automaton in bytes, the numbers of Predicates, Variables and Transitions, the result of emptiness check, the number of Expanded and Visited Nodes during the unfolding and the Time in miliseconds. The experiments were carried out on a MacOS x64 - 1.3 GHz Intel Core i5 - 8 GB 1867 MHz LPDDR3 machine.

The test cases shown in Table 1, come from several sources, namely predicate automata models (*.pa) [6, 7] available online [23], timed automata inclusion problems (abp.ada, train.ada, rr-crossing.foada), array logic entailments (array_rotation.ada, array_simple.ada, array_shift.ada) and hardware circuit verification (hw1.ada, hw2.ada), initially considered in [13], with the restriction that local variables are made visible in the input. The train-simpleN. foada and fischer-mutexN. foada examples are parametric verification problems in which one checks inclusions of the form \(\bigcap _{i=1}^N{\mathcal L}({A_i}) \subseteq {\mathcal L}({B})\), where \(A_i\) is the i-th copy of the template automaton.

The advantage of using FOADA over the INCLUDER [12] tool from [13] is the possibility of having automata over infinite alphabets with local variables, whose values are not visible in the input. In particular, this is essential for checking inclusion of timed automata that use internal clocks to control the computation.

We present first-order alternating automata, a model of computation that generalizes classical boolean alternating automata to first-order theories. Due to their expressivity, first-order alternating automata are closed under union, intersection and complement. However the emptiness problem is undecidable even in the most simple case, of the quantifier-free theory of equality with uninterpreted predicate symbols. We deal with the emptiness problem by developping a practical semi-algorithm that always terminates, when the automaton is not empty. In case of emptiness, termination of the semi-algorithm occurs in most practical test cases, as shown by a number of experiments.