Keywords: Model Checking, Verification, Emptiness, Language Inclusion, Alternating, Infinite Alphabets, IMPACT ) . . . . . . . . . . . . . . . Predicate Automata (PA) . . .

The language inclusion problem is recognised as being central to verification in different domains, such as hardware, communication protocols, software systems, etc. There we might face two challenges: non-determinism and infinite alphabets.

We propose two models of alternating automata over infinite alphabets: (i) alternating data automata (ADA) and (ii) first-order alternating data automata (FOADA). They both recognise the data words over infinite alphabets. In ADA model, the control states are Booleans and the transition rules are specified by a set of formulae in a combined first-order theory of states (Booleans) and data that relate past values of variables with current values of variables. But a restriction of the ADA model is that, there is not hidden variable, hence all the data values taken by the variables are visible in the input. But in FOADA model, the arguments of a predicate atom track the values of the internal variables associated with the state, and these values are invisible in the input sequence, which overcomes the restriction of the ADA model.

With these two alternating models, Boolean operations of union, intersection and complement can be done in linear time, thus matching the complexity of performing these operations in the finite-alphabet case. However, the price to be paid here is that the emptiness checking becomes undecidable. For this reason, we provide two efficient semi-algorithms for emptiness checking: (i) lazy predicate abstraction [START_REF] Henzinger | Lazy abstraction[END_REF] and (ii) IMPACT method [START_REF] Kenneth | Lazy abstraction with interpolants[END_REF]. These semi-algorithms are proven to terminate by returning a word from the language of the given automaton if one exists; but if the language of the given automaton is empty, then the termination is not guaranteed.

The main application of our models is checking inclusions between various classes of automata extended with variables ranging over infinite domains that recognise languages over infinite alphabets. The most widely known classes of this kind are timed automata and finitememory (register) automata. Another application is checking safety (mutual exclusion, absence of deadlocks, etc.) and liveness (termination, lack of starvation, etc.) properties of parameterised concurrent programs.

Besides the theoretical parts, we also have developed a tool -FOADA Checker [START_REF] Xu | Foada checker[END_REF], mainly used for checking inclusion between two automata or checking emptiness of an automaton. FOADA Checker is written in Java, via Java-SMT interface [START_REF]Java smt[END_REF] and using Z3 SMT solver [START_REF]Z3 smt solver[END_REF] for spuriousness, coverage queries and interpolant generation. The IMPACT semi-algorithm [START_REF] Kenneth | Lazy abstraction with interpolants[END_REF] has been implemented in the tool to check the emptiness of an automaton.

Résumé

Le problème de l'inclusion linguistique est reconnu comme étant au coeur de la vérification dans différents domaines, tels que le matériel, les protocoles de communication, les systèmes logiciels, etc. Nous pouvons être confrontés à deux défis: le non-déterminisme et les alphabets infinis.

Nous proposons deux modèles d'automates alternatifs sur des alphabets infinis : (i) les automates alternatifs de données (ADA) et (ii) les automates alternatifs de données du premier ordre (FOADA). Ils reconnaissent tous deux les mots de données sur des alphabets infinis. Dans le modèle ADA, les états de contrôle sont des booléens et les règles de transition sont spécifiées par un ensemble de formules combinées dans une théorie des états du premier ordre (booléens) et des données associant les valeurs passées des variables aux valeurs actuelles des variables. Mais le modèle ADA a une restriction : il n'y a pas de variable cachée, ainsi toutes les valeurs de données prises par les variables sont visibles dans l'entrée. Pourtant dans le modèle FOADA, les arguments d'un atome de prédicat tracent les valeurs des variables internes associées à l'état, et ces valeurs sont invisibles dans la séquence d'entrée, ce qui surmonte la restriction du modèle ADA.

Avec ces deux modèles en alternance, les opérations booléennes d'union, d'intersection et de complément peuvent être effectuées en temps linéaire, ce qui correspond à la complexité de l'exécution de ces opérations dans le cas d'un alphabet fini. Cependant, le prix à payer ici est que la vérification du vide devient indécidable. Pour ceci, nous fournissons deux semi-algorithmes efficaces pour la vérification du vide : (i) abstraction de prédicats paresseux [START_REF] Henzinger | Lazy abstraction[END_REF] et (ii) méthode IMPACT [START_REF] Kenneth | Lazy abstraction with interpolants[END_REF]. S'il existe un mot du langage de l'automate donné, il est prouvé que ces semialgorithmes se terminent en le retournant; mais si la langue de l'automate donné est vide, la terminaison n'est pas garantie.

La principale application de nos modèles est de vérifier l'inclusion entre différentes classes d'automates étendues avec des variables allant de domaines infinis reconnaissant les langues à des alphabets infinis. Les plus connues de ce genre de classes sont les automates temporisés et les automates à mémoire finie (registre). Une autre application est de vérifier les propriétés de sécurité (exclusion mutuelle, absence de blocages, etc.) et de vitalité (résiliation, absence de famine, etc.) des programmes concurrents paramétrés.

Outre les parties théoriques, nous avons également développé un outil -FOADA Checker [START_REF] Xu | Foada checker[END_REF], en général à l'usage de la vérification de l'inclusion entre deux automates ou de la vérification du vide d'un automate. FOADA Checker est écrit en Java, via l'interface Java-SMT [START_REF]Java smt[END_REF] et en utilisant le solveur Z3 SMT [START_REF]Z3 smt solver[END_REF] pour les parasites, les requêtes de couverture et la génération d'interpolation. Le semi-algorithme IMPACT [START_REF] Kenneth | Lazy abstraction with interpolants[END_REF] a été implémenté dans l'outil pour vérifier le vide d'un automate.

Mots-Clés: Vérification de Modèle, Vérification, Vide, Inclusion Linguistique, Alternance, Alphabets Infinis, IMPACT Chapter 1

Introduction 1.1 Motivation

The growth in complexity of designs increases the importance of system verification techniques in many domains, such as hardware [START_REF] Zerksis | Formal verification of a real-time hardware design[END_REF], software engineering, transportation, banking, telecommunications, national defence, aerospace and aeronautical engineering, etc. This could be attributed to important safety requirements where errors either have huge commercial significance, or even lead to life-threatening situations such as in the transport systems, power plants and so forth.

The system verification aims at using formal proofs to demonstrate that a system meets a certain specification. According to the needs, we pick up interesting information from the description of a system or a specification, which is usually written in natural languages, and then, we can use this filtered information to re-describe the system or the specification in an abstract way under a certain specific concept, which is called a model. A model is an abstraction that helps to explain a system or a specification, and can be used for studying the effects of different components or for making predictions about behaviour.

Finite-state automaton (FSA) is a largely used model for verification. It is a mathematical model of computation in which different states of the system (or the specification) are defined as the states of the model. The behaviour of the system (or the specification) is represented by discrete state changes, called transitions. The transitions of the model are triggered by actions or events, formally called input symbols. A word is a sequence of input symbols. Taking one by one the input symbol from a word and starting from the initial state of the model, if there exists an execution that leads to a final state of the model, then the word is accepted by the model. The set of all the words accepted by a model A is called the language of A, often denoted as L(A). In addition, the set of all possible input symbols is called the alphabet of the model, usually denoted by Σ, and Σ * is the set of finite words with symbols from Σ.

Example 1.1 (Automaton for System) In a chemical production line, starting with an empty bottle, we add chemical product in the bottle, and in the end we put a cap on. There are two types of product: A and B; and there are two types of caps: normal cap and special cap. The bottles with different products must use different caps and Table 1.1 shows the type specification of the cap for different products.

Product

Cap A Normal B Special A + B Special Table 1.1: Cap Type Specification for Different Products

The finite-state automaton in Figure 1.1 explains how a complete chemical product is produced in this chemical production line. Given a system that has already been modelled by an automaton, we can build automata for the specifications that we want to check for the given system, over the same alphabet, hence the same actions (or events) for both system and specifications.

Example 1.2 (Automaton for Specification) For the chemical production line in Example 1.1, a recent study shows that the product B is toxic. For all the bottles containing the product B, the special caps are necessary. Figure 1.2 describes the safe production specification where any bottle containing toxic product (the product B) does have a special cap when the production is over. If all the words that are accepted by the system model are also accepted by the given specification, then the system meets the given specification. In other words, if we can prove that the language of the system model is included in the language of the specification, then the verification problem is solved. Hence, the verification problem is a language inclusion problem.

NON-TOXIC

There exists a classical solution (Figure 1.3) to solve the language inclusion problem. Instead of checking language inclusion between two automata A and B over an alphabet Σ, we firstly build a new automaton B, called the complement of B, whose language is the complement of the language of B over the set of all available words Σ * , so L(B) = Σ * -L(B); and then we check whether the intersection between L(A) and L(B) is empty, so check if L(A) ∩ L(B) = ∅. Hence, the verification problem in which we check whether a system S meets a given property P (hence check whether S |= P), can be transformed into an emptiness problem of the intersection between (i) the language of system model L(M S ) and (ii) the complement of the language of the property L(M P ), so check whether L(M S ) ∩ L(M P ) = ∅.

Non-Determinism

A finite state automaton is called a deterministic finite automaton (DFA) if each of its transitions is uniquely determined by its source state and input symbol, and reading an input symbol is required for each transition. Hence, for any input, the deterministic finite state automaton produces a unique computation 1 . A non-deterministic finite automaton (NFA) 2does not need to obey the restrictions above. In other words, for any non-deterministic finite automaton, from a given state, if we take an input symbol, there can be several possible next states. Section 2.2 provides more details about NFA and DFA.

If we transform the verification problem into an emptiness problem (Figure 1.4), then we have to complement the automaton of the specification. Complementing a DFA can be simply done by just flipping the final states and the non-final states, but if the automaton is nondeterministic, then this method does not work.

Example 1.3 If we complement the NFA in Figure 1.5.left by just flipping the final states and the non-final states, then we obtain the NFA in Figure 1.5.right. But both of them accept the word "a", hence the complementation in this way is not correct. One classical technique to deal with the non-determinism is converting a non-deterministic automaton into a deterministic automaton that recognises the same language [START_REF] Rabin | Finite automata and their decision problems[END_REF], by power-set construction (also called subset construction). However, if a non-deterministic automaton has n states, then the resulting deterministic automaton by subset construction may have up to 2 n states, an exponentially larger number, which makes the construction impractical for large automata.

Infinite Alphabets

When dealing with real-life systems, the models usually handle data from very large domains that can be assumed to be infinite, such as 64-bit integers, floating point numbers, strings of characters, etc. The correctness of this kind of systems must be specified in terms of data values. Alternatively, sometimes the systems must respond to strict deadlines, which requires temporal specifications expressed in terms of timed languages [START_REF] Alur | A theory of timed automata[END_REF].

Example 1.5 Giving two integer arrays X and Y , as in Figure 1.7.left: (i)

X 0 = 1; (ii) Y 0 = 1; (iii) ∀i > 0 : X i = Y i-1 , Y i = X i-1 + Y i-1 .
We want to check whether these two arrays meet the specification, as in Figure 1.7.right: ∀i > 0 :

X i > X i-1 , Y i > Y i-1 .
Here, using finite alphabets is not enough since integer is an infinite data domain. There exist some classical automata that can, to some extent, handle infinite alphabets, such as timed automata [START_REF] Alur | A theory of timed automata[END_REF] and finite-memory (register) automata [START_REF] Kaminski | Finite-memory automata[END_REF]. But they both face the closure problem for the complementation due to their infinite alphabets. In other words, for these two kinds of automata, there exist automata for which the complement language cannot be recognised by an automaton in the same class. This excludes the possibility to transform the inclusion problem into the emptiness problem.

0 1 2 3 … 1 1 2 3 … 1 2 3 5 … X Y … i -1 i i + 1 … … >X i-2 >X i-1 >X i … … >Y i-2 >Y i-1 >Y i … X Y

State-of-the-Art 1.3.1 Solutions for Non-Determinism

As mentioned before, the NFA may need to be determinised in order to be complemented. However, this determinisation may cause an exponential blow-up in the number of states. This is the context in which alternation [START_REF] Ashok | [END_REF] has been introduced.

One classical alternating model is alternating finite automata (AFA) [START_REF] Ashok | [END_REF], where the transitions are divided into existential (OR-relation, disjunctive branching) transitions and universal (AND-relation, conjunctive branching) transitions. In AFA, we also allow the formulae true and f alse. We will introduce more about AFA in Section 2.4, and note that, the complementation of an AFA can be done in linear time, since (i) we flip the final states and the non-final states and this operation is linear; (ii) we flip ∧ and ∨ in the transition rules and this operation is linear.

Example 1.7 The automaton in Figure 1.9 is an alternating finite automaton. The transition rules are: (i)

X a -→ Y ∧ Z (ii) Y a -→ Y (iii) Y b - → Y (iv) Z b - → X ∨ Y .

Solutions for Infinite Alphabets

Using finite alphabets for the models and the specifications is very restrictive when dealing with real-life systems. However, there exist some classical models that can, to some extent, handle infinite alphabets.

One classical model is timed automata [START_REF] Alur | A theory of timed automata[END_REF], which can capture several interesting aspects of real-time systems, including some qualitative features such as liveness, fairness and nondeterminism, as well as some quantitative features such as periodicity, bounded response and timing delays. Timed automata accept timed words -possibly infinite sequences in which a real-valued time of occurrence is associated with each symbol. A timed automaton is a finite automaton with a finite set of real-valued clocks. The clocks can be reset to 0 independently of each other with the transitions of the automaton, and keep track of the time elapsed since the last reset. The transitions of the automaton may impose certain constraints on clock values, such that a transition may be taken only if the current values of the clocks satisfy the associated constraints. Language inclusion is generally undecidable3 for timed automata. Moreover, the class of timed regular languages is not closed under complementation, this excludes the possibility to transform the inclusion problem into an emptiness problem.

Example 1.8 The timed automaton in Figure 1.10 accepts the language:

{(a ω , τ ) | ∃i ≥ 1.∃j > i.(τ j = τ i + 1)}
where a ω stands for the infinite concatenation of a to itself and τ is a time sequence (hence a sequence of real numbers). The complement of this language cannot be characterised using a timed automaton. The complement needs to make sure that no pair of a is separated by distance 1. Since there is no bound on the number of a that can happen in a time period of length 1, keeping track of the times of all the a within the past 1 time unit would require an unbounded number of clocks. Another model of computation dealing with infinite alphabets, called finite-memory automata [START_REF] Kaminski | Finite-memory automata[END_REF], is a natural generalisation of the classical finite-state automata [START_REF] Rabin | Finite automata and their decision problems[END_REF]. This model is also called register automata. The basic idea behind this model is to equip the automaton with a finite set of registers, called windows. Each window is capable of being empty or storing a symbol from the infinite alphabet. When the automaton takes the next input symbol: (i) if no window contains the input symbol, then it is copied into a specified window depending on the state; (ii) otherwise the test of equality applies. The language inclusion is undecidable for finite-memory automata (register automata). Moreover, this model is generally not closed under complementation, which makes it impossible to transform the inclusion problem into emptiness problem.

Example 1.9 The finite-memory automaton in Figure 1.11 accepts the language:

{σ 1 , σ 2 , ..., σ n : ∃1 ≤ i ≤ j ≤ n.σ i = σ j }
The complement of this language cannot be characterised using a finite-memory automaton. Assume to the contrary that there exists a finite-memory automaton A that accepts the complement of the language above, hence all the words where each symbol appears at most once. Since the alphabet Σ is infinite, there exists a word σ ∈ L(A) of length |A| + 1. We know that A accepts a word σ of length |A| + 1 that contains at most |A| distinct symbols (see proposition 4 in [START_REF] Kaminski | Finite-memory automata[END_REF]), therefore some symbol of Σ must appear in σ more than once, in contradiction with the assumption.

q 0 ,1 q,2 f,2 1 2 1,2 # # 1 1

Figure 1.11: A Non-Complementable Finite-Memory Automaton

Symbolic finite automata (s-FA) [START_REF] Antoni | The power of symbolic automata and transducers[END_REF][START_REF] Tamm | Theoretical aspects of symbolic automata[END_REF] are a model that can also, to some extent, overcome the limitation of only handling finite and small alphabets. Symbolic automata allow transitions to carry predicates and functions over a specified alphabet theory, such as linear arithmetic, and therefore extend finite automata to operate over infinite alphabets, such as the set of rational numbers. If it is decidable to check whether predicates in the algebra are satisfiable, then (i) symbolic automata are closed under Boolean operations and (ii) emptiness and inclusion are decidable. However, this model loses the previous values after each transition since the values cannot be stored in registers or other forms of memory. This excludes the possibility of comparing the current values with the past values.

Example 1.10 The symbolic automaton in Figure 1.12 defines the list of odd numbers with length greater than 1.

Data automata (DA) [START_REF] Iosif | Abstraction refinement and antichains for trace inclusion of infinite state systems[END_REF] are extensions of non-deterministic finite automata (NFA) with variables ranging over a possibly infinite data domain, equipped with a first-order theory. DA model recognises the data words over infinite alphabets consisting of pairs (a, v) where a is an input event from a finite set and v is a valuation of a finite set of variables that range over a possibly infinite data domain. Data automata are closed under the Boolean operations of intersection and complement, and these Boolean operations can be done in linear time. However, the inclusion problem for data automata is undecidable. We introduce more details about data automata in Section 2.5.

Example 1.11 Consider the data automaton in Figure 1.13. There are two transition rules:

(i) P a,x =0∧v =0 --------→ Q and (ii) Q b,x =v+1∧v =x
----------→ Q, where x refers to the current values of x and x refer to the next (new) value of x (idem for v and v ).

x = 1 mod 2 x = 0 mod 2 true x = 1 mod 2 x = 1 mod 2 x = 0 mod 2 x = 0 mod 2 Figure 1.12: A Symbolic Automaton P Q a : x' = 0 ∧ v' = 0 b : x' = v + 1 ∧ v' = x

Solutions for both Non-Determinism and Infinite Alphabets

There exists an alternating model called predicate automata (PA) [START_REF] Farzan | Proof spaces for unbounded parallelism[END_REF][START_REF] Farzan | Proving liveness of parameterized programs[END_REF][START_REF] Kincaid | Parallel proofs for parallel programs[END_REF], in the class of infinite-state automata which recognise languages over an infinite alphabet. This model is used in some works on verification of parameterised concurrent programs with shared memory. In this model, the alphabet consists of pairs of program statements and thread identifiers, thus being infinite because the number of threads is potentially unbounded. The data theory in PA is the theory of equality because thread identifiers can only be compared for equality or disequality. The emptiness problem is undecidable when either (i) the predicates have arity greater than one, or (ii) some transition rule is quantified. Checking emptiness of quantifier-free PA is possible with some semi-algorithms, by explicitly enumerating reachable configurations and checking coverage by looking for permutations of argument values. However, no semi-algorithm exists for quantified PA.

Another alternating model that can, to some extent, handle infinite alphabets, is symbolic alternating finite automata (s-AFA) [START_REF] Antoni | A symbolic decision procedure for symbolic alternating finite automata[END_REF]. The two key-features of s-AFA are that: (i) the alphabet is symbolic, as in a symbolic finite automaton (s-FA) [START_REF] Antoni | The power of symbolic automata and transducers[END_REF]; (ii) the automaton may make use of both existential and universal non-determinism, as in an alternating finite automaton (AFA). For a normal s-AFA, the complementation can be done in linear time, however, for any given s-AFA, the normalisation [START_REF] Antoni | A symbolic decision procedure for symbolic alternating finite automata[END_REF][START_REF] Mcmillan | Applying sat methods in unbounded symbolic model checking[END_REF][START_REF] Veanes | Symbolic automata constraint solving[END_REF] which aims at converting an s-AFA into an equivalent normal s-AFA, may (in the worst case) cause an exponential blow-up in the number of outgoing transitions of any one state in an s-AFA.

Solutions for Language Inclusion

Antichains [START_REF] Doyen | Antichain algorithms for finite automata[END_REF] algorithms or semi-algorithms have been implemented for automata on finite words [START_REF] De Wulf | Antichains: A new algorithm for checking universality of finite automata[END_REF], on finite trees [START_REF] Bouajjani | Antichain-based universality and inclusion testing over nondeterministic finite tree automata[END_REF], on infinite words [START_REF] Doyen | Antichains for the automata-based approach to model-checking[END_REF][START_REF] Fogarty | Büchi complementation and size-change termination[END_REF], and for other applications where exponential constructions are involved such as model-checking of linear-time logic [START_REF] De Wulf | Antichains: Alternative algorithms for ltl satisfiability and model-checking[END_REF], games of imperfect information [START_REF] Chatterjee | Algorithms for omega-regular games with imperfect information[END_REF][START_REF] Berwanger | Strategy construction for parity games with imperfect information[END_REF], and synthesis of linear-time specifications [START_REF] Filiot | An antichain algorithm for ltl realizability[END_REF].

The idea is always to exploit the special structure of the subset constructions. For example, consider the classical subset construction for the complementation of automata on finite words. States of the complement automaton are sets of states of the original automaton, that we call cells and denote by s i . Set inclusion between cells is a partial order that turns out to be a simulation relation for the complement automaton: if s 2 ⊆ s 1 and there is a transition from s 1 to s 3 , then there exists a transition from s 2 to some s 4 ⊆ s 3 . This structural property carries over to the sets of cells manipulated by reachability algorithms: if s 2 ⊆ s 1 and a final cell can be reached from s 1 , then a final cell can be reached from s 2 . Therefore, in a breadth-first search algorithm with backward state traversal, if s 1 is visited by the algorithm, then s 2 is visited simultaneously; the algorithm manipulates ⊆-downward closed sets of cells that can be canonically and compactly represented by the antichain of their ⊆-maximal elements.

There exists also a semi-algorithm described in [START_REF] Iosif | Abstraction refinement and antichains for trace inclusion of infinite state systems[END_REF], which combines the principle of the antichain-based language inclusion algorithm [START_REF] Parosh | When simulation meets antichains[END_REF] with the interpolant-based abstraction refinement semi-algorithm [START_REF] Kenneth | Lazy abstraction with interpolants[END_REF] via a general notion of language-based subsumption relation. This method aims at solving the trace inclusion problem (an instance is shown in Figure 1.14). One of our contributions is a new model of alternating automata over infinite alphabets, called alternating data automata (ADA). Inspired by the data automata (DA) model [START_REF] Bojanczyk | Two-variable logic on data words[END_REF] and related studies [START_REF] Decker | Ordered navigation on multi-attributed data words[END_REF][START_REF] Iosif | Abstraction refinement and antichains for trace inclusion of infinite state systems[END_REF], we extend the DA model to the alternating automata model [START_REF] Vardi | Alternating Automata and Program Verification[END_REF] where the control states become Booleans and the transition rules are specified by a set of formulae in a combined first-order theory of states (Booleans) and data that relate past values of variables with current values of variables. As the DA model does, the ADA model recognises the data words over infinite alphabets consisting of pairs (a, v) where a is an input event from a finite set and v is a valuation of a finite set of variables that range over a possibly infinite data domain.

q 0 i init : x' = 0 v' = 1 q 1 i a i : (i -1)∆ ≤ x < i ∆ x' = x + 1 v' = i ∆' = ∆ A i=1,2,…,N p 0 B p 1 p 2 … p N init : v' = 1 a 2 : v' = v + 1 a 3 : v' = v + 1 a N : v' = v + 1 a 1,2,…,N : v' = v a 2,3,…,N : v' = v a N : v' = v
Example 1.12 Consider the alternating data automaton in Figure 1.15. The transitions are:

(i) X a -→ Y ∧ x = 0 ∧ Z ∧ y = 0 (ii) Y a -→ Y (iii) Y b - → Y (iv) Z b - → X ∧ y = x + 1 ∨ Y ∧ x = y
, where X, Y and Z are Boolean control states, x refers to the current value of x and x refers to the past value of x (idem for y and y). With the ADA model, Boolean operations of union, intersection and complement can be done in linear time, thus matching the complexity of performing these operations in the finitealphabet case. The price to be paid here is that emptiness checking becomes undecidable, this is the reason why we provide two efficient semi-algorithms for emptiness checking. One of these two semi-algorithms is based on lazy predicate abstraction [START_REF] Henzinger | Lazy abstraction[END_REF]; and the other is based on the IMPACT method [START_REF] Kenneth | Lazy abstraction with interpolants[END_REF]. These two semi-algorithms are proven to terminate by returning a word from the language of the automaton if one exists. But if the language of the given automaton is empty, then termination is not guaranteed.

A restriction of the ADA model here is that there is no hidden variable, hence all the data values taken by the variables are visible in the input.

More details about ADA are given in Chapter 3.

First-Order Alternating Data Automata (FOADA)

Another contribution of this thesis is a generalised alternating automata model, called firstorder alternating data automata (FOADA), in which states are predicate symbols, the input is associated with data variables ranging over an infinite data domain and transitions use formulae in the first-order theory of the data domain. As the ADA model does, the FOADA model also recognises the data words over infinite alphabets consisting of pairs (a, v) where a is an input event from a finite set and v is a valuation of a finite set of variables that range over a possibly infinite data domain.

In the FOADA model, the arguments of a predicate atom track the values of the internal variables associated with the state, and these values are invisible in the input sequence. This overcomes the restriction of ADA, and it solves a classical language inclusion problem ∩ n i=1 L(A i ) ⊆ L(B), between FSA with data variables whose languages are alternating sequences of input events and variable valuations [START_REF] Iosif | Abstraction refinement and antichains for trace inclusion of infinite state systems[END_REF], where the variables of the right-hand side automaton B are also controlled by the left-hand side automaton A, in other words, that B has no hidden variables. Example 1.13 Here is an example of FOADA A = (D, Σ, X, Q, ι, F, ∆):

• D = Z, Σ = {a, b}, X = {x, y}, Q = {q 0 , q 1 , q 2 }, ι = q 0 (0), F = {q 2 },
• ∆ contains transitions:

q 0 (d) a(x,y) ----→ q 1 (x) ∧ x > d ∧ q 2 (x, y) ∧ y > d, q 1 (d) b(x,y) ----→ q 1 (x) ∧ y < d ∨ q 2 (x, y) ∧ y > d, q 2 (d, e) b(x,y) ----→ q 2 (x, y) ∧ x > d ∧ y > e.
Note that d and e are not visible in the input.

The FOADA model is closed under union, intersection and complementation. Again, Boolean operations are possible in linear time. As the ADA model, the price here to be paid is that the emptiness checking of FOADA is undecidable, even for the simplest data theory of equality [START_REF] Farzan | Proof spaces for unbounded parallelism[END_REF]. Hence, in this thesis we also introduce an effective emptiness checking semi-algorithm for FOADA model, in the spirit of the IMPACT procedure [START_REF] Kenneth | Lazy abstraction with interpolants[END_REF], originally developed for checking safety of non-deterministic integer programs.

More details about FOADA are given in Chapter 4.

FOADA Checker

For validation purposes, we also have developed a tool -FOADA Checker [START_REF] Xu | Foada checker[END_REF], mainly used for checking inclusion between two automata or checking emptiness of an automaton. The tool is written in Java, via Java-SMT interface [START_REF]Java smt[END_REF] and using Z3 SMT solver [START_REF]Z3 smt solver[END_REF] for checking spuriousness, coverage queries and interpolant generation. The IMPACT semi-algorithm has been implemented in the tool to check the emptiness of an automaton. The automata models supported as input are: (i) predicate automata [START_REF] Farzan | Proof spaces for unbounded parallelism[END_REF][START_REF] Farzan | Proving liveness of parameterized programs[END_REF], (ii) alternating data automata and (iii) first-order alternating data automata.

More details about FOADA Checker are given in Chapter 6.

Applications

The main application of our models (ADA and FOADA) is checking inclusions between various classes of automata extended with variables ranging over infinite domains that recognise languages over infinite alphabets. The most widely known such classes are (i) timed automata [START_REF] Alur | A theory of timed automata[END_REF] and (ii) finite-memory automata [START_REF] Kaminski | Finite-memory automata[END_REF]. In both cases, complementation is not possible inside the class and inclusion is undecidable. Our contribution here is providing a systematic semi-algorithm for these decision problems. In addition, we can extend generic register automata [START_REF] Iosif | Abstraction refinement and antichains for trace inclusion of infinite state systems[END_REF] inclusion checking framework by allowing monitor (right-hand side) automata to have local (hidden) variables that are not visible in the language.

Another application is checking safety (mutual exclusion, absence of deadlocks, etc.) and liveness (termination, absence of starvation, etc.) properties of parameterised concurrent programs, consisting of an unbounded number of replicated threads that communicate via a fixed set of global variables (locks, counters, etc.). The verification of parametric programs has been reduced to checking the emptiness of a possibly infinite sequence of first-order alternating data automata, called predicate automata [START_REF] Farzan | Proof spaces for unbounded parallelism[END_REF][START_REF] Farzan | Proving liveness of parameterized programs[END_REF], encoding the inclusion of the set of traces of a parametric concurrent program into increasingly general proof spaces, obtained by generalisation of counter-examples. The program and the proof spaces are first-order alternating data automata over the infinite alphabet of pairs consisting of program statements and thread identifiers.

Organisation

Chapter 2 presents some preliminaries, including some basics of the first order logic, some brief introductions to automata and alternating automata.

In Chapter 3 we define Alternating Data Automata (ADA). Then we introduce the closure properties and show how the Boolean operations on ADA can be done in linear time. After that, we introduce the anti-chains and interpolants for the emptiness of ADA. Based on this, we provide two efficient semi-algorithms for emptiness checking, inspired by two state-ofthe-art abstraction refinement model checking methods: lazy predicate abstraction [START_REF] Henzinger | Lazy abstraction[END_REF] and the IMPACT semi-algorithm [START_REF] Kenneth | Lazy abstraction with interpolants[END_REF].

In Chapter 4 we define First-Order Alternating Data Automata (FOADA). Then we explain symbolic execution of FOADA. After that, we show that FOADA are closed under union, intersection and complementation. The emptiness problem for FOADA is undecidable, therefore we introduce an abstraction refinement semi-algorithm based on lazy annotation [START_REF] Kenneth | Lazy abstraction with interpolants[END_REF][START_REF] Kenneth | Lazy annotation revisited[END_REF] of the symbolic execution paths with interpolants obtained by (i) applying quantifier elimination with witness term generation and (ii) Lyndon interpolation in the quantifier-free theory of the data domain with uninterpreted predicate symbols.

The main applications of ADA and FOADA is checking inclusions between various classes of automata extended with variables ranging over infinite domains that recognise languages over infinite alphabets. Chapter 5 shows the applications of our models for timed automata [START_REF] Alur | A theory of timed automata[END_REF], register automata [START_REF] Kaminski | Finite-memory automata[END_REF] and predicate automata [START_REF] Farzan | Proof spaces for unbounded parallelism[END_REF][START_REF] Farzan | Proving liveness of parameterized programs[END_REF].

Chapter 6 explains our tool, the FOADA Checker [START_REF] Xu | Foada checker[END_REF]. The IMPACT semi-algorithm [START_REF] Kenneth | Lazy abstraction with interpolants[END_REF] described in previous chapters has been implemented in this tool. Some insightful case-studies can also be found in this chapter.

Notations

The following notations are frequently used throughout this thesis:

• N : The symbol N denotes natural numbers;

• Z : The symbol Z denotes integers;

• R : The symbol R denotes real numbers; Chapter 2

Preliminaries

In this chapter, we introduce some basics that are important for the following chapters.

In the first section, we introduce the syntax of the First-Order Logic (FOL), starting by terms and formulae; then we explain its semantics including interpretation and valuation. The second section introduces Craig interpolation and Lyndon interpolation. In the third section, we introduce some basics of automata on finite words. We start with Non-Deterministic Finite Automata (NFA), then we introduce Deterministic Finite Automata (DFA) which is a particular case of NFA, and then we explain the transformation of an NFA into a DFA that accepts the same language, which is called determinisation. We terminate this section by explaining complementation of an NFA. In the forth section, we introduce alternation. We first present Alternating Finite Automata (AFA) model, then we show how to complement AFA in linear time.

First-Order Logic

Functions and Constants

Given a set of sort symbols Σ S , a function symbol f σ1,σ2,...,σ #(f ) :σ f contains the following information:

• σ 1 , σ 2 , ..., σ #(f ) : σ f is the function signature1 where:

σ 1 , σ 2 , ..., σ #(f ) ∈ Σ S are the sorts of the function arguments; σ f ∈ Σ S is the sort of the function result;

• #(f ) ≥ 0 is the function arity.

For a function f with result sort σ f , if #(f ) = 0 then f is called a constant, and denoted by f σ f or simply2 f . For the Boolean sort Bool = { , ⊥} ∈ Σ S , we write for the constant true and ⊥ for the constant f alse.

Terms

Given a set of sort symbols Σ S , a set of function symbols Σ F and a countable set of variables VAR where each variable x σx ∈ VAR (simply3 denoted as x) has an associated sort σ x ∈ Σ S , a term t of sort σ t ∈ Σ S , denoted4 by t σt , is defined recursively by the grammar:

t ::= x σt , x σt ∈ VAR; variable | c σt , c σt ∈ Σ F ; constant | f σ1,σ2,...,σ #(f ) :σt (t σ1 1 , t σ2 2 , ..., t σ #(f ) #(f ) ), f σ1,σ2,...,σ #(f ) :σt ∈ Σ F , σ 1 , σ 2 , ..., σ #(f ) ∈ Σ S , t σ1 1 , t σ2 2 , ..., t σ #(f )
#(f ) are terms; function application

Formulae

Given a set of sort symbols Σ S , a first-order formula φ is defined recursively by the grammar: For a formula φ, we denote by FV(φ) the set of variables not occurring under the scope of a quantifier in φ. It is also called the set of free variables.

φ ::= t Bool , t Bool is Boolean term; Boolean term | t σ1 1 ≈ t σ2 2 , σ 1 , σ 2 ∈ Σ S , t σ1

Interpretation and Valuation

Given a set of sort symbols Σ S and a set of function symbols Σ F , an interpretation I for (Σ S , Σ F ) maps each:

• Sort symbol σ ∈ Σ S : to a non-empty set σ I ;

• Function symbol f σ1,σ2,...,σ #(f ) :σ f ∈ Σ F with #(f ) > 0 where σ 1 , σ 2 , ..., σ #(f ) , σ f ∈ Σ S : to a function f

I : σ I 1 × σ I 2 × ... × σ I #(f ) → σ I ;
• Constant symbol c σ ∈ Σ F where σ ∈ Σ S : to an element of σ I .

Given an interpretation I, the set of all possible valuations under I is denoted by V I . A valuation v ∈ V I maps each variable x σx ∈ VAR to an element of σ I

x . Given in addition a value α ∈ σ I

x , we write v[x ← α] for a valuation such that: (i) v[x ← α](x) = α, and (ii) v[x ← α](y) = v(y) for any y ∈ VAR with y = x.

Interpretation of Terms

Given an interpretation I and a valuation v ∈ V I , the interpretation of a term t, denoted by t I v , is defined recursively:

x I v = v(x), x ∈ VAR; c I v = c I , c ∈ Σ F ; f I v (t 1 , t 2 , ..., t #(f ) ) = f I (t 1 I v , t 2 I v , ..., t #(f ) I v ), f ∈ Σ F ,

Semantics of Formulae

Given an interpretation I and a valuation v ∈ V I , we write I, v |= φ if the first-order formula φ is interpreted to true under I and v. We have the following recursive definitions:

I, v |= t Bool iff t Bool I v = , t Bool is Boolean term; I, v |= t 1 ≈ t 2 iff t 1 I v = t 2 I v , t 1 , t 2 are terms; I, v |= ¬ψ iff I, v |= ψ, ψ is first-order formula; I, v |= ψ 1 ∧ ψ 2 iff I, v |= ψ 1 and I, v |= ψ 2 , ψ 1 , ψ 2 , are first-order formulae; I, v |= ∃x σ .ψ iff I, v[x σ ← α] |= ψ for some α ∈ σ I , ψ is first-order formula, x σ ∈ FV(ψ);
A first-order formula φ is satisfiable under the interpretation I if there exists a valuation v such that I, v |= φ, otherwise φ is unsatisfiable under I. If I, v |= φ for any v under I, then φ is valid under I.

Given two formulae φ and ψ, we write φ |= I ψ and say that φ entails ψ under the interpretation I, if and only if I, v |= φ implies I, v |= ψ for any valuation v.

Interpolation

Craig's Interpolation

Given a formula φ, the vocabulary of φ, denoted V (φ), is the set of predicate symbols and variables occurring in φ. For a term t, its vocabulary 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. Definition 2.1 [START_REF] Craig | Linear reasoning. a new form of the herbrand-gentzen theorem[END_REF][START_REF] Craig | Three uses of the herbrand-gentzen theorem in relating model theory and proof theory[END_REF] For two formulae A and B such that A |= B, a Craig interpolant is a formula I such that: (i) A |= I, (ii) I |= B and (iii)

V (I) ⊆ V (A) ∩ V (B).
Definition 2.2 For two formulae A and B, suppose the conjunction A ∧ B is unsatisfiable, a reverse interpolant is a formula I such that: (i) A |= I , (ii) I ∧ B is unsatisfiable and (iii)

V (I) ⊆ V (A) ∩ V (B).

Lyndon's Interpolation

Lyndon's interpolation theorem [START_REF] Lyndon | An interpolation theorem in the predicate calculus[END_REF] is a stronger form of Craig's interpolation theorem. By P + (φ) we denote the set of predicate symbols that occur in φ under an even number of negations and by P -(φ) we denote the set of predicate symbols that occur in φ under an odd number of negations. Definition 2.3 [START_REF] Lyndon | An interpolation theorem in the predicate calculus[END_REF] Given two formulae A and B such that A ∧ B is unsatisfiable, a Lyndon interpolant is a formula I such that: (i) A |= I, (ii) I ∧ B is unsatisfiable and (iii) V (I) ⊆ V (A) ∩ V (B), P + (I) ⊆ P + (A) ∩ P + (B) and P -(I) ⊆ P -(A) ∩ P -(B).

Automata on Finite Words

Non-Deterministic Finite Automata (NFA)

A non-deterministic finite automaton (NFA) is a tuple A = (Σ, Q, I, F, δ) where:

• Σ is a finite input alphabet;

• Q is a finite set of states;

• I ⊆ Q is the set of initial states;

• F ⊆ Q is the set of final states;

• δ : Q × Σ → 2 Q is the transition function.
Σ defines the symbols on which the automaton is defined. The set I defines the states in which the automaton may start, and I is possibly empty. The transition function δ can be identified with the relation →⊆ Q × Σ × Q given by: for q, p ∈ Q, a ∈ Σ : q a -→ p iff p ∈ δ(q, a)

Intuitively, q a -→ p denotes that the automaton can move from the state q to the state p when reading the input a.

Example 2.1 An example of NFA is depicted in Figure 2.1. Here in the AFA A = (Σ, Q, I, F, δ):

• Σ = {a, b}; • Q = {q 0 , q 1 , q 2 }; • I = {q 0 }; • F = {q 2 };
• δ is defined by:

δ(q 0 , a) = {q 0 }, δ(q 0 , b) = {q 0 , q 1 }, δ(q 1 , a) = {q 2 }, δ(q 1 , b) = {q 2 }, δ(q 2 , a) = δ(q 2 , b) = ∅ q 0 q 2 a,b q 1 b a b Figure 2.1: A Non-Deterministic Finite Automaton

Runs and Languages of NFA

Let A = (Σ, Q, I, F, δ) be an NFA and w = a 1 , a 2 , ..., a n ∈ Σ * a finite word of length n. A run for w in A is a finite sequence of states q 0 , q 1 , ..., q n such that:

• q 0 ∈ I • q i ai+1 ---→ q i+1 for all 0 ≤ i < n
In an NFA A = (Σ, Q, I, F, δ), there can be several runs for a given word w ∈ Σ * and the set of all possible runs for w in A is denoted by R A (w). A run r = q 0 , q 1 , ..., q n in A is called accepting if q n ∈ F . In addition, a finite word w ∈ Σ * is called accepted by A if there exists an accepting run for w.

The accepted language of an NFA A = (Σ, Q, I, F, δ), denoted by L(A), is the set of all words in Σ * accepted by A:

L(A) = {w ∈ Σ * | ∃r ∈ R A (w).r

is accepting}

For any NFA A = (Σ, Q, I, F, δ), here we extend the transition function δ to the function δ * : Q × Σ * → 2 Q as follows:

• δ * (q) = {q} for q ∈ Q;

• δ * (q, a) = δ(q, a) for q ∈ Q and a ∈ Σ;

• δ * (q, a 1 , a 2 , ..., a n ) = p∈δ(q,a1) δ * (p, a 2 , ..., a n ) for q, p ∈ Q and a 1 , a 2 , ..., a n ∈ Σ and n ≥ 2.

Stated in words, given a state q ∈ Q and a word w ∈ Σ * , δ * (q, w) is the set of states that are reachable from the state q for the input word w. Here we can represent the accepted language of a NFA A = (Σ, Q, I, F, δ) by means of the extended transition function δ * :

L(A) = {w ∈ Σ * | ∃q 0 ∈ I.δ * (q 0 , w) ∩ F = ∅}

Deterministic Finite Automata (DFA) and Determinisation

Let A = (Σ, Q, I, F, δ) be a NFA. A is called a deterministic finite automaton (ADA) if |I| ≤ 1 and |δ(q, a)| ≤ 1 for all states q ∈ Q and all symbols a ∈ Σ. In other words, a NFA is a DFA if it has at most one initial state and for each symbol the successor state of each state is either uniquely defined or undefined.

A DFA A = (Σ, Q, I, F, δ) is total if it has exactly one initial state and for each symbol the successor state of each state is uniquely defined, hence |I| = 1 and |δ(q, a)| = 1 for all states q ∈ Q and all symbols a ∈ Σ. Total DFA is often written in the form A = (Σ, Q, ι, F, δ) where ι stands for the unique initial state, and δ is a total transition function δ : Q × Σ → Q. In addition, the extended transition function δ * of a total DFA can be viewed as a total function δ * : Q × Σ * → Q, which for a given state q ∈ Q and a finite word w ∈ Σ * , returns a unique state p ∈ Q that is reached from the state q for the input word w, hence δ * (q, w) = p. So here particularly, the accepted language of a total DFA A = (Σ, Q, ι, F, δ) is given by:

L(A) = {w ∈ Σ * | δ * (ι, w) ∈ F } For a given NFA A = (Σ, Q, I, F, δ), we can construct a total DFA A D = (Σ D , Q D , ι D , F D , δ D )
that accepts the same language, hence L(A) = L(A D ), by power-set construction (also called subset construction), in which we simulate A by moving the prefixes of the given input word to the set of reachable states. This total DFA maybe exponentially larger than the original NFA:

• A D starts in the state set I;

• If A D is in a state set Q ⊆ Q, then with the input symbol a ∈ Σ, A D moves to another state set Q = q∈Q δ(q, a);
• If the input word has been consumed and A D is in a state set Q ⊆ Q that contains a state in F , then A D accepts the input word.

More formally, we define

A D = (Σ D , Q D , ι D , F D , δ D )
as follows:

• Σ D = Σ;

• Q D = 2 Q ; • ι D = I; • F D = {Q ⊆ Q | Q ∩ F = ∅}; • δ D : 2 Q × Σ → 2 Q is defined by: δ D (Q , a) = q∈Q δ(q, a) for Q ∈ Q D and a ∈ Σ. Example 2.2
The NFA in Example 2.1 (depicted in Figure 2.1) in Page 31 is not deterministic as on input symbol b in state q 0 the next state is either q 0 or q 1 . We apply power-set construction to obtain a DFA accepting same language and the result is depicted in Figure 2.2.

{q 0 } {q 0 ,q 1 ,q 2 } {q 0 ,q 2 } a {q 0 ,q 1 } b a b a b a b

Complementation of NFA

Since total DFA have exactly one run for each input word, complementing a total DFA is simple, by just declaring all the non-final states to be final and all the final states to be nonfinal. This defines again a total DFA that accepts the complement of the language of the original DFA under the same alphabet. More formally, given a total DFA A = (Σ, Q, ι, F, δ),

then A = (Σ, Q, ι, Q \ F, δ) is a total DFA with L(A) = Σ * \ L(A).
For any given NFA A over an alphabet Σ, we can first transform it into a total DFA A D by power-set construction, and complement A D to obtain A D . A D accepts the complement of the language of A, hence L(A D ) = Σ * \ L(A).

Example 2.3 Considering the total DFA in Figure 2.2, we declare all its non-final states to be final, hence {q 0 } and {q 0 , q 1 } become final states; and we declare all its final states to be nonfinal, hence {q 0 , q 2 } and {q 0 , q 1 , q 2 } become non-final states. Then we obtain a DFA, depicted in Figure 2.3, which is the complement of the DFA in Figure 2.2, hence also the complement of the NFA in Figure 2.1 in Page 31.

{q 0 ,q 1 ,q 2 } {q 0 } {q 0 ,q 2 } a {q 0 ,q 1 } b a b a b a b Figure 2.3: Complement of NFA in Example 2.1 in Page 31
2.4 Alternating Finite Automata (AFA)

Definition of AFA

An alternating finite automaton (AFA) is a tuple A = (Σ, Q, ι, F, g) where:

• Σ is a finite input alphabet;

• Q = {q 1 , q 2 , ..., q |Q| } is a finite set of states;

• ι ∈ Q is the initial states;

• F ⊆ Q is the set of final states;

• g : Q → (Σ × B |Q| → B)
is the transition function where B denotes the Boolean set {0, 1}.

In an AFA A = (Σ, Q, ι, F, g), the function g associates with each state q ∈ Q a Boolean function g(q) : Σ × B |Q| → B. Given an input symbol a ∈ Σ and associating a Boolean value u i with each of the |Q| states q i where q i ∈ Q for i ∈ N and 1 ≤ i ≤ |Q|, then g(q) computes a Boolean value g(q)(a)(u 1 , u 2 , ..., u |Q| ) to be associated with state q.

Example 2.4 In Figure 2.4 we introduce alternation into FSA, where there are two types of alternating transitions: (i) a universal transition: q 1 a -→ q 2 ∧ q 3 ; (ii) an existential transition:

q 3 b - → q 1 ∨q 2 . Formally, we define an AFA A = (Σ, Q, ι, F, g), where Σ = {a, b}, Q = {q 1 , q 2 , q 3 }, ι = q 1 , F = {q 2 , q 3 }
and g is given by Table 2.1. According to the definition of the function g, we can also build three Σ × B |Q| → B tables referring respectively to g(q 1 ), g(q 2 ) and g(q 3 ).

q 1 q 3 q 2 a a a,b b b Figure 2.4: An Automaton with Alternating Transitions a b q 1 q 2 ∧ q 3 0 q 2 q 2 q 2 q 3 0 q 1 ∨ q 2 Table 2.1: g a b (0, 0, 0) 0 0 (0, 0, 1) 0 0 (0, 1, 0) 0 0 (0, 1, 1) 1 0 (1, 0, 0) 0 0 (1, 0, 1) 0 0 (1, 1, 0) 0 0 (1, 1, 1) 1 0 Table 2.2: g(q 1 ) a b (0, 0, 0) 0 0 (0, 0, 1) 0 0 (0, 1, 0) 1 1 (0, 1, 1) 1 1 (1, 0, 0) 0 0 (1, 0, 1) 0 0 (1, 1, 0) 1 1 (1, 1, 1) 1 1 Table 2.3: g(q 2 ) a b (0, 0, 0) 0 0 (0, 0, 1) 0 0 (0, 1, 0) 0 1 (0, 1, 1) 0 1 (1, 0, 0) 0 1 (1, 0, 1) 0 1 (1, 1, 0) 0 1 (1, 1, 1) 0 1 Table 2.4: g(q 3 )

Languages of AFA

Given an n-tuple u = u 1 , u 2 , ..., u n of Boolean values, we define the projection function π : [1, n] → (B n → B) as follows:

π(i)(u) = u i for i ∈ N and 1 ≤ i ≤ n
With this projection, for an AFA A = (Σ, Q, ι, F, g), we define f , the characteristic vector of F where:

π(i)(f ) = 1 if q i ∈ F 0 if q i / ∈ F for i ∈ N and 1 ≤ i ≤ |Q|
For any AFA A = (Σ, Q, ι, F, g), we extend the function g to the function g * : Q → (Σ * → (B |Q| → B)) as follows:

• g * (q i )(λ) = π(i) where q i ∈ Q and λ ∈ Σ * is the empty string; • g * (q i )(ax)(u) = g(q i )(a, g * (q 1 )(x)(u), g * (q 2 )(x)(u), ..., g * (q |Q| )(x)(u)) where q i ∈ Q, a ∈ Σ, x ∈ Σ * , u = u 1 , u 2 , ..., u |Q| and u j ∈ {0, 1} for j ∈ N and 1 ≤ j ≤ |Q|.
Now with this function g * , we can define the accepted words of the AFA. Let A = (Σ, Q, ι, F, g) be an AFA, a word w ∈ Σ * is accepted by A if and only if:

g * (ι)(w)(f ) = 1 where f is the characteristic vector of F Example 2.5
The word "ab" is accepted by the AFA in Example 2.4 and here is the proof: g * (q 1 )(ab)(0, 1, 1) = g(q 1 )(a, g * (q 1 )(b)(0, 1, 1), g * (q 2 )(b)(0, 1, 1), g * (q 3 )(b)(0, 1, 1)) = g(q 1 )(a, g(q 1 )(b, g * (q 1 )(λ)(0, 1, 1), g * (q 2 )(λ)(0, 1, 1), g * (q 3 )(λ)(0, 1, 1)) g(q 2 )(b, g * (q 1 )(λ)(0, 1, 1), g * (q 2 )(λ)(0, 1, 1), g * (q 3 )(λ)(0, 1, 1))

g(q 3 )(b, g * (q 1 )(λ)(0, 1, 1), g * (q 2 )(λ)(0, 1, 1), g * (q 3 )(λ)(0, 1, 1))) = g(q 1 )(a, g(q 1 )(b, π(1)(0, 1, 1), π(2)(0, 1, 1), π(3)(0, 1, 1)) g(q 2 )(b, π(1)(0, 1, 1), π(2)(0, 1, 1), π(3)(0, 1, 1)) g(q 3 )(b, π(1)(0, 1, 1), π(2)(0, 1, 1), π(3)(0, 1, 1))) = g(q 1 )(a, g(q 1 )(b, 0, 1, 1), g(q 2 )(b, 0, 1, 1), g(q 3 )(b, 0, 1, 1)) = g(q 1 )(a, 0, 1, 1) = 1
The language accepted by an AFA is the set of all accepted words, hence for a given AFA A = (Σ, Q, ι, F, g): Formally, a DA is a tuple A = (D, Σ, X, Q, ι, F, ∆) where:

L(A) = {w ∈ Σ * | g * (ι)(w)(f ) = 1}
• D is a possibly infinite data domain;

• Σ is a finite alphabet of input events including a special padding symbol ∈ Σ;

• X = {x 1 , x 2 , ..., x |X| } is a set of variables; • Q is a finite set of states; • ι ∈ Q is the initial state; • F ⊆ Q is the set of final states; • ∆ is a set of rules of the form q a,φ(X,X ) ------→ q where a ∈ Σ is an input symbol and φ(X, X ) is a formula in T(D). A configuration of a DA A = (D, Σ, X, Q, ι, F, ∆) is a pair (q, v) ∈ Q×D X and a configuration (q , v ) is called a successor of (q, v) if and only if: (i) ∃a ∈ Σ.q a,φ --→ q ∈ ∆ ; (ii) (v, v ) |= T(D) φ.
We denote the successor relation by (q, v) a,φ --→ (q , v ) and we omit writing φ when no confusion may arise. We denote by succ(q, v) = {(q , v ) | (q, v) → (q , v )} the set of successors of a configuration (q, v).

Languages of DA

For a DA A = (D, Σ, X, Q, ι, F, ∆), a trace is a finite sequence w of pairs (v i , a i ) taken from D X × Σ: w = (v 0 , a 0 ), (v 1 , a 1 ), ..., (v n-1 , a n-1 ), (v n , )
Accordingly, a run of A over the trace w

= (v 0 , a 0 ), (v 1 , a 1 ), ..., (v n-1 , a n-1 ), (v n , ) is a sequence of configurations π: π = (q 0 , v 0 ), (q 1 , v 1 ), ..., (q n , v n ) for each i ∈ N, 0 ≤ i ≤ n -1 : (q i , v i ) ai -→ (q i+1 , v i+1 )
We say that π is accepting if and only if q n ∈ F , in which case A accepts w. The language of A, denoted by L(A), is the set of all traces accepted by A.

Determinisation

Let A = (D, Σ, X, Q, ι, F, ∆) be a DA, A is said to be deterministic if and only if, for each trace w ∈ L(A), A has at most one run over w. Any DA can be determinised while preserving its language. The reason why determinisation is possible for automata over an infinite data alphabet D X × Σ is that the successive values taken by each variable x ∈ X are tracked by the language L(A) ⊆ (D X × Σ) * . But there is an example of classical automata over an infinite alphabet that cannot be determinised -timed automata [START_REF] Alur | A theory of timed automata[END_REF], in which only the elapsed time is reflected in the language but not the values of the clocks.

The determinisation procedure is a generalisation of the classical subset construction for word automata [START_REF] Rabin | Finite automata and their decision problems[END_REF] on finite alphabets. Formally, for a DA A = (D, Σ, X, Q, ι, F, ∆), the deterministic data automata (DDA) accepting the language L(A) are defined as

A D = (D, Σ, X, Q D , ι D , F D , ∆ D ):
• D is the same infinite data domain;

• Σ is the same finite alphabet of input events including a special padding symbol ∈ Σ;

• X = {x 1 , x 2 , ..., x |X| } is the same set of variables; • Q D = 2 Q ; • ι D = {ι}; • F D = {P ⊆ Q | P ∩ F = ∅}; • ∆ D is the set of rules P a,θ --→ P such that: (i) ∀p ∈ P .∃p ∈ P.p a -→ p ∈ ∆; (ii) θ(X, X ) ≡ p ∈P p a,ψ --→p ∈∆,p∈P,a∈Σ ψ ∧ p ∈Q\P p a,φ
--→p ∈∆,p∈P,a∈Σ ¬φ.

The main difference with the classical subset construction for Rabin-Scott automata is that here we consider all sets P of states that have a predecessor in P , not just the maximal such set. This refined subset construction takes not only the alphabet symbols in Σ but also the valuations of variables in X. This determinisation can be done for any theory T h(D) closed under conjunction and negation.

Given a DA A = (D, Σ, X, Q, ι, F, ∆) and its determinisation A D = (D, Σ, X, Q D , ι D , F D , ∆ D ), we have 5 :
• For any w ∈ (D X × Σ) * and P ∈ Q D , A D has exactly one run on w that starts in P ;

• L(A) = L(A D ).

Closure Properties

Given a DA A = (D, Σ, X, Q, ι, F, ∆) and its determinisation

A D = (D, Σ, X, Q D , ι D , F D , ∆ D ),
we can construct the complement of A, denoted by A, defined as follow:

A = (D, Σ, X, Q D , ι D , Q D \ F D , ∆ D )
A has the same structure as A D , and its set of final states consists of those subsets that contain no final state of A, hence

{P ⊆ Q | P ∩ F = ∅}. We have L(A) = (D X × Σ) * \ L(A). Given two DA A = (D, Σ, X, Q A , ι A , F A , ∆ A ) and B = (D, Σ, X, Q B , ι B , F B , ∆ B ), we define the intersection of these two DA: A × B = (D, Σ, X, Q A × Q B , (ι A , ι B ), F A × F B , ∆ × ) where (q A , q B ) a,φ --→ (q A , q B ) ∈ ∆ × if and only if: (i) q A a,ψ --→ q A ∈ ∆ A ; (ii) q B a,η --→ q B ∈ ∆ B ; (iii) φ ≡ ψ ∧ η. And we have L(A × B) = L(A) ∩ L(B).
Above we show that DA are closed under intersection, now it is easy to show that DA are also closed under union since:

L(A × B) = L(A) ∪ L(B)
Chapter 3

Alternating Data Automata (ADA)

Alternating automata have been widely used to model and verify systems that handle data from finite domains, such as communication protocols or hardware. The main advantage of the alternating model of computation is that complementation is possible in linear time, thus allowing one to concisely encode trace inclusion problems that occur often in verification.

In this chapter, we consider a model of alternating automata over infinite alphabets, called alternating data automata (ADA), whose transition rules are formulae in a combined theory of Booleans and some infinite data domain, that relate past and current values of the data variables. The data theory is not fixed, but rather it is a parameter of the class.

We also show that union, intersection and complementation are possible in linear time in this model and though the emptiness problem is undecidable, we provide two efficient semialgorithms, inspired by two state-of-the-art abstraction refinement model checking methods: lazy predicate abstraction [START_REF] Henzinger | Lazy abstraction[END_REF] and the IMPACT semi-algorithm [START_REF] Kenneth | Lazy abstraction with interpolants[END_REF].

Introduction of ADA

Data Words

Firstly, we fix an interpretation I and a finite alphabet Σ of input events for the rest of this section. Given a finite set X ⊂ VAR of variables of sort D, let X → D I be the set of data symbols. A data word w is a finite sequence:

(a 1 , v 1 ), (a 2 , v 2 ), ..., (a |w| , v |w| )
where a 1 , a 2 , ..., a |w| ∈ Σ and v 1 , v 2 , ..., v |w| : X → D I are valuations. We denote by ε the empty sequence, by Σ * the set of finite sequences of input events and by Σ[X] * the set of data words over X. This definition generalises the classical notion of words from a finite alphabet to a possibly infinite alphabet Σ[X]. More precisely, when D I is sufficiently large or infinite, we can map the elements of Σ into designated elements of D I and use a special variable to encode the input events.

Definition of ADA

Given a finite set X ⊂ VAR of variables of sort D and a finite set B of Boolean variables, we denote by FORM(B, X) the set of formulae φ such that F V Boolean (φ) ⊆ B and F V D (φ) ⊆ X. In addition, by FORM + (B, X) we denote the set of formulae from FORM(B, X) in which each Boolean variable occurs only under an even number of negations.

An alternating data automaton (ADA) is a tuple A = (D, Σ, X, Q, ι, F, ∆) where:

• D is a possibly infinite data domain;

• Σ is a finite alphabet of input events;

• X ⊂ VAR is a finite set of variables of sort D;

• Q ⊂ VAR is a finite set of states which are Boolean;

• ι ∈ FORM + (Q, ∅) is the initial configuration; • F ⊆ Q is the set of final states; • ∆ : Q × Σ → FORM + (Q, X ∪ X) is a transition function where X denotes {x | x ∈ X}.
In each formula ∆(q, a) where q ∈ Q and a ∈ Σ, the variables X track the previous values and X track the current values of variables of A. Observe that the initial configuration does not contain free data variables, hence the initial values of the variables are left unconstrained. The size of A is defined as

|A| = |ι| + (q,a)∈Q×Σ |∆(q, a)|. Example 3.1 Figure 3.1.left depicts an ADA over D I = Z with an input alphabet Σ = {a, b}, variables X = {x, y}, states Q = {q 0 , q 1 ,
q 2 , q 3 , q 4 }, initial configuration ι = q 0 , final states F = {q 3 , q 4 } and transitions ∆ given in Figure 3.1.right, where missing rules are assumed to be f alse, for example ∆(q 0 , b) = ⊥. Transition rules ∆(q 0 , a) and ∆(q 1 , a) are universal, and there is no existential non-deterministic rule in this ADA. Transition rule ∆(q 2 , a) ≡ q 2 ∧x > x∧y > y compares the current value of x (denoted by x) with the past value of x (denoted by x) and compares the current value of y (denoted by y) with the past value of y (denoted by y). Transition rule ∆(q 0 , a) ≡ q 1 ∧ q 2 ∧ x ≈ 0 ∧ y ≈ 0 constrains the current value of x and the current value of y.

q 0 q 2 q 1 a : x ≈ 0 ∧ y ≈ 0 a : x ≈ y + 1 ∧ y ≈ x + 1 q 3 q 4 b : x ≥ y b : x > y a : x > x ∧ y > y ∆(q 0 , a) ≡ q 1 ∧ q 2 ∧ x ≈ 0 ∧ y ≈ 0 ∆(q 1 , a) ≡ q 1 ∧ q 2 ∧ x ≈ y + 1 ∧ y ≈ x + 1 ∆(q 1 , b) ≡ q 3 ∧ x ≥ y ∆(q 2 , a) ≡ q 2 ∧ x > x ∧ y > y ∆(q 2 , b) ≡ q 4 ∧ x > y

Time Stamp and Accepted Words

Given an ADA A = (D, Σ, X, Q, ι, F, ∆), for an input event a ∈ Σ and a formula φ, we write ∆(φ, a) for the formula obtained from φ by simultaneously replacing each state q ∈ FV Boolean (φ) by the formula ∆(q, a). Let X k = {x k | x ∈ X}, for any k ∈ N, be a set of time-stamped variables. We write ∆ k (φ, a) for the formula obtained from φ by replacing each state q ∈ FV Boolean (φ) by the formula ∆(q, a)[X k /X, X k+1 /X].

For any ADA A = (D, Σ, X, Q, ι, F, ∆), given a word w = (a 1 , v 1 ), (a 2 , v 2 ), ..., (a |w| , v |w| ) where a 1 , a 2 , ..., a |w| ∈ Σ and v 1 , v 2 , ..., v |w| : X → D I , the run of A over w is the sequence of formulae:

φ 0 (Q), φ 1 (Q, X 0 ∪ X 1 ), φ 2 (Q, X 0 ∪ X 1 ∪ X 2 ), ..., φ |w| (Q, X 0 ∪ X 1 ∪ ... ∪ X |w| ) where φ 0 ≡ ι and ∀k ∈ [1, |w|].φ k ≡ ∆ k (φ k-1 , a k ).
Next, let us write ∆(ι, a 1 , a 2 , ..., a |w| ) for the formula φ |w| (X 0 , X 1 , ..., X |w| ) above. We say that A accepts the word w if and only if I, v |= ∆(ι, a 1 , a 2 , ..., a |w| ) for the valuation v that maps:

• each x ∈ X k to v k (x) for all k ∈ [1, |w|]; • each q ∈ FV Boolean (φ |w| ) ∩ F to ; • each q ∈ FV Boolean (φ |w| ) \ F to ⊥;
Example 3.2 For the ADA in Example 3.1 (in Figure 3.1), where the function symbols have standard arithmetic interpretation, the word w = (a, 0, 0), (a, 1, 1), (b, 2, 1) is not accepted. Here is the run of A on w:

q 0 (φ 0 ) a,0,0 ---→ q 1 ∧ q 2 ∧ x 1 ≈ 0 ∧ y 1 ≈ 0 (φ 1 ) a,1,1 ---→ q 1 ∧ q 2 ∧ x 2 ≈ y 1 + 1 ∧ y 2 ≈ x 1 + 1 ∧ q 2 ∧ x 2 > x 1 ∧ y 2 > y 1 ∧ x 1 ≈ 0 ∧ y 1 ≈ 0 (φ 2 ) b,2,1 ---→ q 3 ∧ x 2 ≥ y 2 ∧ q 4 ∧ x 2 > y 2 ∧ x 2 ≈ y 1 + 1 ∧ y 2 ≈ x 1 + 1 ∧ q 4 ∧ x 2 > y 2 ∧ x 2 > x 1 ∧ y 2 > y 1 ∧ x 1 ≈ 0 ∧ y 1 ≈ 0 (φ 3 )
with the valuation v where:

• v(x 1 ) = 0, v(y 1 ) = 0, v(x 2 ) = 1, v(y 2 ) = 1, v(x 3 ) = 2, v(y 3 ) = 1; • v(q 3 ) = , v(q 4 ) = ;
we can have:

φ 3 I v = ∧ 1 ≥ 1 ∧ ∧ 1 > 1 ∧ 1 = 0 + 1 ∧ 1 = 0 + 1 ∧ ∧ 1 > 1 ∧ 1 > 0 ∧ 1 > 0 ∧ 0 = 0 ∧ 0 = 0 = ∧ ∧ ∧ ⊥ ∧ ∧ ∧ ∧ ⊥ ∧ ∧ ∧ ∧ = ⊥
Hence I, v |= ∆(q 0 , a, a, b), therefore the word w = (a, 0, 0), (a, 1, 1), (b, 2, 1) is not accepted.

Closure Properties of ADA

Intersection

Given two ADA A = (D, Σ, X, Q A , ι A , F A , ∆ A ) and B = (D, Σ, X, Q B , ι B , F B , ∆ B ), assuming without loss of generality, that Q A ∩ Q B = ∅,
we define the intersection automaton:

A ∩ B = (D, Σ, X, Q A ∪ Q B , ι A ∧ ι B , F A ∪ F B , ∆ A ∪ ∆ B )
and we have

L(A ∩ B) = L(A) ∩ L(B)
. The intersection can be built in linear time since

|A ∩ B| = |A| + |B|.

Union

Given two ADA A = (D, Σ, X, Q A , ι A , F A , ∆ A ) and B = (D, Σ, X, Q B , ι B , F B , ∆ B )
, assuming without loss of generality, that Q A ∩ Q B = ∅, we define the union automaton:

A ∪ B = (D, Σ, X, Q A ∪ Q B , ι A ∨ ι B , F A ∪ F B , ∆ A ∪ ∆ B )
and we have L(A ∪ B) = L(A) ∪ L(B). The union can be built in linear time since |A ∪ B| = |A| + |B|.

Complementation

Given a set B of Boolean variables and a set X of variables of sort D, for a formula φ ∈ FORM + (B, X) with no negated occurrences of the Boolean variables, we define its complement:

φ 1 ∧ φ 2 ≡ φ 1 ∨ φ 2 φ 1 ∨ φ 2 ≡ φ 1 ∧ φ 2 φ ≡ φ if φ ∈ B φ ≡ ¬φ if φ / ∈ B atom ¬φ ≡ ¬φ if φ not atom
Given an ADA A = (D, Σ, X, Q, ι, F, ∆), now we define the complement automaton:

A = (D, Σ, X, Q, ι, Q \ F, ∆)
where ∆(q, a) ≡ ∆(q, a) for all q ∈ Q and a ∈ Σ. We have

L(A) = Σ[X] * \ L(A).
The operation of complementation can be build in linear time since |A| = |A|.

Proofs for Boolean Closures

We prove L(A ∪ B) = L(A) ∪ L(B) first, and the proof for L(A ∩ B) = L(A) ∩ L(B) is analogous. Let w = (a 1 , v 1 ), (a 2 , v 2 ), ..., (a n , v n ) be a word, where n = 0 corresponds to the empty word. We prove by induction on n ≥ 0 that ∆(ι 1 ∨ ι 2 , a 1 , a 2 , ..., a n ) ⇔ ∆(ι 1 , a 1 , a 2 , ..., a n ) ∨ ∆(ι 2 , a 1 , a 2 , ..., a n ). The case n = 0 follows from the definition of the initial configuration of A ∪ B. For the inductive step n > 0, ∆(ι 1 ∨ι 2 , a 1 , a 2 , ..., a n ) is obtained from ∆(ι 1 ∨ι 2 , a 1 , a 2 , ..., a n-1 ) by replacing each variable q ∈ FV Boolean (ι

1 ∨ ι 2 , a 1 , a 2 , ..., a n-1 ) with ∆(q, a n )[X n-1 /X, X n /X], denoted ∆ n (∆(ι 1 ∨ ι 2 , a 1 , a 2 , ..., a n-1 ), a n ).
Since by induction hypothesis:

∆(ι 1 ∨ ι 2 , a 1 , a 2 , ..., a n-1 ) ⇔ ∆(ι 1 , a 1 , a 2 , ..., a n-1 ) ∨ ∆(ι 2 , a 1 , a 2 , ..., a n-1 )
we obtain:

∆ n (∆(ι 1 ∨ ι 2 , a 1 , a 2 , ..., a n-1 ), a n ) ⇔ ∆ n (∆(ι 1 , a 1 , a 2 , ..., a n-1 ), a n ) ∨ ∆ n (∆(ι 2 , a 1 , a 2 , ..., a n-1 ), a n ) ⇔ ∆(ι 1 , a 1 , a 2 , ..., a n ) ∨ ∆(ι 2 , a 1 , a 2 , ..., a n ) Proposition 3.1 Given a formula φ ∈ FORM + (Q, X
) and a valuation v mapping each q ∈ Q to a value v(q) ∈ B and each x ∈ X to a value v(x) ∈ D I , let v be the valuation that assigns each q ∈ Q the value ¬v(q) and each x ∈ X the value v(x). Then we have I, v |= φ if and only if I, v |= φ. (Can be proved immediately by induction on the structure of φ.)

To prove L(A) = Σ[X] * \ L(A), let w = (a 1 , v 1
), (a 2 , v 2 ), ..., (a n , v n ) be a word and by induction on n ≥ 0 show that:

∆(ι, a 1 , a 2 , ..., a n ) = ∆(ι, a 1 , a 2 , ..., a n )
The case n = 0 is immediate, because FV(ι) ⊆ Q and thus ι ≡ ι. For the case n > 0, we compute: ∆(ι, a 1 , a 2 , ..., a n ) = ∆(ι, a 1 , a 2 , ..., a n ) by induction on n ≥ 0.

In the case n = 0, we have ∆(ι, a 1 , a 2 , ..., a n ) ≡ ι. Then ε is accepted by A if and only if v 0 |= ι, where v 0 (q) = if q ∈ F and v 0 (q) = ⊥, otherwise. But v 0 |= ι if and only if v 0 |= ι, where v 0 (q) = if q ∈ F and v 0 (q) = ⊥, otherwise. Thus ε is accepted by A if and only if it is not accepted by A.

For the case n > 0, we compute:

∆ n (∆(ι, a 1 , a 2 , ..., a n-1 ), a n ) ⇔ ∆ n (∆(ι, a 1 . . . a n-1 ), a n ) ⇔ ∆(ι, a 1 , a 2 , ..., a n ) Let v, v : (Q ∪ n i=0 X i ) → (B ∪ D I
) be valuations such that:

• v(q) = and v (q) = ⊥, for each q ∈ F ;

• v(q) = ⊥ and v (q) = , for each q ∈ Q \ F ;

• v(x) = v (x), for each x ∈ X 0 ; • v(x) = v (x) = v i (x), for each x ∈ X i and each i ∈ [1, n].
By Proposition 3.1, we have:

I, v |= ∆(ι, a 1 , a 2 , ..., a n ) ⇔ I, v |= ∆(ι, a 1 , a 2 , ..., a n ) ⇔ I, v |= ∆(ι, a 1 , a 2 , ..., a n )
Thus for all w ∈ Σ[X] * , we have w ∈ L(A) if and only if w ∈ L(A).

Antichains and Interpolants for ADA Emptiness

Undecidability for Emptiness Problem

The emptiness problem for ADA is undecidable, even in very simple cases. For example, given the set of positive integers as D I , an ADA can simulate an alternating vector addition system with states (AVASS) [START_REF] Courtois | Alternating Vector Addition Systems with States[END_REF] using only atoms x ≥ k and x = x + k for k ∈ Z, with the classical interpretation of the function symbols on integers. Since the reachability of a control state is undecidable for AVASS [START_REF] Lincoln | Decision problems for propositional linear logic[END_REF], ADA emptiness is undecidable.

Consequently, given an ADA A, we give up on the guarantee for termination and build semi-algorithms that meet the requirements below:

• if L(A) = ∅, the procedure will terminate and return a word w ∈ L(A) which is called a counter-example of emptiness;

• if the procedure terminates without returning any counter-example, then L(A) = ∅.

Post-Images and Acceptance Function

Let A = (D, Σ, X, Q, ι, F, ∆) be an ADA, given a formula φ ∈ FORM + (Q, X) and an input event a ∈ Σ, we define the post-image function

POST A : FORM + (Q, X) × Σ → FORM + (Q, X) as follows: POST A (φ, a) ≡ ∃X.∆(φ[X/X], a)
mapping each formula in FORM + (Q, X) to a formula defining the effect of reading the event a.

For any ADA A = (D, Σ, X, Q, ι, F, ∆), we extend the post-image function to FORM + (Q, X)× Σ * → FORM + (Q, X) as follows:

• POST A (φ, ε) ≡ φ; • POST A (φ, ua) ≡ POST A (POST A (φ, u), a) for a ∈ Σ and u ∈ Σ * .

And we define now the acceptance function ACC

A : Σ * → FORM + (Q, X) as follows: ACC A (u) ≡ POST A (ι, u) ∧ q∈Q\F (q → ⊥) for u ∈ Σ * .
The emptiness problem for an ADA A = (D, Σ, X, Q, ι, F, ∆) then becomes "Does there exist a word u ∈ Σ * such that the formula ACC A (u) is satisfiable?". Since we ask a satisfiability query, the final states of A need not be constrained. Because each state occurs positively in ACC A (u), this formula has a model if and only if there is a model with every q ∈ F set to true. A naive semi-algorithm enumerates all finite sequences and checks the satisfiability of ACC A (u) for each u ∈ Σ * , using a decision procedure for the theory T(S, I)1 .

Improvement by Anti-Chains

Given a partial order over a data domain D, an antichain is a set A ⊆ D such that a b for any a, b ∈ A.

For any ADA A = (D, Σ, X, Q, ι, F, ∆), since no Boolean variable from Q occurs under negation in any formula, it is easy to prove the monotonicity property:

given φ, ψ ∈ FORM + (Q, X), if φ |= ψ then POST A (φ, u) |= POST A (ψ, u) for any u ∈ Σ * .
This suggests an improvement of the above semi-algorithm that enumerates and stores only a set U ⊆ Σ * for which {POST A (φ, u) | u ∈ U } forms an antichain with respect to the entailment partial order. This is because, for any u, v ∈ Σ * , if POST A (ι, u) |= POST A (ι, v) and ACC A (uw) is satisfiable for some w ∈ Σ * , then POST A (ι, uw) |= POST A (ι, vw), thus ACC A (vw) is satisfiable as well, and there is no need to check further for u, since the non-emptiness of A can be proved using v alone. However, even with this improvement, the enumeration of sequences from Σ * diverges in many real cases, because infinite antichains exist in many interpretations, such as q ∧ x ≈ 0, q ∧ x ≈ 1, ... for D I = N.

Safety Invariants

A safety invariant for an ADA A = (D, Σ, X, Q, ι, F, ∆) is a function INV : (Q → B) → 2 X →D I
such that, for every Boolean valuation β : Q → B, every valuation v : X → D I of the data variables and every finite sequence u ∈ Σ * of input events, the following hold:

• I, β ∪ v |= POST A (ι, u) ⇒ v ∈ INV(β); • v ∈ INV(β) ⇒ I, β ∪ v |= ACC A (u).
If INV satisfies only the first point above, then we call it an invariant. Intuitively, a safety invariant maps every Boolean valuation into a set of data valuations, that contains the initial configuration ι ≡ POST A (ι, ε), whose data variables are unconstrained, over-approximates the set of reachable valuations and excludes the valuations satisfying the acceptance condition.

For an ADA A = (D, Σ, X, Q, ι, F, ∆), a formula φ(Q, X) is said to define INV if and only if for all β : Q → B and v : X → D I , we have I, β ∪ v |= φ if and only if v ∈ INV(β)
. And in addition, we have following lemma:

Lemma 3.1 L(A) = ∅ if and only if A has a safety invariant.
The proof of Lemma 3.1 is very simple. Let A = (D, Σ, X, Q, ι, F, ∆) in the following:

⇐ This direction is trivial. ⇒ We define: IN V : (Q → B) → 2 X→D I as follows. For each β : Q → B, let IN V (β) = {v : X → D I | ∃u ∈ Σ * .β ∪ v |= P OST A (ι, u)}.
Checking that IN V is a safety invariant is straightforward.

Abstraction and Refinement

Turning back to our issue of divergence of language emptiness semi-algorithms in the case L(A) = ∅, we can observe that an enumeration of input sequences u 1 , u 2 , ... ∈ Σ * can stop at step k as soon as

k i=1
POST A (ι, u i ) defines a safety invariant for A. Although this condition can be effectively checked using a decision procedure for the theory T(S, I), there is no guarantee that this check will ever succeed.

The solution we adopt in the sequel is an abstraction to ensure the termination of invariant computations. However, it is worth pointing out from the start that the abstraction alone will only allow us to build invariants that are not necessarily safety invariants. To meet the latter condition, we resort to counter-example guided abstraction refinement (CEGAR).

Formally, for a given ADA A = (D, Σ, X, Q, ι, F, ∆), we fix Π ⊆ FORM(Q, X), a set of formulae such that ⊥ ∈ Π and refer to these formulae as predicates. Given a formula φ, we denote by φ # ≡ {π ∈ Π | φ ∈ π} the abstraction of φ with respect to the predicates in Π. The abstract version of the post-image is defined as follows:

• POST # A (φ, ε) ≡ φ # ; • POST # A (φ, ua) ≡ (POST A (POST # A (φ, u), a)) # for a ∈ Σ and u ∈ Σ * .
With this abstract version of post-image, we can define the abstract version of acceptance function:

ACC # A (u) ≡ POST # A (ι, u) ∧ q∈Q\F (q → ⊥) for u ∈ Σ * .
Lemma 3.2 For any bijection µ : N → Σ * , there exists k > 0 such that

k m=0 POST # A (ι, µ(m)) defines an invariant INV # for A.
The proof of Lemma 3.2 is not complicated. It is sufficient to show that there exists k ≥ 0 such that for all u ∈ Σ * there exists

i ∈ [0, k] such that P OST A (ι, u) |= P OST # A (ι, µ(i)). We have P OST A (ι, u) |= P OST # A (ι, u) for all u ∈ Σ * . But since Π is a finite set, also the set {P OST # A (ι, u) | u ∈ Σ * } is finite. Thus there exists k ≥ 0 such that, for all u ∈ Σ * there exists i ∈ [0, k] such that P OST # A (ι, u) ⇔ P OST # A (ι, µ(i))
, which concludes the proof. If we look back to the definition of safety invariants in the previous section, we are left with fulfilling the second point from the definition. To this end, suppose that, for a given set Π of predicates, the invariant INV # defined above meets the first point of the definition of a safety invariant but not the second point. In other words, there exists a finite sequence u ∈ Σ * such that v ∈ INV # (β) and I, β ∪ v |= ACC # A (u) for some Boolean β : Q → B and data v : X → D I valuations. Such u ∈ Σ * is called a counter-example. Once a counter-example u is discovered, there are two possibilities: either (i) ACC A (u) is satisfiable, in which case u is feasible and L(A) = ∅; or (ii) ACC A (u) is unsatisfiable, in which case u is spurious. In the first case, our semi-algorithm stops and returns a witness for non-emptiness (the counter-example), obtained from the satisfying valuation of ACC A (u). In the second case, we must strengthen the invariant by excluding from INV # all pairs (β, v) such that I, β ∪ v |= ACC # A (u). This strengthening is carried out by adding to Π several predicates that are sufficient to exclude the spurious counter-example.

Given an unsatisfiable conjunction of formulae ψ 1 ∧ ψ 2 ∧ ... ∧ ψ n , an interpolant is a tuple of formulae (I 1 , I 2 , ..., I n ) such that I n ≡ ⊥, I i ∧ ψ i |= I i+1 and I i contains only variables and function symbols that are common to ψ i and ψ i+1 , for all i ∈ [1, n -1]. Moreover, by Lyndon's Interpolation Theorem [START_REF] Lyndon | An interpolation theorem in the predicate calculus[END_REF], we can assume without loss of generality that every Boolean variable with at least one positive/negative occurrence in I i has at least one positive/negative occurrence in both ψ i and ψ i+1 . In the following, we shall assume the existence of an interpolating decision procedure for T(S, I) that meets the requirements of Lyndon's Interpolation Theorem.

A classical method for abstraction refinement is to add the elements of the interpolant obtained from a proof of spuriousness to the set of predicates. This guarantees progress, meaning that the particular spurious counter-example, from which the interpolant was generated, will never be revisited in the future. Though not always, in many practical test cases, this progress property eventually yields a safety invariant.

Given a non-empty spurious counter-example u = a 1 , a 2 , ..., a n , where n > 0, we consider the following interpolation problem:

Θ(u) ≡ θ 0 (Q 0 ) ∧ θ 1 (Q 0 ∪ Q 1 , X 0 ∪ X 1 ) ∧ ... ∧ θ n (Q n-1 ∪ Q n , X n-1 ∪ X n ) ∧ θ n+1 (Q n ) where Q k = {q k | q ∈ Q} for k ∈ [0, n] are time-stamped sets of Boolean variables corresponding to the set Q of states of A. The first conjunct θ 0 (Q 0 ) ≡ ι[Q 0 /Q]
is the initial configuration of A, with every q ∈ FV Boolean (ι) replaced by q 0 . The definition of θ k for all k ∈ [1, n], uses replacement sets R j ⊆ Q j , j ∈ [0, n], which are defined inductively below:

• R 0 = FV Boolean (θ 0 ); • θ j ≡ qj-1∈Rj-1 (q j-1 → ∆(q, a j )[Q j /Q, X j-1 /X, X j /X] and R j = FV Boolean (θ j ) ∩ Q j for each j ∈ [1, n]; • θ n+1 (Q n ) ≡ q∈Q\F (q n → ⊥).
The intuition is that R 0 , R 1 , ..., R n are the sets of states replaced, θ 0 , θ 1 , ..., θ n are the sets of transition rules fired on the run of A over u and θ n+1 is the acceptance condition, which forces the last remaining non-final states to be false. We recall that a run of A over u is a sequence:

φ 0 (Q), φ 1 (Q, X 0 ∪ X 1 ), φ 2 (Q, X 0 ∪ X 1 ∪ X 2 ), ..., φ n (Q, X 0 ∪ X 1 ∪ ... ∪ X n )
where φ 0 is the initial configuration ι and for each k > 0, φ k is obtained from φ k-1 by replacing each state q ∈ FV Boolean (φ k-1 ) by the formula ∆(q, a k )[X k-1 /X, X k /X], given by the transition function of A. Observe that, because the states are replaced with transition formulae when moving one step in a run, these formulae lose track of the control history and are not suitable for producing interpolants that relate states and data.

The main idea behind the above definition of the interpolation problem is that we would like to obtain an interpolant ( , I 0 (Q), I 1 (Q, X), ..., I n (Q, X), ⊥) whose formulae combine states with the data constraints that must hold locally, whenever the control reaches a certain Boolean configuration. This association of states with data valuations is tantamount to defining efficient semi-algorithms, based on lazy abstraction. Furthermore, the abstraction defined by the interpolants generated in this way can also over-approximate the control structure of an automaton, in addition to the sets of data values encountered throughout its run.

The correctness of this interpolation-based abstraction refinement setup is captured by the progress property below, which guarantees that adding the formulae of an interpolant for Θ(u) to the set Π of predicates suffices to exclude the spurious counter-example u from future searches.

Lemma 3.3 Let A = (D, Σ, X, Q, ι, F, ∆) be an ADA, for any sequence u = a 1 , a 2 , ..., a |u| ∈ Σ * , if ACC A (u) is unsatisfiable, then: • Θ(u) is unsatisfiable; • if ( , I 0 , I 1 , ..., I n , ⊥) is an interpolant for Θ(u) such that {I i | i ∈ [0, n]} ⊆ Π, then ACC # A (u) is unsatisfiable.
In order to prove Lemma 3.3, we need to firstly see following proposition.

Proposition 3.2 Given a formula φ ∈ FORM + (Q, X) and a ∈ Σ, we have:

∆(φ, a) ⇔ ∃Q .φ[Q /Q] ∧ q∈Q (q → ∆(q, a))
Here is the proof of Proposition 3.2:

⇒ If I, β ∪ v ∪ v |= ∆(φ, a), for some valuations β : Q → B and v : X → D I , v : X → D I , then we build a valuation β : Q → B such that I, β ∪ β ∪ v ∪ v |= φ[Q /Q] ∧ q∈Q (q → ∆(q, a)).
For each occurrence of a formula ∆(q, a) in ∆(φ, a) we set β (q ) = true if I, β ∪v∪v |= ∆(q, a) and β (q ) = f alse, otherwise. Since there are no negated occurrences of such sub-formulae, the definition of β is consistent, and the check

I, β ∪ β ∪ v ∪ v |= φ[Q /Q] ∧ q∈Q (q → ∆(q, a)) is immediate.
⇐ This direction is an easy check.

Here is the proof of Lemma 3.

3. Let Θ(u) ≡ θ 0 (Q 0 ) ∧ θ 1 (Q 0 ∪ Q 1 , X 0 ∪ X 1 ) ∧ ... ∧ θ n (Q n-1 ∪ Q n , X n-1 ∪ X n ) ∧ θ n+1 (Q n ) in the following:
(1) We apply Proposition 3.2 recursively and get:

P OST # A (ι, u)[Q n /Q, X n /X] ⇐⇒ ∃Q 0 , ∃Q 1 , ..., ∃Q n-1 , ∃X 0 , ∃X 1 , ..., ∃X n-1 . n i=0 θ i
Assuming that Θ(u) is satisfiable, we obtain a model for ACC A (u)

≡ P OST A (ι, u) ∧ θ n+1 [Q/Q n ].
(2) if ( , I 0 , I 1 , ..., I n , ⊥) is an interpolant for Θ(u), the following entailments hold:

-θ 0 |= I 0 [Q 0 /Q]; -I k-1 [Q k-1 /Q, X k-1 /X] ∧ θ k |= I k [Q k /Q, X k /X], for all k ∈ [1, n]; -I n [Q n /Q] ∧ θ n+1 |= ⊥.
We prove that P OST # A (ι, a 1 , a 2 , ..., a n ) |= I n by induction on n ≥ 0. This is sufficient to conclude because

ACC # A (a 1 , a 2 , ..., a n ) ≡ P OST # A (ι, a 1 , a 2 , ..., a n ) ∧ θ n+1 [Q/Q n ] |= I n ∧ θ n+1 [Q/Q n ] |= ⊥. For the base case n = 0, we have P OST # A (ι, ε) ≡ ι ≡ θ 0 [Q/Q 0 ] |= I 0 .
For the induction step n > 0, we compute:

P OST A (ι, a 1 , a 2 , ..., a n )[Q n /Q] ≡ (by def. of P OST # A ) ∃X n-1 .∆ n (P OST # A (ι, a 1 , a 2 , ..., a n-1 ), a n ) # [Q n /Q] |= (by Proposition 3.2) ∃Q n-1 ∃X n-1 .P OST # A (ι, a 1 , a 2 , ..., a n-1 )[Q n-1 /Q] ∧ θ n |= (ind. hyp.) ∃Q n-1 ∃X n-1 .I n-1 [Q n-1 /Q] ∧ θ n |= I n [Q n /Q]
3.4 Checking Emptiness -Lazy Predicate Abstraction

Abstract Reachability Tree (ART)

In the context of checking emptiness of an ADA A = (D, Σ, X, Q, ι, F, ∆), an abstract reachability tree (ART) is a tuple T = (N, E, r, Λ, R, T, ) where:

• N is a set of nodes;

• E ⊆ N × Σ × N is a set of edges;
• r ∈ N is the root of the directed tree (N, E);

• Λ : N → FORM(Q, X
) is a labelling of the nodes with formulae such that Λ(r) = ι;

• R : N → 2 Q is a labelling of nodes with replacement sets such that R(r) = FV Boolean (ι);

• T : E → ∞ i=0 FORM + (Q i , X i , Q i+1 , X i+1
) is a labelling of edges with time-stamped formulae;

• ⊆ N × N is a set of covering edges.

Each node n ∈ N corresponds to a unique path from the root to n, labelled by a sequence λ(n) ∈ Σ * of input events. The least infeasible suffix of λ(n) is the smallest sequence v = a 1 , a 2 , ..., a k such that λ(n) = wv for some w ∈ Σ * and the following formula is unsatisfiable:

Ψ(v) ≡ Λ(p)[Q 0 /Q] ∧ θ 1 (Q 0 ∪ Q 1 , X 0 ∪ X 1 ) ∧ ... ∧ θ k+1 (Q k )
where θ 1 , θ 2 , ..., θ n+1 are defined as in the interpolation problem and

θ 0 ≡ Λ(p)[Q 0 /Q].
The pivot of n is the node p corresponding to the start of the least infeasible suffix. We assume the existence of two functions without detailing their implementation:

• FindPivot(u, T ) returning the pivot of a sequence u ∈ Σ * in an ART T ;

• LeastInfeasibleSuffix(u, T ) returning the least infeasible suffix of a sequence u ∈ Σ * in an ART T ;

Lazy Predicate Abstraction Semi-Algorithm

We now have all the ingredients to describe the first emptiness checking semi-algorithm for ADA.

Semi-Algorithm 1 builds an ART whose nodes are labelled with formulae over-approximating the concrete sets of configurations, and a covering relation between nodes in order to ensure that the set of formulae labelling the nodes in the ART forms an antichain. Any spurious counter-example is eliminated by computing an interpolant and adding its formulae to the set of predicates.

Semi-Algorithm 1 Lazy Predicate Abstraction for ADA Emptiness

Input: an ADA A = (D, Σ, X, Q, ι, F, ∆) N := N ∪ {n} the procedure returns a data word w ∈ L(A), which interleaves the input events of u with the data valuations from the model of ACC A (u). Since u is feasible, clearly ACC A (u) is satisfiable. Otherwise, u is spurious and we compute its pivot p, add the interpolants for the least infeasible suffix of u to Π, remove and recompute the sub-tree of T rooted at p. Termination of Semi-Algorithm 1 depends on the ability of a given interpolating decision procedure for the combined Boolean and data theory T(S, I) to provide interpolants that yield a safety invariant, whenever L(A) = ∅. In this case, we use the covering relation to ensure that, when a newly generated node is covered by a node already in N , it is not added to the work-list, thus cutting the current branch of the search.

Output: true if L(A) = ∅ a data word w ∈ L(A) if L(A) = ∅ 1: let T = (N, E,
Formally, for any two nodes n, m ∈ N , we have n m if and only if POST # A (Λ(n), a) |= Λ(m) for some a ∈ Σ. In other words, if n has a successor whose label entails the label of m. and since there are no other formulae than ⊥ in Π, the successor of ι ≡ q 0 is (see Figure 3.2.a). The spuriousness check for a yields the root of the ART as pivot and the interpolant (q 0 , q 1 ), which is added to the set Π. Then the node is removed and the next time a is fired, it creates a node labelled q 1 . The second sequence aa creates a successor node q 1 , which is covered by the first, depicted with a dashed arrow (see Figure 3.2.b). The third sequence is ab, which results in a new uncovered node and triggers a spurious check. The new predicate obtained from this check is x ≤ 0 ∧ q 2 ∧ y ≥ 0 and the pivot is again the root. Then the entire ART is rebuilt with the new predicates and the fourth sequence aab yields an uncovered node (see Figure 3.2.c). The new pivot is the end-point of a and the newly added predicates are q 1 ∧ q 2 and y > x -1 ∧ q 2 . Finally, the ART is rebuilt from the pivot node and finally all nodes are covered; thus proving the emptiness of the automaton (see Figure 3.2.d).

Π = {⊥} q 0 PIVOT ⊤ a add predicates {q0,q1} (𝑎) (𝑏) (𝑐) (𝑑) Π = {⊥, q 0 , q 1 } q 0 PIVOT q 1 a add predicates {x ≤ 0 ∧ q2 ∧ y ≥ 0} q 1 a ⊤ b Π = {⊥, q 0 , q 1 , x ≤ 0 ∧ q 2 ∧ y ≥ 0} q 0 PIVOT a add predicates {q 1 ∧ q 2 , y > x -1 ∧ q 2 } a ⊤ b q 1 ∧ x ≤ 0 ∧ q 2 ∧ y ≥ 0 q 1 q 1 a ⊥ b Π = {⊥, q 0 , q 1 , x ≤ 0 ∧ q 2 ∧ y ≥ 0, q 1 ∧ q 2 , y > x -1 ∧ q 2 } q 0 a q 1 ∧ x ≤ 0 ∧ q 2 ∧ y ≥ 0 PIVOT q 1 ∧ q 2 ∧ y > x -1 q 1 ∧ q 2 ∧ y > x -1 a ⊥ b a ⊥ b
Theorem 3.1 Given an ADA A = (D, Σ, X, Q, ι, F, ∆):

• if L(A) = ∅, then Semi-Algorithm 1 terminates by returning a word w ∈ L(A) (hence the termination is guaranteed when A is not empty);

• if Semi-Algorithm 1 terminates by reporting true, then L(A) = ∅ (although the termination is not guaranteed when A is empty, if the semi-algorithm terminates by reporting true, then A is surely empty, hence the correctness of the result is guaranteed).

Here is the proof of Theorem 3.1:

We prove the following invariant: each time Semi-Algorithm 1 reaches line 10, the set W of nodes in WorkList contains all the frontier nodes in the ART (N ∪ W, E, r, Λ, ) which are not covered by some node in N , namely that:

W = {n | ∀m ∈ N, ∀a ∈ Σ.(n, a, m) ∈ E ∧ (n, m) ∈ }
Initially, this is the case because W = {r} and E = = ∅. If the invariant holds previously, at line 10, it will hold again after line 26 is executed, because, when the sub-tree rooted at the pivot p is removed, p becomes a member of the set of uncovered frontier nodes, and is added to W at line 26. Otherwise, the invariant holds at line 10 and the control follows the else branch at line 29. In this case, the newly created frontier node s is added to W only if it is not covered by an existing node in N (line 32 ).

Next we prove that, if Semi-Algorithm 1 returns true, then n∈N Λ(n) defines a safety invariant. Suppose that Semi-Algorithm 1 returns at line 53. Then it must be that W = ∅. Each node in N is either covered by another node in N , or all its successors are in N . We prove first that n∈N Λ(n) is an invariant: for any u ∈ Σ * , there exists some node n ∈ N such that P OST A (ι, u) |= Λ(n). Let u ∈ Σ * be an arbitrary sequence. If u labels the path from r to some n ∈ N , we have P OST A (ι, u) |= P OST # A (ι, u) |= Λ(n) and we are done. Otherwise, let v be the (possibly empty) prefix of u which labels the path from r to some n ∈ N , which is covered by another m ∈ N , where (n, a, m) ∈ E, that is u = vav , for some a ∈ Σ and v ∈ Σ * . Moreover, we have P OST A (ι, va) |= P OST # A (ι, va) |= Λ(m), by the construction of the set of covering edges: lines line 33, line 41 and line 44. Continuing this argument recursively from m, since |v | < |u|, we shall eventually discover a node p such that P OST A (ι, u) |= Λ(p).

To prove that n∈N Λ(n) is, moreover, a safety invariant, suppose, by contradiction, that there exists u ∈ Σ * such that ACC A (u) is satisfiable. By the previous point, there exists a node p ∈ N such that P OST A (ι, u) |= Λ(p). But then we have ACC A (ι, u) |= ACC A (ι, Λ(p)), thus ACC A (ι, Λ(p)) is satisfiable as well. However, this cannot be the case, because p has been processed at line 15 and Semi-Algorithm 1 would have returned a counter-example, contradicting the assumption that it returns true. This concludes the proof that n∈N Λ(n) is a safety invariant, thus L(A) = ∅, by Lemma 3.1. We have then proved the second point of the statement.

For the first point, assume that L(A) = 0 and let w = (a 1 , v 1 ), (a 2 , v 2 ), ..., (a k , v k ) ∈ L(A) be a word. By the above, Semi-Algorithm 1 cannot return true. Suppose, by contradiction that it does not terminate. Since the sequences from Σ * are explored in breadth-first order, every sequence of length k is eventually explored, which leads to the discovery of w at line 15. Then Semi-Algorithm 1 terminates returning w ∈ L(A).

Checking Emptiness -IMPACT

In-Place Refinement and Coverage

As pointed out by a number of authors, the bottleneck of predicate abstraction is the high cost of reconstructing parts of the ART, subsequent to the refinement of the set of predicates. The main idea of the IMPACT procedure [START_REF] Kenneth | Lazy abstraction with interpolants[END_REF] is that this can be avoided and the refinement (strengthening of the node labels of the ART) can be performed in-place. This refinement step requires an update of the covering relation, because a node that used to cover another node might not cover it anymore after the strengthening of its label.

We consider a total alphabetical order ≺ on Σ and lift it to the total lexicographical order

≺ * on Σ * . A node n ∈ N is covered if (n, p) ∈ or it has an ancestor m such that (m, p) ∈ for some p ∈ N . A node n is closed if it is covered, or Λ(n) |= Λ(m) for all m ∈ N such that λ(m) ≺ * λ(n).
Observe that we use the coverage relation here with a different meaning than in Semi-Algorithm 1.

IMPACT Semi-Algorithm

The execution of Semi-Algorithm 2 consists of three phases: close, refine and expand, corresponding to the CLOSE, REFINE and EXPAND in [START_REF] Kenneth | Lazy abstraction with interpolants[END_REF].

Semi-Algorithm 2 IMPACT for ADA Emptiness

Input: an ADA A = (D, Σ, X, Q, ι, F, ∆) let (r, a 1 , n 1 ), (n 1 , a 2 , n 2 ), ..., (n k-1 , a k , n) be the path from r to n 14:

Output: true if L(A) = ∅ a data word w ∈ L(A) if L(A) = ∅ 1: let T = (N, E,
if ACC A (a 1 , a 2 , ..., a k ) is satisfiable then 15: get model (β, v 1 , v 2 , ..., v k ) of ACC A (λ(n)) 16: return w = (a 1 , v 1 ), (a 2 , v 2 ), ..., (a k , v k ) 17:
for i ∈ [0, k] do 21: if Λ(n i ) |= I i then 22: := \ {(m, n i ) ∈ | m ∈ N } 23: Λ(n i ) := Λ(n i ) ∧ I i 24:
if ¬b then let s be a fresh node

true if x is closed f alse if x is not closed 1: for y ∈ N such that λ(y) ≺ * λ(x) do 2: if Λ(x) |= Λ(y) then 3: := ( \ {(p, q) ∈ | q is x or a successor of x}) ∪ {(x, y)} 4: return true 5:
end if 6: end for 7: return f alse Let n be a node removed from the WorkList. If ACC A (λ(n)) is satisfiable, the counterexample λ(n) is feasible, in which case a model of ACC A (λ(n)) is obtained and a word w ∈ L(A) is returned. Otherwise, λ(n) is a spurious counter-example and the procedure enters the refinement phase. The interpolant for Θ(λ(n)) is used to strengthen the labels of all the ancestors of n by conjoining the formulae of the interpolant to the existing labels. In this process, the nodes on the path between 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. Observe that, in this case the call to CLOSE must uncover each node which is covered by a successor of n. This is required because, due to the over-approximation of the sets of reachable configurations, the covering relation is not transitive, as explained in [START_REF] Kenneth | Lazy abstraction with interpolants[END_REF]. If CLOSE adds a covering edge (n i , m) to , 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 by creating a new node for each successor s via the input event a ∈ Σ and inserting it into the WorkList. Theorem 3.2 Given an ADA A = (D, Σ, X, Q, ι, F, ∆):

• if L(A) = ∅,
then Semi-Algorithm 2 terminates by returning a word w ∈ L(A) (hence the termination is guaranteed when A is not empty);

• if Semi-Algorithm 2 terminates by reporting true, then L(A) = ∅ (although the termination is not guaranteed when A is empty, if the semi-algorithm terminates by reporting true, then A is surely empty, hence the correctness of the result is guaranteed).

In order to prove Theorem 3.2, we firstly introduce the following lemma: Lemma 3.4 Given an ART T = (N, E, r, Λ, R, T, ) built by Semi-Algorithm 2, we have:

P OST A (Λ(n), a) |= Λ(m), for all (n, a, m) ∈ E
Here is the proof of Lemma 3.4. We distinguish two cases. First, if (n, a, m) occurs on a path in T that has never been refined, then Λ(m) = and the entailment holds trivially. Otherwise, let Ω be the set of paths ω = (n 0 , a 1 , n 1 ), (n 1 , a 2 , n 2 ), ..., (n k-1 , a k , n k ), where n 0 = r and (n, a, m) = (n i-1 , a i , n i ), for some i ∈ [1, k] and, moreover, a 1 , a 2 , ..., a k was found, at some point, to be a spurious counter-example. Let ( , I ω 0 , I ω 1 , ..., I ω k , ⊥) be an interpolant for

Φ(a 1 , a 2 , ..., a k ) ≡ Λ(r) ∧ k i=1 θ i ∧ q∈R(n k ) (q k → ⊥), such that I ω i ∈ FORM + (Q, X), for all i ∈ [0, k].
According to Lyndon's Interpolation Theorem, it is possible to build such an interpolant, when Φ(a 1 , a 2 , ..., a k ) is unsatisfiable. By Proposition 3.2, we obtain ∆ i (

I ω i-1 , a i )[Q i /Q] ⇔ ∃Q i-1 .I ω i-1 [Q i-1 /Q, X i-1 /X] ∧ θ i and, since I ω i-1 [Q i-1 /Q, X i-1 /X] ∧ θ i |= I ω i [Q i /Q, X i /X], we obtain that ∆ i (I ω i-1 , a i )[Q i /Q] |= I ω i [Q i /Q, X i /X]. Since Λ(n i-1 ) = ω∈Ω I ω i-1 and Λ(n i ) = ω∈Ω I ω i , we obtain P OST A (Λ(n i-1 ), a i ) |= Λ(n i ).
Now we can prove Theorem 3.2. We prove first that, each time Semi-Algorithm 2 reaches the line 10, we have:

W = {n | n uncovered, ∃a ∈ Σ ∀s ∈ N.(n, a, s) ∈ E} (1)
Initially, W = {r} and E = = ∅, thus (1) holds trivially. Suppose that (1) holds at when reaching line 10 and some node n was removed from W and inserted into N . We distinguish two cases, either:

• n is covered, in which case W becomes W \ {n} and (1) holds, or

• n is not covered, in which case W becomes (W \ {n} ∪ S), where S = {s ∈ N | (n, a, s) ∈ E, a ∈ Σ} is the set of fresh successors of n. But then no node s ∈ S is covered and has successors in E, thus (1) holds.

Then the condition (1) holds next time line 10 is reached, thus it is invariant.

Suppose first that Semi-Algorithm 2 returns true, thus W = ∅ and, by (1), for each node in n ∈ N one of the following hold:

• n is covered, or • for each a ∈ Σ there exists s ∈ N such that (n, a, s) ∈ E.

We prove that, in this case, n∈N Λ(n) defines a safety invariant and conclude that L(A) = ∅, by Lemma 3.2. To this end, let u = a 1 , a 2 , ..., a k ∈ Σ * be an arbitrary sequence and let v 1 be the largest prefix of u that labels a path from r to some node n 1 ∈ N . If v 1 = u we are done. Otherwise, by the choice of v 1 , it must be the case that a successor of n 1 is missing from (N, E), thus n 1 must be covered, by [START_REF]Smt2 format[END_REF] and the fact that W = ∅. Let n 1 be the closest ancestor of n 1 such that (n 1 , n 1 ) ∈ , for some n 1 ∈ N , and let v 1 be the prefix of v 1 leading to n 1 . By the construction of , we have Λ(n 1 ) |= Λ(n 1 ). Applying Lemma 3.4 inductively on v 1 , we obtain that P OST A (ι, v 1 ) |= Λ(n 1 ), thus P OST A (ι, v 1 ) |= Λ(n 1 ). Continuing inductively from n 1 , we exhibit a sequence of strings v 1 , v 2 , ..., v l ∈ Σ * and nodes r = m 0 , m 1 , ..., m l such that, for all i ∈ [1, l]:

• v i labels the path between m i-1 and m 1 in (N, E);

• P OST A (ι, v 1 , v 2 , ..., v i ) |= Λ(m i ).
Moreover, we have u = v 1 , v 2 , ..., v k , thus P OST A (ι, u) |= Λ(m k ) and we are done showing that n∈N Λ(n) is an invariant.

To prove that n∈N Λ(n) is, moreover, a safety invariant, suppose that ACC A (u) is satisfiable, for some u ∈ Σ * and let n ∈ N be a node such that P OST A (ι, u) |= Λ(n). By the previous point, such a node must exist. But then ACC A (u) |= ACC A (λ(n)), thus ACC A (λ(n)) is satisfiable, and Semi-Algorithm 2 returns at line 16, upon encountering λ(n). But this contradicts the assumption that Semi-Algorithm 2 returns true, hence we have proved that n∈N Λ(n) is a safety invariant, and L(A) = ∅ follows, by Lemma 3.2. We have then proved the second point of the statement.

To prove the first point, assume that L(A) = ∅. By the previous point, Semi-Algorithm 2 does not return true. Suppose, by contradiction, that it does not terminate and conclude using the breadth-first argument from the proof of Theorem 3.1.

Example 3.4

We show the execution of Semi-Algorithm 2 on the ADA in Figure 3.1. Initially, the procedure fires the sequence a, whose end-point is labelled with (see Figure 3.3.a). Since this node is uncovered, we check the spuriousness of the counter-example and refine the label of the node to q 1 . Since the node is still uncovered, two successors labelled with are computed, corresponding to the sequences aa and ab (see Figure 3.3.b). The spuriousness check for aa yields the interpolant (q 0 , x ≤ 0 ∧ q 2 ∧ y ≥ 0)) which strengthens the label of the end-point of a from q 1 to q 1 ∧ x ≤ 0 ∧ q 2 ∧ y ≥ 0. The sequence ab is also found to be spurious, which changes the label of its end-point from to ⊥, and also covers it (depicted with a dashed edge). Since the end-point of aa is not covered, it is expanded to aaa and aab (see Figure 3.3.c). Both sequences aaa and aab are found to be spurious, and the end-point of aab, whose label has changed from to ⊥, is now covered. In the process, the label of aa has also changed from q 1 to q 1 ∧y > x-1∧q 2 , due to the strengthening with the interpolant from aab. Finally, the only uncovered node aaa is expanded to aaaa and aaab, both found to be spurious (see Figure 3.3.d). The refinement of aaab causes the label of aaa to change from q 1 to q 1 ∧ y > x -1 ∧ q 2 and this node is now covered by aa. Since its successors are also covered, there are no uncovered nodes and the procedure returns true.

q 0 ⊤ a refined q1 (𝑎)
q0 [0] → q1 [1] ∧ q2 [1] ∧ x [1] = 1 ∧ y [1] = 0 q 0 q 1 a q0 [0] → q1 [1] ∧ q2 [1] ∧ x [1] = 1 ∧ y [1] = 0 refined [1] → q1 [2] ∧ q2 [2] ∧ x [2] = y [1] + 1 ∧ y [2] = x [1] + 1) ∧ (q 2 [1] → q 2 [2] ∧ x [2] > x [1] ∧ y [2] > y [1] ) b (q1 [1] → q3 [2] ∧ x [1] ≥ y [1] ) ∧ (q 2 [1] → q 4 [2] ∧ x [1] > y [1] ) refined ⊥ refined q 1

q 1 ∧ x ≤ 0 ∧ q 2 ∧ y ≥ 0 ⊤ ⊤ a (q1
(𝑏) (𝑐) q 0 q 1 ∧ x ≤ 0 ∧ q 2 ∧ y ≥ 0 a q0 [0] → q1 [1] ∧ q2 [1] ∧ x [1] = 1 ∧ y [1] = 0 ⊥ q 1 a (q1 [1] → q1 [2] ∧ q2 [2] ∧ x [2] = y [1] + 1 ∧ y [2] = x [1] + 1) ∧ (q2 [1] → q2 [2] ∧ x [2] > x [1] ∧ y [2] > y [1] ) b (q1 [1] → q3 [2] ∧ x [1] ≥ y [1] ) ∧ (q 2 [1] → q 4 [2] ∧ x [1] > y [1] ) ⊤ b ⊤ a (q1 [2] → q3 [3] ∧ x [2] ≥ y [2] ) ∧ (q2 [2] → q4 [3] ∧ x [2] > y [2] ) refined

⊥ refined q1 refined q1 ∧ y > x -1 ∧ q2
(q 1 [2] → q 1 [3] ∧ q 2 [3] ∧ x [3] = y [2] + 1

∧ y [3] = x [2] + 1) ∧ (q2 [2] → q2 [3] ∧ x [3] > x [2] ∧ y [3] > y [2] ) [1] ∧ x [1] = 1 ∧ y [1] = 0 ⊥ q 1 ∧ y > x -1 ∧ q 2 a (q 1 [1] → q 1 [2] ∧ q 2 [2] ∧ x [2] = y [1] + 1 ∧ y [2] = x [1] + 1) ∧ (q2 [1] → q2 [2] ∧ x [2] > x [1] ∧ y [2] > y [1] ) b (q1 [1] → q3 [2] ∧ x [1] ≥ y [1] ) ∧ (q 2 [1] → q 4 [2] ∧ x [1] > y [1] ) ⊥ b q 1 a (q1 [2] → q3 [3] ∧ x [2] ≥ y [2] ) ∧ (q 2 [2] → q 4 [3] ∧ x [2] > y [2] ) (q1 [2] → q1 [3] ∧ q2 [3] ∧ x [3] = y [2] + 1 ∧ y [3] = x [2] + 1) ∧ (q 2 [2] → q 2 [3] ∧ x [3] > x [2] ∧ y [3] > y [2] )

(𝑑) q 0 q 1 ∧ x ≤ 0 ∧ q 2 ∧ y ≥ 0 a q 0 [0] → q 1 [1] ∧ q 2
refined q 1 ∧ y > x -1 ∧ q 2 ⊤ refined q 1 ⊤ refined ⊥ b a
(q1 [3] → q1 [4] ∧ q2 [4] ∧ x [4] = y [3] + 1 ∧ y [4] = x [3] + 1) ∧ (q2 [3] → q2 [4] ∧ x [4] > x [3] ∧ y [4] > y [3] ) (q1 [3] → q3 [4] ∧ x [3] ≥ y [3] )

∧ (q 2 [3] → q 4 [4] ∧ x [3] > y [4] ) First-Order Alternating Data Automata (FOADA)

Many results in formal language theory rely on the assumption that languages are defined over finite alphabets. In practice, this assumption is problematic when attempting to use automata as models of real-time systems or even simple programs, whose input and observable output require taking into account data values, ranging over very large domains, better viewed as infinite mathematical abstractions.

Alternating automata are a generalisation of non-deterministic automata with universal transitions, that create several copies of the automaton, which synchronise on the same input word. Alternating automata are appealing for verification because they allow encoding of problems such as temporal logic model checking in linear time, as opposed to the exponential time required by non-deterministic automata [START_REF] Vardi | Alternating Automata and Program Verification[END_REF]. A finite-alphabet alternating automaton is typically described by a set of transition rules q a -→ φ, where q is a state, a is an input symbol and φ is a positive Boolean combinations of states, viewed as propositional variables.

In this chapter, we introduce a generalisation of Boolean alternating automata, called First-Order Alternating Data Automata (FOADA), in which transition rules are described by multisorted first order formulae, with states and internal variables given by uninterpreted predicate terms. The model is closed under union, intersection and complement, and its emptiness problem is undecidable, even for the simplest data theory of equality. To cope with this limitation, we develop an abstraction refinement semi-algorithm based on lazy annotation of the symbolic execution paths with interpolants, obtained by applying: (i) quantifier elimination with witness term generation and (ii) Lyndon interpolation in the quantifier-free data theory with uninterpreted predicate symbols. This provides a method for checking inclusion of timed and finite-memory register automata, and emptiness of quantified predicate automata, previously used in the verification of parameterised concurrent programs, composed of replicated threads, with a shared-memory communication model.

Introduction of FOADA

Data Words

Let Σ be a finite alphabet of input events. Given a finite set of variables X ⊆ VAR, we denote by X → D the set of valuations of the variables X and Σ[X] = Σ × (X → D) be the possibly infinite set of data symbols (a, v), where a is an input symbol and v is a valuation.

A data word is a finite sequence w = (a 1 , v 1 ), (a 2 , v 2 ), ..., (a n , v n ) of data symbols. Given a word w, we denote by w Σ def = == = a 1 , a 2 , ..., a n its sequence of input events and by w D the valuation associating each time-stamped variable x [i] the value v i (x), for all x ∈ VAR and i ∈ [1, n]. We denote by ε the empty sequence, by Σ * the set of finite sequences of input events and by Σ[X] * the set of data words over the variables X.

Definition of FOADA

A first-order alternating data automaton (FOADA) is a tuple A = (D, Σ, X, Q, ι, F, ∆) where:

• D is a possibly infinite data domain;

• Σ is a finite alphabet of input events;

• X ⊂ VAR is a finite set of variables of sort D;

• Q is a finite set of predicates denoting control states;

• ι ∈ FORM + (Q, ∅) is a sentence defining initial configurations;
• F ⊆ Q is the set of predicates denoting final states;

• ∆ is a set of transition rules of the form q(y 1 , y 2 , ..., y #(q) ) a(X) ---→ ψ where q ∈ Q is predicate, a ∈ Σ is an input event and ψ ∈ FORM + (Q, X ∪ {y 1 , y 2 , ..., y #(q) }) is a positive formula, where X ∩ {y 1 , y 2 , ..., y #(q) } = ∅.

The intuition of a transition rule q(y 1 , y 2 , ..., y #(q) ) a(X) ---→ ψ is the following: a is the input event and X are the input data values that trigger the transition, whereas q and y 1 , y 2 , ..., y #(q) are the current control state and data values in that state, respectively. Without loss of generality, we consider, for each predicate q ∈ Q and each input event a ∈ Σ, 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 referred to as transition quantifiers. The size of A is defined as

|A| = |ι| + q(y) a(X) ---→ψ∈∆ |ψ|.

Execution Semantic

The execution semantics of FOADA is given in close analogy with the case of Boolean alternating automata, with transition rules of the form q a -→ φ, where q is a Boolean constant and φ a positive Boolean combination of such constants. For instance, q 0 a -→ q 1 ∧q 2 ∨q 3 means that the automaton can choose to transition in either, both q 1 and q 2 , or, in q 3 alone. This intuition leads to saying that the steps of the automaton are defined by the minimal Boolean models of the transition formulae. In this case, both {q 1 ← , q 2 ← , q 3 ← ⊥} and {q 1 ← ⊥, q 2 ← ⊥, q 3 ← } are minimal models, however, {q 1 ← , q 2 ← , q 3 ← } is also a model but is not minimal. The original definition of alternating finite-state automata [START_REF] Ashok | [END_REF] works around this problem by considering Boolean valuations (models) instead of formulae. However, describing FOADA using interpretations instead of formulae would be rather hard to follow. Let A = (D, Σ, X, Q, ι, F, ∆) be a FOADA. Given a predicate q ∈ Q and a tuple of data values d 1 , d 2 , ..., d #(q) , then q(d 1 , d 2 , ..., d #(q) ) is called a configuration. To formalise the execution semantics of automata, we relate sets of configurations to models of first-order sentences. Each first-order interpretation I corresponds to a set of configurations C(I) Definition 4.1 Given a word w = (a 1 , v 1 ), (a 2 , v 2 ), ..., (a n , v n ) ∈ Σ[X] * and a cube c, an execution of a FOADA A = (D, Σ, X, Q, ι, F, ∆) over w, starting with c, is a possibly infinite forest T = {T 1 , T 2 , ...}, where each T i is a tree labelled with configurations, such that: • all paths in T have the same length n;

def = == = {q(d 1 , d 2 , ..., d #(q) ) | q ∈ Q, (d 1 , d 2 , ..., d #(q) ) ∈ q I }, called a cube.
• c = {T ( ) | T ∈ T } is the set of configurations labelling the roots of T 1 , T 2 , ...; • if q(d 1 , d 2 , ..., d #(q) ) labels a node on the level j ∈ [1, n -1] in T i , then the labels of its children form a cube from C([[ψ]] µ η ), where η = v j+1 [y 1 ← d 1 , y 2 ← d 2 , ..., y #(q) ← d #(q) ] and q(y 1 , y 2 , ..., y #(q) ) aj+1(X) -----→ ψ ∈ ∆ is a transition rule of A.
• the frontier of each tree T ∈ T is labelled with final configurations q(d 1 , d 2 , ..., d #(q) ), where q ∈ F .

If A has an accepting execution over w starting with a cube c ∈ C([[ι]] µ ), then A accepts w and let L(A) be the set of words accepted by A.

Symbolic Execution of FOADA 4.2.1 Path Formulae

In the upcoming developments, it is sometimes more convenient to work with logical formulae defining executions of automata, than with low-level execution forests. For this reason, we first introduce path formulae Θ(α), which are formulae defining the executions of an automaton, over words that share a given sequence α of input events.

Let A = (D, Σ, X, Q, ι, F, ∆) be a FOADA. For any i ∈ N, we denote by:

• Q [i] = {q [i] | q ∈ Q} • X [i] = {x [i] | x ∈ X}
the sets of time-stamped predicates and variables, respectively. As a shorthand, we write Q [≤n] (resp. X [≤n] ) for the set {q

[i] | q ∈ Q, i ∈ [1, n]} (resp. {x [i] | x ∈ X, i ∈ [1, n]}). For a formula ψ and i ∈ N, we define ψ [i] def = == = ψ[X [i] /X, Q [i]
/Q] the formula in which all input variables and state predicates (and only those symbols) are replaced by their time-stamped counterparts. As a shorthand, we shall write q(y) for q(y 1 , y 2 , ..., y #(q) ) when no confusion arises. Given a sequence of input events α = a 1 , a 2 , ..., a n ∈ Σ * , the path formula of α is:

Θ(α) def = == = ι [0] ∧ n i=1 q(y) a i (X)
----→ψ∈∆ ∀y 1 , ∀y 2 , ..., ∀y #(q) .q [i-1] (y) → ψ [i] The automaton A, to which Θ(α) refers, will always be clear from the context. To formalise the relation between the low-level configuration-based execution semantics and the symbolic path formulae, consider a word w = (a 1 , v 1 ), (a 2 , v 2 ), ..., (a n , v n ) ∈ Σ[X] * . Any execution forest T of A over w is associated an interpretation I T of the set of time-stamped predicates Q [≤n] , defined as:

I T (q [i] ) def = == = {(d 1 , d 2 , ..., d #(q) ) | q(d 1 , d 2 , ..., d #(q) ) labels a node on T i }, ∀q ∈ Q, ∀i ∈ [1, n]
where T i refers to the level i in T .

Lemma 4.1 Given a first-order alternating data automaton A = (D, Σ, X, Q, ι, F, ∆), for any word w = (a 1 , v 1 ), (a 2 , v 2 ), ..., (a n , v n ) ∈ Σ[X] * , we have:

[[Θ(w Σ )]] µ w D = {I T | T is an execution of A over w}.
Here is the proof of Lemma 4.1:

⊆: Let I be a minimal interpretation such that I, w D |= Θ(w Σ ). We show that there exists an execution T of A over w such that I = I T , by induction on n ≥ 0. For n = 0, we have w = ε and Θ(w Σ ) = ι [0] . Because ι is a sentence, the valuation w D is not important in I, Θ(w Σ ) |= ι [0] and, moreover, since I is minimal, we have I ∈ [[ι [0] ]] µ . We define the interpretation J (q) = I(q [0] ), for all q ∈ Q. Then C(J ) is an execution of A over ε and I = I C(J ) is immediate. For the inductive case n > 0, we assume that w = u • (a n , v n ) for a word u. Let J be the interpretation defined as I for all q [i] , with q ∈ Q and i ∈ [1, n -1], and ∅ everywhere else. Then J , u D |= Θ(u Σ ) and J is moreover minimal. By the induction hypothesis, there exists an execution G of A over u, such that J = I G . Consider a leaf of a tree T ∈ G, labelled with a configuration q(d 1 , d 2 , ..., d #(q) ) and let ∀y 1 , ∀y 2 , ..., ∀y #(q) .q [n-1] (y) → ψ [n] be the sub-formula of Θ(w Σ ) corresponding to the application(s) of the transition rule q(y)

an --→ ψ at the (n -1)-th step. Let v = w D [y 1 ← d 1 , y 2 ← d 2 , ..., y #(q) ← d #(q)
]. Because I, w D |= ∀y 1 , ∀y 2 , ..., ∀y #(q) .q [n-1] (y) → ψ [n] , we have I ∈ [[ψ [n] ]] v and let K be one of the minimal interpretations such that K ⊆ I and K ∈ [[ψ [n] ]] v . It is not hard to see that K exists and is unique, otherwise we could take the point-wise intersection of two or more such interpretations. We define the interpretation K(q) = K(q [n] ) for all q ∈ Q. We have that K ∈ [[ψ]] µ v if K was not minimal, K was not minimal to start with, contradiction. Then we extend the execution G by appending to each node labelled with a configuration q(d 1 , d 2 , ..., d #(q) ) the cube C(K). By repeating this step for all leaves of a tree in G, we obtain an execution of A over w.

⊇: Let T be an execution of A over w. We show that I T is a minimal interpretation such that I T , w D |= Θ(w Σ ), by induction on n ≥ 0. For n = 0, T is a cube from C([[ι]] µ ), by definition. Then I T |= ι [0] and moreover, it is a minimal such interpretation. For the inductive case n > 0, let w = u • (a n , v n ) for a word u. Let G be the restriction of T to u. Consequently, I G is the restriction of I T to Q [≤n -1] . By the inductive hypothesis, I G is a minimal interpretation such that I G , u D |= Θ(u Σ ). Since

I T (q [n] ) = {(d 1 , d 2 , ..., d #(q) ) | q(d 1 , d 2 , ..., d #(q)
) labels a node on the n-th level in T }, we have I T , w D |= ϕ, for each sub-formula ϕ = ∀y 1 , ∀y 2 , ..., ∀y #(q) .q [n-1] (y) → ψ [n] of Θ(w Σ ), by the execution semantics of A. This is the case because the children of each node labelled with q(d 1 , d 2 , ..., d #(q) ) on the (n-1)-th level of T form a cube from C([[ψ]] µ v ), where v is a valuation that assigns each y i the value d i and behaves like w D , otherwise. Now suppose, for a contradiction, that I T is not minimal and let J I T be an interpretation such that J , w D |= Θ(w Σ ). First, we show that the restriction J of J to

n-1 i=0 Q [i]
must coincide with I G . Assuming this is not the case, i.e. J I G , contradicts the minimality of I G . Then the only possibility is that

J (q [n] ) I T (q [n] ), for some q ∈ Q. Let p 1 (y 1 , y 2 , ..., y #(p1) ) an --→ ψ 1 , p 2 (y 1 , y 2 , ..., y #(p2) ) an --→ ψ 2 , ..., p k (y 1 , y 2 , ..., y #(p k ) )
an --→ ψ k be the set of transition rules in which the predicate symbol q occurs on the right-hand side. Then it must be the case that, for some node on the (n -1)-th level of G, labelled with a configuration p i (d 1 , d 2 , ..., d #(pi) ), the set of children does not form a minimal cube from

C([[ψ [n]

i ]] µ ), which contradicts the execution semantics of A.

Acceptance Formulae

Now we give a logical characterisation of acceptance, relative to given sequence of input events α ∈ Σ * . To this end, we constrain the path formula Θ(α) by requiring that only final states of A occur on the last level of the execution. The result is the acceptance formula for α:

Υ(α) def = == = Θ(α) ∧ q∈Q\F ∀y 1 , ∀y 2 , ..., ∀y #(q) .q [n] (y) → ⊥
The top-level universal quantifiers from a sub-formula ∀y 1 , ∀y 2 , ..., ∀y #(q) .q [i] (y) → ψ of Υ(α) will be referred to as path quantifiers, in the following. Notice that path quantifiers are distinct from the transition quantifiers that occur within a formula ψ of a transition rule

q(y 1 , y 2 , ...y #(q) ) a(X) ---→ ψ of A.
The acceptance formula Υ(A) is false in every interpretation of the predicates that assigns a non-empty set to a non-final predicate occurring on the last level in the execution forest. The relation between the words accepted by A and the acceptance formula above, is formally captured by the lemma below. A = (D,Σ,X,Q,ι,F,∆), for every word w ∈ Σ[X] * , the following are equivalent:

Lemma 4.2 Given an automaton

(1) there exists an interpretation I such that I, w D |= Υ(w Σ );

(2) w ∈ L(A).

Here is the proof of Lemma 4.2:

1⇒2 Let I be an interpretation such that I, w D |= Υ(w Σ ). We know that A has an execution T over w such that I = I T . To prove that T is accepting, we show that (i) all paths in T have length n and that (ii) the frontier of T is labelled with final configurations only. First, assume that (i) there exists a path in T of length 0 ≤ m < n. Then there exists a node on the m-th level, labelled with some configuration q(d 1 , d 2 , ..., d #(q) , that has no children. By the definition of the execution semantics of A, we have C([[ψ]] µ η ) = ∅, where q(y) am+1(X) ------→ ψ is the transition rule of A that applies for q and a m+1 and η = w D [y 1 ← d 1 , y 2 ← d 2 , ..., y #(q) ← d #(q) ]. Hence [[ψ]] η = ∅, and because I, w D |= Υ(α), we obtain that I, η |= q(y) → ψ [m+1] , thus (d 1 , d 2 , ..., d #(q) ) ∈ I(q). However, this contradicts the fact that I = I T and that q(d 1 , d 2 , ..., d #(q) ) labels a node of T . Second, assume that (ii), there exists a frontier node of T labelled with a configuration q(d 1 , d 2 , ..., d #(q) ) such that q ∈ Q \ F . Since I, w D |= ∀y 1 , ∀y 2 , ..., ∀y #(q) .q(y) → ⊥, by a similar reasoning as in the above case, we obtain that (d 1 , d 2 , ..., d #(q) ) ∈ I(q), contradiction. 2⇒1 Let T be an accepting execution of A over w. We can prove that I T , w D |= Υ(w Σ ). By Lemma 4.1, we obtain I T , w D |= Θ(w Σ ). Since every path in T is of length n and all nodes on the n-th level of T are labelled by final configurations, we can here obtain that I T , w D |= q∈Q\F ∀y 1 , ∀y 2 , ..., ∀y #(q) .q [n] (y) → ⊥, trivially.

As an immediate consequence, one can decide whether A accepts some word w with a given input sequence w Σ = α, by checking whether Υ(α) is satisfiable. However, unlike non-alternating infinite-state models of computation, such as counter automata (non-deterministic programs with integer variables), the satisfiability query for an acceptance (path) formula falls outside of known decidable theories, supported by standard SMT solvers. There are basically two reasons for this, namely (i) the presence of predicate symbols, and (ii) the non-trivial alternation of quantifiers. To understand this point, consider for example, the decidable theory of Presburger arithmetic [START_REF] Presburger | Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen[END_REF]. Adding even only one monadic predicate symbol to it yields undecidability in the presence of non-trivial quantifier alternation [START_REF] Joseph | Presburger arithmetic with unary predicates is π11 complete[END_REF]. However the quantifier-free fragment of Presburger arithmetic extended with predicate symbols can be shown to be decidable, using a Nelson-Oppen style congruence closure argument [START_REF] Nelson | Fast decision procedures based on congruence closure[END_REF].

To tackle this problem, we start from the observation that acceptance formulae have a particular form, which allows the elimination of path quantifiers and of predicates, by a couple of satisfiability-preserving transformations. The result of applying these transformations is a formula with no predicate symbols, whose only quantifiers are those introduced by the transition rules of the automaton, referred to as transition quantifiers. We shall further assume that the first order theory of the data sort D has quantifier elimination, which allows to effectively decide the satisfiability of such formulae. The next two sections introduce the elimination of path quantifiers and predicates.

Elimination of Path Quantifiers

Consider a given sequence of input events α = a 1 , a 2 , ..., a n and denote by α i the prefix a 1 , a 2 , ..., a i of α for i ∈ [1, n] where α 0 = ε. Definition 4.3 Let Θ(α 0 ), Θ(α 1 ), ..., Θ(α n ) be the sequence of formulae defined by:

• Θ(α 0 ) def = == = ι [0] ; • Θ(α i ) def = == = Θ(α i-1 ) ∧ cond1,cond2 q [i-1] (t 1 , t 2 , ..., t #(q) ) → ψ [i] [t 1 /y 1 , t 2 /y 2 , ..., t #(q) /y #(q) ] for i ∈ [1, n] where cond1: q [i-1] (t 1 , t 2 , ..., t #(q) ) occurs in Θ(α i-1 )
and cond2: q(y 1 , y 2 , ..., y #(q) ) ai(X) ----→ ψ ∈ ∆ We write Υ(α) for the prenex normal form of the formula:

Θ(α n ) ∧ q [n] (t1,t2,...,t #(q) ) occurs in Θ(αn),q∈Q\F q [n] (t 1 , t 2 , ..., t #(q) ) → ⊥
Observe that Υ(α) contains no path quantifiers, as required. On the other hand, the scope of the transition quantifiers in Υ(α) exceeds the right-hand side formulae from the transition rules, as shown by the following example.

Example 4.1 Consider an automaton A = (N, {a 1 , a 2 }, {x}, {q, q f }, ι, {q f }, ∆) where:

• ι = ∃z.z ≥ 0 ∧ q(z);

• ∆ = {q(y) a1(x) ---→ x ≥ 0 ∧ ∀z.z ≤ y → q(x + z), q(y) a2(x) ---→ y < 0 ∧ q f (x + y)}.
For the input event sequence α = a 1 a 2 , the acceptance formula is: [1] ≥ 0 ∧ ∀z.z ≥ y → q [1] (x [1] + z)]∧ ∀y.q [1]

Υ(α) =∃z.z ≥ 0 ∧ q [0] (z)∧ ∀y.q [0] (y) → [x
(y) → [y < 0 ∧ q [2] f (x [2] + y)]
The result of eliminating the path quantifiers, in prenex normal form, is shown below:

Υ(α) =∃z 1 ∀z 2 .z 1 ≥ 0 ∧ q [0] (z 1 )
[q [0] (z 1 ) → x [1] ≥ 0 ∧ (z 2 ≥ z 1 → q [1] (x [1] + z 2 ))]∧ [q [1] (x [1]

+ z 2 ) → x [1] + z 2 < 0 ∧ q [2]
f (x [2] + x [1]

+ z 2 )]
Now we show a formal relation between the satisfiability of an acceptance formula Υ(α) and that of the formula Υ(α), obtained by eliminating the path quantifiers from Υ(α). • if there exists an interpretation I such that I, v |= Υ(α) then there exists an interpretation J ⊆ I such that J , v |= Υ(α).

Here is the proof of Lemma 4.3:

(1) Trivial, since every sub-formula q(t 1 , t 2 , ..., t #(q) ) → ψ[t 1 /y 1 , t 2 /y 2 , ..., t #(q) /y #(q) ] of Υ is entailed by a sub-formula ∀y 1 , ∀y 2 , ..., ∀y #(q) .q(y 1 , y 2 , ..., y #(q) ) → ψ of Υ(α).

(2) By repeated applications of Fact 4.1.

Fact 4.1 Given formulae φ and ψ, such that no predicate atom with predicate symbol q occurs in ψ(y 1 , y 2 , ..., y #(q) ), for each valuation v, if there exists an interpretation I such that I, v |= φ ∧ q(t1,t2,...,t #(q) ) occurs in φ q(t 1 , t 2 , ..., t #(q) ) → ψ[t 1 /y 1 , t 2 /y 2 , ..., t #(q) /y #(q) ] then there exists a valuation J such that J (q) ⊆ I(q) and J (q ) ⊆ I(q ) for all q ∈ Q \ {q} and J , v |= φ ∧ ∀y 1 , ∀y 2 , ..., ∀y #(q) .q(y 1 , y 2 , ..., y #(q) ) → ψ.

Here is the proof of Fact 4.1:

Assume w.l.o.g. that φ is quantifier free. The proof can be easily generalised to the case where φ has quantifiers. Let J (q) = {(t v 1 , t v 2 , ..., t v #(q) ) ∈ I(q) | q(t 1 , t 2 , ..., t #(q) ) occurs in φ} and J (q ) ⊆ I(q ) for all q ∈ Q \ {q}. Since I, v |= φ, we obtain also that J , v |= φ because the tuples of values in I(q) \ J (q) are not interpretations of terms that occur within sub-formulae q(t 1 , t 2 , ..., t #(q) ) of φ. Moreover, two formulae:

(1) q(t1,t2,...,t #(q) ) occurs in φ q(t 1 , t 2 , ..., t #(q) ) → ψ[t 1 /y 1 , t 2 /y 2 , ..., t #(q) /y #(q) ] (2) ∀y 1 , ∀y 2 , ..., ∀y #(q) .q(y 1 , y 2 , ..., y #(q) ) → ψ

(1) and ( 2) are equivalent under J , thus J , v |= ∀y 1 , ∀y 2 , ..., ∀y #(q) .q(y 1 , y 2 , ..., y #(q) ) → ψ, as required. This concludes the proof.

Elimination of Predicate Atoms

We proceed with the elimination of predicate atoms from Υ(α) defined below. Definition 4.4 Let Θ(α 0 ), Θ(α 1 ), ..., Θ(α n ) be the sequence of formulae defined by Θ(α 0 ) def = == = ι [0] and, for all i ∈ [1, n], Θ(α i ) is obtained by replacing each occurrence of a predicate atom

q [i-1] (t 1 , t 2 , ..., t #(q) ) in Θ(α i-1
) by the formula ψ [i] [t 1 /y 1 , t 2 /y 2 , ..., t #(q) /y #(q) ], where q(y) ai(X) ----→ ψ ∈ ∆. We write Υ(α) for the formula obtained by replacing, in Θ(α), each occurrence of a predicate q [n] , such that q ∈ Q \ F (resp. q ∈ F ), by ⊥ (resp. ).

Υ(α) = ∃z 1 ∀z 2 .z 1 ≥ 0 ∧ [x [1] ≥ 0 ∧ (z 2 ≥ z 1 → x [1] + z 2 < 0)]
Since this formula is unsatisfiable, no word w with input event sequence w Σ = a 1 a 2 is accepted by the automaton A from Example 4.1.

At this point, we prove the formal relation between the satisfiability of the formulae Υ(α) and Υ(α). Since there are no occurrences of predicates in Υ(α), for each valuation v : X [≤n] → D, there exists an interpretation I such that I, v |= Υ(α) if and only if J , v |= Υ(α), for every interpretation J . In this case we omit I and simply write v |= Υ(α). Here is the proof of Lemma 4.4 by induction on n ≥ 0:

• The base case n = 0 is trivial, since Υ(A) = Υ(A) = ι [0] .
• For the induction step, we rely on Fact 4.2. Fact 4.2 Given formulae φ and ψ, such that φ is positive, q(t 1 , t 2 , ..., t #(q) ) is the only one occurrence of the predicate symbol q in φ and no predicate atom with predicate symbol q occurs in ψ(y 1 , y 2 , ..., y #(q) ), for each interpretation I and each valuation v, we have:

I, v |= φ ∧ q(t 1 , t 2 , ..., t #(q) ) → ψ[t 1 /y 1 , t 2 /y 2 , ..., t #(q) /y #(q) ] ⇔ v |= φ[ψ[t 1 /y 1 , t 2 /y 2 , ..., t #(q) /y #(q) ]/q(t 1 , t 2 , ..., t #(q) )].
Here is the proof of Fact 4.2. We assume w.l.o.g. that φ is quantifier-free. The proof can be easily generalised to the case φ has quantifiers:

⇒ We distinguish two cases: -if (t v 1 , t v 2 , ..., t v #(q) ) ∈ I(q) then I, v |= ψ[t 1 /y 1 , t 2 /y 2 , ..., t #(q) /y #(q)
]. Since φ is positive, replacing q(t 1 , t 2 , ..., t #(q) ) with ψ[t 1 /y 1 , t 2 /y 2 , ..., t #(q) /y #(q) ] does not change the truth value of φ under v, thus:

v |= φ[ψ[t 1 /y 1 , t 2 /y 2 , ..., t #(q) /y #(q) ]/q(t 1 , t 2 , ..., t #(q) )]; -else, (t v 1 , t v 2 , ..., t v #(q) ) ∈ I(q), thus v |= φ[⊥/q(t 1 , t 2 , ..., t #(q) )
]. Since φ is positive and ⊥ entails ψ[t 1 /y 1 , t 2 /y 2 , ..., t #(q) /y #(q) ], we obtain:

v |= φ[ψ[t 1 /y 1 , t 2 /
y 2 , ..., t #(q) /y #(q) ]/q(t 1 , t 2 , ..., t #(q) )] by monotonicity.

⇐ Let I(q) = {(t v 1 , t v 2 , ..., t v #(q) ) | v |= ψ[t 1 /y 1 , t 2 /y 2 , .
.., t #(q) /y #(q) ]}. We distinguish two cases:

-if I(q) = ∅, then I, v |= q(t 1 , t 2 , ..., t #(q) ) and v |= ψ[t 1 /y 1 , t 2 /y 2 , ..., t #(q) /y #(q) ].
Thus replacing ψ[t 1 /y 1 , t 2 /y 2 , ..., t #(q) /y #(q) ] by q(t 1 , t 2 , ..., t #(q) ) does not change the truth value of φ under I and v, and we obtain I, v |= φ. Moreover, I, v |= ψ[t 1 /y 1 , t 2 /y 2 , ..., t #(q) /y #(q) ] implies I, v |= q(t 1 , t 2 , ..., t #(q) ) → ψ[t 1 /y 1 , t 2 /y 2 , ..., t #(q) /y #(q) ].

else

I(q) = ∅, hence v |= ψ[t 1 /y 1 , t 2 /y 2 , ..., t #(q) /y #(q) ], thus v |= φ[⊥/q(t 1 , t 2 , ..., t #(q) )]. Because φ is positive, we obtain I, v |= φ by monotonicity. But I, v |= q(t 1 , t 2 , ..., t #(q) ) → ψ[t 1 /y 1 , t 2 /y 2 , ..., t #(q) /y #(q) ] trivially, because I, v |= q(t 1 , t 2 , ..., t #(q) ).
Finally, we define the acceptance of a word with a given input event sequence by means of a formula in which no predicate atom occurs. As previously discussed, several decidable theories, such as Presburger arithmetic, become undecidable if predicate atoms are added to them. Therefore, the result below makes a step forward towards deciding whether the automaton accepts a word with a given input sequence, by reducing this problem to the satisfiability of a quantified formula without predicates.

Lemma 4.5 Given an automaton

A = (D, Σ, X, Q, ι, F, ∆), for every word w ∈ Σ[X] * , we have w D |= Υ(w Σ ) if and only if w ∈ L(A).
Here is the proof of Lemma 4.5:

• By Lemma 4.2, w ∈ L(A) if and only if I, w D |= Υ(w Σ ), for some interpretation I;

• By Lemma 4.3 there exists an interpretation I such that I, w D |= Υ(w Σ ) if and only if there exists an interpretation J such that J , v |= Υ(w Σ );

• By Lemma 4.4 there exists an interpretation J such that J , v |= Υ(w Σ ) if and only if v |= Υ(w Σ ).

Closure Properties of FOADA

Given a positive formula φ, we define the dual formula φ recursively as follows:

• φ 1 ∨ φ 2 = φ 1 ∧ φ 2 • φ 1 ∧ φ 2 = φ 1 ∨ φ 2 • t ≈ s = ¬(t ≈ s) • ¬(t ≈ s) = (t ≈ s) • ∃x.φ 1 = ∀x.φ 1 • ∀x.φ 1 = ∃x.φ 1 • q(x 1 , x 2 , ..., x #(q) ) = q(x 1 , x 2 , ..., x #(q) )
Observe that, because predicate atoms do not occur negated in φ, there is no need to define dualisation for formulae of the form ¬q(x 1 , x 2 , ..., x #(q) ). The following theorem shows closure of automata under all Boolean operations.

Theorem 4.1 Given two automata

A 1 = (D, Σ, X, Q 1 , ι 1 , F 1 , ∆ 1 ) and A 2 = (D, Σ, X, Q 2 , ι 2 , F 2 , ∆ 2 ), such that Q 1 ∩ Q 2 = ∅, the following hold: • L(A ∩ ) = L(A 1 ) ∩ L(A 2 ), where A ∩ = (D, Σ, X, Q 1 ∪ Q 2 , ι 1 ∧ ι 2 , F 1 ∪ F 2 , ∆ 1 ∪ ∆ 2 ); • L(A i ) = Σ[X] * \ L(A i ), where A i = (D, Σ, X, Q i , ι i , Q i \ F i , ∆ i ) and for i = 1, 2: ∆ i = {q(y) a(X) ---→ ψ | q(y) a(X) ---→ ψ ∈ ∆ i }. Moreover, |A ∩ | = O(|A 1 | + |A 2 |) and |A i | = O(|A i |) for all i = 1, 2.
Here is the proof of Theorem 4.1:

(1) ⊆ Let w ∈ L(A ∩ ) be a word and T be an execution of A ∩ over w.

Since Q 1 ∩ Q 2 = ∅,
it is possible to partition T into T 1 and T 2 such that the roots of T i form a cube from C([[ι i ]] µ ), for all i = 1, 2. Because ∆ 1 ∩ ∆ 2 = ∅, by induction on |w| ≥ 0, one shows that T i is an execution of A i over w, for all i = 1, 2. Finally, because T is accepting, we obtain that T i and T 2 are accepting, respectively, hence w ∈ L(A 1 ) ∩ L(A 2 ).

⊇ Let w ∈ L(A 1 ) ∩ L(A 2 ) and let T i an accepting execution of A i over w, for all i = 1, 2.

We show that T 1 ∪ T 2 is an execution of A ∩ over w, by induction on |w| ≥ 0. For the base case |w| = 0, we have

T i ∈ C([[ι i ]] µ ) for all i = 1, 2 and since Q 1 ∩ Q 2 = ∅, we have T i ∪ T 2 ∈ C([[ι 1 ∧ ι 2 ]] µ ))
. The induction step follows as a consequence of the fact that ∆ 1 ∪ ∆ 2 is the set of transition rules of A ∩ . Finally, since both T 1 and T 2 are accepting, T i ∪ T 2 is accepting as well. Moreover, we have:

|A ∩ | = |ι 1 ∧ι 2 |+ q(y) a(X) ---→ψ∈∆1∪∆2 |ψ| = 1+|ι 1 |+|ι 2 |+ q(y) a(X) ---→ψ∈∆1 |ψ|+ q(y) a(X) ---→ψ∈∆2 |ψ| (2) Let w ∈ Σ[X]
* be a word. We denote by Υ A1 (w Σ ) and Υ A1 (w Σ ) (resp. Υ A1 (w Σ ) and Υ A1 (w Σ )) the formulae Υ(w Σ ) and Υ(w Σ ) for A 1 and A 1 , respectively. It is enough to show that Υ A1 (w Σ ) = ¬Υ A1 (w Σ ) and apply Lemma 4.5 to prove that w ∈ L(A 1 ) ⇔ w ∈ L(A 1 ). Since the choice of w was arbitrary, this proves

L(A 1 ) = Σ[X] * \ L(A 1 )
. By induction on the number of predicate atoms in Υ A1 (w Σ ) that are replaced during the generation of Υ A1 (w Σ ). The proof relies on the following fact:

Fact 4.3 Let φ be a positive formula and let q(t 1 , t 2 , ..., t #(q) ) be the only occurrence of a predicate symbol within φ. Then, every formula φ with no predicate occurrences:

¬φ[ψ[t 1 /y 1 , t 2 /y 2 , ..., t #(q) /y #(q) ]/q(t 1 , t 2 , ..., t #(q) )]

≡ φ[¬ψ[t 1 /y 1 , t 2 /y 2 , ..., t #(q) /y #(q) ]/q(t 1 , t 2 , ..., t #(q) )]

The proof of Fact 4.3 can be done by induction on the structure of φ.

Emptiness Problem of FOADA 4.4.1 Unfoldings of FOADA

Given a finite input event alphabet Σ, for two sequences α, β ∈ Σ * , we say that α is a prefix of β, written α β, if α = βγ for some sequence γ ∈ Σ * . A set S of sequences is:

• prefix-closed if for each α ∈ S, if β α then β ∈ S;
• complete if for each α ∈ S, there exists α ∈ Σ such that αa ∈ S if and only if αb ∈ S for all b ∈ Σ.

Definition 4.5 An unfolding of a first-order alternating data automaton A = (D, Σ, X, Q, ι, F, ∆) is a finite partial mapping U : Σ * → f in FORM + (Q, ∅), such that:

• DOM(U ) is a finite prefix-closed complete set;

• U (ε) = ι;

• for each sequence αa ∈ DOM(U ), such that α ∈ Σ * and a ∈ Σ:

U (α) [0] ∧ q(y) a(X)
---→ψ ∀y 1 , ∀y 2 , ..., ∀y #(q) .q [0] (y) → ψ [1] |= U (αa) [1] Moreover, U is safe if for each α ∈ DOM(U ), the formula U (α)∧ q∈Q\F ∀y 1 , ∀y 2 , ..., ∀y #(q) .q(y) → ⊥ is unsatisfiable.

IMPACT Semi-Algorithm

The problem of checking emptiness of a given automaton is undecidable, even for automata with predicates of arity two, whose transition rules use only equality and dis-equality, having no transition quantifiers [START_REF] Farzan | Proof spaces for unbounded parallelism[END_REF]. 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 [START_REF] Kenneth | Lazy abstraction with interpolants[END_REF][START_REF] Kenneth | Lazy annotation revisited[END_REF].

In a nutshell, a lazy annotation procedure systematically explores the set of execution paths (in our case, sequences of input events) in search of an accepting execution. Each path has a corresponding path formula that defines all words accepted along that path. If the path formula is satisfiable, the automaton accepts a word. Otherwise, the path is said to be spurious. When a spurious path is encountered, the search backtracks and the path is annotated with a set of learned facts, that marks this path as infeasible. The semi-algorithm uses moreover a coverage relation between paths, ensuring that the continuations of already covered paths are never explored. Sometimes this coverage relation provides a sound termination argument, when the automaton is empty.

We check emptiness of first order alternating automata using a version of the IMPACT lazy annotation semi-algorithm [START_REF] Kenneth | Lazy abstraction with interpolants[END_REF].

Semi-Algorithm 3 IMPACT for FOADA Emptiness

Input: a FOADA A = (D, Σ, X, Q, ι, F, ∆) Output: true if L(A) = ∅ a data word w ∈ L(A) if L(A) = ∅ 1: let U = (N, E, r, U, ) be an unfolding tree 2: let WorkList be a list Function 2 CLOSE Input: a node x Output: true if x is closed f alse if x is not closed 1: for y ∈ N such that α(y) ≺ * α(x) do 2: if U (x) |= U (y)
:= ( \ {(p, q) ∈ | q is x or a successor of x}) ∪ {(x, y)} 4:
return true

5:

end if 6: end for 7: return f alse Lazy annotation semi-algorithms [START_REF] Kenneth | Lazy abstraction with interpolants[END_REF][START_REF] Kenneth | Lazy annotation revisited[END_REF] build unfoldings of automata trying to discover counter-examples for emptiness. If the automaton A in question is non-empty, a systematic enumeration of the input event sequences (for instance, using breadth-first search) from Σ * will suffice to discover a word w ∈ L(A), provided that the first order theory of the data domain D is decidable (Lemma 4.2). However, if L(A) = ∅, 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.

Definition 4.6 Given an unfolding U of an automaton

A = (D, Σ, X, Q, ι, F, ∆) a node α ∈ DOM(U ) is covered by another node β ∈ DOM(U ), denoted α
β if and only if there exists a node α α such that U (α ) |= U (β). Moreover, U is closed if and only if every leaf from DOM(U ) is covered by an uncovered node.

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, for any three nodes of an unfolding U , say α, β, γ ∈ DOM(U ), if α ≺ β and α γ, then β γ as well. There is no need to expand covered nodes, because, intuitively, there exists a word w ∈ L(A) such that α w Σ and α γ only if there exists another word u ∈ L(A) such that γ u Σ . Hence, exploring only those input event sequences that are continuations of γ (and ignoring those of α) suffices in order to find a counter-example for emptiness, if one exists.

An unfolding node α ∈ DOM(U ) is said to be spurious if and only if Υ(α) is unsatisfiable. In this case, we change (refine) the labels of (some of the) prefixes of α (and that of α), such that U (α) becomes ⊥, 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 γ α used to cover another node from DOM(U ), it might not cover it with the new label. Therefore, the coverage relation has to be recomputed after each refinement of the labelling. The semi-algorithm stops when (and if) a safe complete unfolding has been found. The proof is not that complicated. Let U be a safe and complete unfolding of A, such that DOM(U ) = ∅. Suppose, by contradiction, that there exists a word w ∈ L(A) and let

α def = == = w Σ .
Since w ∈ L(A), by Lemma 4.2, there exists an interpretation I such that I, w D |= Υ(α). Assume first that α ∈ DOM(U ). In this case, one can show, by induction on the length n ≥ 0 of w, that Θ(α) |= U (α) [n] , thus I, w D |= U (α) [n] . Since I, w D |= Υ(α), we have I, w D |= q∈Q\F ∀y 1 , ∀y 2 , ..., ∀y #(q) .q [n] (y) → ⊥, hence U (α) [n] ∧ q∈Q\F ∀y 1 , ∀y 2 , ..., ∀y #(q) .q [n] (y) → ⊥. By renaming q [n] with q in the previous formula, we obtain U (α) ∧ ∀y 1 , ∀y 2 , ..., ∀y #(q) .q(y) → ⊥ is satisfiable, thus U is not safe, contradiction.

We proceed thus under the assumption that α ∈ DOM(U ). Since DOM(U ) is a non-empty prefix-closed set, there exists a strict prefix α of α that is a leaf of DOM(U ). Since U is closed, the leaf α must be covered and let α 1 α α be a node such that U (α 1 ) |= U (β 1 ), for some uncovered node β 1 ∈ DOM(U ). Let γ 1 be the unique sequence such that α 1 γ 1 = α. Since α 1 β 1 and w Σ = α 1 γ 1 ∈ L(A), there exists a word w 1 and a cube c

1 ∈ C([[U (α 1 )]]) ⊆ C([[U (β 1 )]]), such that w 1Σ = γ 1 and A accepts w 1 starting with c 1 . If β 1 γ 1 ∈ DOM(U )
, we obtain a contradiction by a similar argument as above. Hence β 1 γ 1 ∈ DOM(U ) and there exists a leaf of DOM(U ) which is also a prefix of β 1 γ 1 . Since U is closed, this leaf is covered by an uncovered node β 2 ∈ DOM(U ) and let α 2 ∈ DOM(U ) be the minimal (in the prefix partial order) node such that β 1 α 2 β 1 γ 1 and α 2 β 2 . Let γ 2 be the unique sequence such that α 2 γ 2 = β 1 γ 1 . Since β 1 is uncovered, we have β 1 = α 2 and thus |γ 1 | > |γ 2 |. By repeating the above reasoning for α 2 , β 2 and γ 2 , we obtain an infinite sequence |γ 1 | > |γ 2 | > ..., which is again a contradiction.

As mentioned above, we check emptiness of first order alternating automata using the same method previously used to check emptiness of a simpler model of alternating automata, which uses Boolean constants for control states and whose transition rules have no quantifiers [START_REF] Iosif | Abstraction refinement for emptiness checking of alternating data automata[END_REF]. The higher complexity of the automata model considered here, manifests itself within the interpolant generation procedure, used to refine the labelling of the unfolding. We discuss generation of interpolants in the next section.

Interpolant Generation of FOADA

Over-Approximation and Interpolants

Typically, when checking the unreachability of a set of program configurations [START_REF] Kenneth | Lazy abstraction with interpolants[END_REF], 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. However, in an alternating model of computation, it is useful to 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 defined by formulae involving a single predicate symbol, whereas time-local interpolants involve only predicates q [i] and variables x [i] , for a single i ≥ 0.

When considering an alternating model of computation, control-local interpolants are not always enough to prove emptiness, because of the synchronisation of several branches of the computation on the same sequence of input values.

Example 4.3 Consider, a FOADA with the following transition rules and final state q f :

• q 0 (y) a(x) ---→ q 1 (y + x) ∧ q 2 (y -x) • q 1 (y) a(x) ---→ y + x > 0 ∧ q f • q 1 (y) a(x) ---→ q 1 (y + x) • q 2 (y) a(x) ---→ y -x > 0 ∧ q f • q 2 (y) a(x) ---→ q 2 (y -x)
Started in an initial configuration q 0 (0) with an input word (a, v 1 ), (a, v 2 ), ..., (a, v n-1 ), (a, v n ), such that v i (x) = k i , the automaton executes as follows:

q 0 (0) (a,v1) ----→ {q 1 (k 1 ), q 2 (-k 1 )} (a,v2) ----→ ... (a,vn-1) -----→ {q 1 ( n-1 i=1 k i ), q 2 (- n-1 i=1 k i )} (a,vn) ----→ ∅
An over-approximation of the set of cubes generated after one or more steps is defined by the formula ∃x 1 ∃x 2 .q 1 (x 1 ) ∧ q 2 (x 2 ) ∧ x 1 + x 2 ≈ 0. Observe that a control-local formula using one occurrence of a predicate would give a too rough over-approximation of this set, unable to prove the emptiness of the automaton.

In the rest of this section, let us fix an automaton A = (D, Σ, X, Q, ι, F, ∆). Due to the above observation, none of the interpolants considered will be control-local and we shall use the term local to denote time-local interpolants, with no free variables. Definition 4.7 Given a non-empty sequence of input events α = a 1 , a 2 , ..., a n ∈ Σ * , a generalised Lyndon interpolant (GLI) is a sequence (I 0 , I 1 , ..., I n ) of formulae such that, for all k ∈ [1, n -1]:

• P -(I k ) = ∅; • ι [0] |= I 0 and I k ∧ ( q(y) a i (X)
----→ψ∈∆ ∀y 1 , ∀y 2 , ..., ∀y #(q) .q [k] (y) → ψ [k+1] ) |= I k+1 ;

• I n ∧ q∈Q\F ∀y 1 , ∀y 2 , ..., ∀y #(q) .q(y) is unsatisfiable.

Moreover, the GLI is local if and only if

V (I k ) ⊆ Q [k] , for all k ∈ [1, n].
The following proposition states the existence of local GLI for the theories in which Lyndon's Interpolation Theorem holds. If there exists a Lyndon interpolant for any two formulae φ and ψ, such that φ ∧ ψ is unsatisfiable, then any sequence of input events α = a 1 , a 2 , ..., a n ∈ Σ * , such that Υ(α) is unsatisfiable, has a local GLI (I 0 , I 1 , ..., I n ). Here is the proof. By definition, Υ(α) is the formula:

ι [0] ∧ n i=1 q(y) a i (X)
----→ψ∈∆ ∀y 1 , ∀y 2 , ..., ∀y #(q) .q [i-1] (y) → ψ [i] ∧ q∈Q\F ∀y 1 , ∀y 2 , ..., ∀y #(q) .q [n] (y) → ⊥

We define the formulae:

• ϕ i def = == = q(y) a i (X)
----→ψ∈∆ ∀y 1 , ∀y 2 , ..., ∀y #(q) .q [i-1] (y) → ψ [i] , for all i ∈ [1, n]

• ψ def = == = q∈Q\F ∀y 1 , ∀y 2 , ..., ∀y #(q) .q [n] (y) → ⊥

Observe that V (ι [0] ) ⊆ Q [0] , V (ϕ i ) ⊆ Q [i-1] ∪ Q [i] ∪ X [i]
, for all i ∈ [1, n], and V (ψ) ⊆ Q [n] . We apply Lyndon's Interpolation Theorem for the formulae ι [0] and n i=1 ϕ i ∧ ψ and obtain a formula

I 0 , such that ι [0] |= I 0 , I 0 ∧ n i=1 ϕ i ∧ ψ is unsatisfiable, V (I 0 ) ⊆ V (ι [0] ) ∩ ( n i=1 V (ϕ i ) ∪ V (ψ)) ⊆ Q [0]
and

P -(I 0 ) ⊆ P -(ι [0] ) ∩ ( n i=1 P -(ϕ i ) ∪ P -(ψ)) = ∅.
Repeating the reasoning for the formulae

I 0 ∧ ϕ 1 and n i=2 ϕ i ∧ ψ, we obtain I 1 , such that I 0 ∧ ϕ 1 |= I 1 , I 1 ∧ n i=2 ϕ i ∧ ψ is unsatisfiable, V (I 1 ) ⊆ (V (I 0 ) ∪ V (ϕ 1 )) ∩ ( n i=2
V (ϕ i ) ∪ V (ψ)) ⊆ Q [1] and P -(I 1 ) ⊆ (P

-(I 0 ) ∪ P -(ϕ 1 )) ∩ ( n i=2 P -(ϕ i )∪P -(ψ)) = ∅.
Continuing in this way, we obtain formulae (I 0 , I 1 , ..., I n ) as required.

The main problem with the local GLI construction described in the proof of above is that the existence of Lyndon interpolants is guaranteed in principle, but the proof is non-constructive. Building an interpolant for an unsatisfiable conjunction of formulae φ ∧ ψ is typically the job of the decision procedure that proves the unsatisfiability and, in general, there is no such procedure, when φ and ψ 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.) [START_REF] Rybalchenko | Constraint solving for interpolation[END_REF]. This is where the predicate-free path formulae come into play. For a given event sequence α, the automaton A accepts a word w such that w Σ = α if and only if Υ(α) is satisfiable. Assuming further that the equality atoms in the transition rules of A are written in the language of a decidable first order theory, such as Presburger arithmetic, Lemma 4.5 gives us an effective way of checking emptiness of 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 Υ(α), the interpolants needed to annotate α. This is because (i) the formula Υ(α), obtained by repeated substitutions loses track of the steps of the execution, and (ii) quantifiers that occur nested in Υ(α) make it difficult to write Υ(α) as an unsatisfiable conjunction of formulae from which interpolants are extracted.

The solution we adopt for the first issue (i) consists in partially recovering the time-stamped structure of the acceptance formula Υ(α) using the formula Υ(α) in which only transition quantifiers occur. The second issue (ii) is solved under the additional assumption that the theory of the data domain D has witness-producing quantifier elimination. More precisely, we assume that, for each formula ∃x.φ(x), there exists an effectively computable term τ , in which x does not occur, such that ∃x.φ(x) and φ[τ /x] are equisatisfiable. These terms, called witness terms in the following, are actual definitions of the Skolem function symbols from the following folklore theorem.

Theorem 4.3 [11] Given Q 1 x 1 Q 2 x 2 ...Q n x n .φ a first-order sentence, where Q 1 , Q 2 , ..., Q n ∈ {∃, ∀} and φ is quantifier-free, let η i def = == = f i (y 1 , y 2 , ..., y ki ) if Q i = ∀ and η i def = == = x i if Q i = ∃,
where f i is a fresh function symbol and {y 1 , y 2 , ...,

y ki } = {x j | j < i, Q j = ∃}. Then the entailment Q 1 x 1 Q 2 x 2 ...Q n x n .φ |= φ[η 1 /x 1 , η 2 /x 2 , ..., η n /x n ] holds.
See Theorem 2.1.8 and Lemma 2.1.9 in [START_REF] Börger | The Classical Decision Problem[END_REF] for the proof of Theorem 4.3.

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) [START_REF] Kuncak | Software synthesis procedures[END_REF].

Under the assumption that witness terms can be effectively built, let us describe the generation of a non-local GLI for a given input event sequence α = a 1 , a 2 , ..., a n . First, we generate successively the acceptance formula Υ(α) and its equisatisfiable forms Υ(α

) = Q 1 x 1 Q 2 x 2 ...Q m x m . Φ and Υ(α) = Q 1 x 1 Q 2 x 2 ...Q m x m . Φ,
both written in prenex form, with matrices Φ and Φ, respectively. Because we assumed that the first order theory of D has quantifier elimination, the satisfiability problem for Υ(α) is decidable. If Υ(α) is satisfiable, we build a counter-example for emptiness w such that w Σ = α and w D is a satisfying assignment for Υ(α). Otherwise, Υ(α) is unsatisfiable and there exist witness terms τ i1 , τ i2 , ..., τ i l , where {i

1 , i 2 , ..., i l } = {j ∈ [1, m] | Q j = ∀}, such that Φ[τ i1 /x i1 , τ i2 /x i2 , ..., τ i l /x i l ]
is unsatisfiable. Then it turns out that the formula Φ[τ i1 /x i1 , τ i2 /x i2 , ..., τ i l /x i l ], obtained analogously from the matrix of Υ(α), is unsatisfiable as well. Because this latter formula is structured as a conjunction of formulae

ι [0] ∧ φ 1 ∧ φ 2 ∧ ... ∧ φ n ∧ ψ, where V (φ k ) ∩ Q [≤n] ⊆ Q [k-1] ∪ Q [k] and V (ψ) ∩ Q [≤n] ⊆ Q [n]
, it is now possible to use an existing interpolation procedure for the quantifier-free theory of D, extended with uninterpreted function symbols, to compute a sequence of non-local GLI (I 0 , I 1 , ..., I n ) such that

V (I k ) ∩ Q [≤n] ⊆ Q [k] for all k ∈ [1, n].
Example 4.4 The formula Υ(α) in Example 4.2 is unsatisfiable and let τ 2 = z 1 be the witness term for the universally quantified variable z 2 . Replacing z 2 with τ 2 in the matrix of Υ(α) in Example 4.1 yields the unsatisfiable conjunction: [1] ≥ 0 ∧ (z 1 ≥ z 1 → q [1] (x [1] + z 1 ))∧ q [1] (x [1] + z 1 ) → x [1]

z 1 ≥ 0 ∧ q [0] (z 1 ) ∧ q [0] (z 1 ) → x
+ z 1 < 0 ∧ q [2]
f (x [2] + x [1] + z 1 )

A non-local GLI for the above is: [1] ≥ 0 ∧ q [1] (x [1] Lemma 4.6 Given a non-empty input event sequence α = a 1 , a 2 , ..., a n ∈ Σ * , such that Υ(α) is unsatisfiable, let Q 1 x 1 Q 2 x 2 ...Q m x m . Φ be a prenex form of Υ(α) and let ξ : [1, m] → [1, n] be a monotonic function mapping each transition quantifier to the minimal index from the sequence Θ(α 0 ), Θ(α 1 ), ..., Θ(α n ) where it occurs. Then one can effectively build:

(q [0] (z 1 ) ∧ z 1 ≥ 0, x
+ z 1 ) ∧ z 1 ≥ 0, ⊥) A function ξ : N → N is (i) [
• witness terms τ i1 , τ i2 , ..., τ i l , where {i

1 , i 2 , ..., i l } = {j ∈ [1, m] | Q j = ∀} and V (τ ij ) ⊆ X [≤ξ(ij )] ∪ {x k | k < i j , Q k = ∃}, ∀j ∈ [1, l] such that Φ[τ i1 /x i1 , τ i2 /x i2 , ..., τ i l /x i l ] is unsatisfiable; • a GLI (I 0 , I 1 , ..., I n ) for α, such that V (I k ) ⊆ Q [k] ∪ X [≤k] ∪ {x j | j < ξ -1 (k), Q j = ∃}, for all k ∈ [1, n].
Here is the proof of Lemma 4.6:

(1) If Υ(α) is unsatisfiable, by Lemma 4.3 and Lemma 4.4, we obtain that, successively Υ(α) and Υ(α) are unsatisfiable.

Let Q 1 x 1 Q 2 x 2 ...Q m x m . Φ and Q 1 x 1 Q 2 x 2 ...Q m x m .
Φ be prenex forms for Υ(α) and Υ(α), respectively. Since we assumed that the first order theory of the data domain has witness-producing quantifier elimination, one can effectively build witness terms τ i1 , τ i2 , ..., τ i l , where {i

1 , i 2 , ..., i l } = {i ∈ [1, m] | Q i = ∀} and: -V (τ ij ) ⊆ X [≤ξ(ij )] ∪ {x k | k < i j , Q k = ∃}, for all j ∈ [1, l];
-Φ[τ i1 /x i1 , τ i2 /x i2 , ..., τ i l /x i l ] is unsatisfiable.

Let Φ 0 , Φ 1 , ..., Φ n be the sequence of quantifier-free formulae, defined as follows:

-Φ 0 is the matrix of some prenex form of ι [0] ;

for all i = 1, 2, ..., n, let Φ i be the matrix of some prenex form of:

Φ i def = == = Φ i-1 ∧ cond1,cond2
q [i-1] (t 1 , t 2 , ..., t #(q) ) → ψ [i] [t 1 /y 1 , t 2 /y 2 , ..., t #(q) /y #(q) ] def = == =φi where cond1 : q [i-1] (t 1 , t 2 , ..., t #(q) ) occurs in Φ i-1

and cond2 : q(y 1 , y 2 , ..., y #(q) ) ai(X)

----→ ψ ∈ ∆
It is easy to see that Φ is the matrix of some prenex form of:

Φ n ∧ q [n
] (t1,t2,...,t #(q) ) occurs in Φn,q∈Q\F

q [n] (t 1 , t 2 , ..., t #(q) ) → ⊥ def = == =ψ
We can obtain a sequence of quantifier-free formulae Φ 0 , Φ 1 , ..., Φ n such that Φ i ≡ Φ i , for all i ∈ [1, n] and Φ is obtained from Φ n by replacing each occurrence of a predicate atom q(t 1 , t 2 , ..., t #(q) ) in Φ n by ⊥ if q ∈ Q \ F and by if q ∈ F . Clearly Φ ≡ Φ, thus Φ[τ i1 /x i1 , τ i2 /x i2 , ..., τ i l /x i l ] ≡ Φ[τ i1 /x i1 , τ i2 /x i2 , ..., τ i l /x i l ] ≡ ⊥.

(2) With the notation introduced at (1), we have Φ = Φ 0 ∧ n i=1 φ i ∧ ψ. Consider the sequence of witness terms τ i1 , τ i2 , ..., τ i l , whose existence is provided by [START_REF]Smt2 format[END_REF]. Because

V (τ ij ) ⊆ X [≤ξ(ij )] ∪ {x k | k < i j , Q k = ∃} for all j ∈ [1, l],
and moreover ξ -1 is strictly monotonic, we obtain:

-V ( Φ 0 [τ i1 /x i1 , τ i2 /x i2 , ..., τ i l /x i l ]) ⊆ Q [0] ∪ X [0] ∪ {x j | j < ξ -1 max (0), Q j = ∃}; -V (φ i [τ i1 /x i1 , τ i2 /x i2 , ..., τ i l /x i l ]) ⊆ Q [i-1] ∪ Q [i] ∪ X [≤i] ∪ {x j | j < ξ -1 max (i), Q j = ∃} for all i ∈ [1, n]; -V (ψ[τ i1 /x i1 , τ i2 /x i2 , ..., τ i l /x i l ]) ⊆ Q [n] ∪ X [≤n] ∪ {x j | j ∈ [1, m], Q j = ∃}.
By repeatedly applying Lyndon's Interpolation Theorem, we obtain a sequence of formulae (I 0 , I 1 , ..., I n ) such that:

-Φ 0 [τ i1 /x i1 , τ i2 /x i2 , ..., τ i l /x i l ] |= I 0 and V (I 0 ) ⊆ Q [0] ∪ X [0] ∪ {x j | j < ξ -1 max (0), Q j = ∃}; -I k-1 ∧ φ i [τ i1 /x i1 , τ i2 /x i2 , ..., τ i l /x i l ] |= I k and V (I k ) ⊆ Q [k] ∪ X [≤k] ∪ {x j | j < ξ -1 max (k), Q j = ∃} for all k ∈ [1, n]; -I n ∧ ψ[τ i1 /x i1 , τ i2 /x i2 , ..., τ i l /x i l ] is unsatisfiable.
To show that (I 0 , I 1 , ..., I n ) is a GLI for a 1 , a 2 , ..., a n , it is sufficient to notice that:

q(y) a k (X)
----→ψ∈∆ ∀y 1 , ∀y 2 , ..., ∀y #(q) .q [k]

-I k-1 ∧ ( q(y) a k (X)
----→ψ∈∆ ∀y 1 , ∀y 2 , ..., ∀y #(q) .q

[k-1] (y) → ψ [k] ) |= I k-1 ∧ φ k |= I k ; -I n ∧ ( q∈Q\F ∀y 1 , ∀y 2 , ..., ∀y #(q) .q(y) → ⊥) |= I n ∧ ψ |= ⊥.
In conclusion, under two assumptions about the first order theory of the data domain, namely the (i) witness-producing quantifier elimination, and (ii) Lyndon interpolation for the quantifierfree fragment with uninterpreted functions, we developed a rather generic method that produces generalised Lyndon interpolants for infeasible input event sequences. Moreover, each formula I k in the interpolant refers only to the current predicate symbols Q [I k ] , the current and past input variables X [≤k] and the existentially quantified transition variables introduced at the previous steps {x j | j < ξ -1 max (k), Q j = ∃}. The remaining question is how to use such non-local interpolants to label the unfolding of an automaton and to compute the coverage between nodes of the unfolding.

Unfolding with Non-local Interpolants

The unfolding U of an automaton A = (D, Σ, X, Q, ι, F, ∆) is labelled by formulae U (α) ∈ FORM + (Q, ∅), with no free symbols, other than predicate symbols, such that the labelling is compatible with the transition relation of the automaton. The following lemma describes the refinement of the labelling of an input sequence α of length n by a non-local GLI (I 0 , I 1 , ..., I n ), such that V (I k ) ⊆ Q [k] ∪ X [≤k] ∪ X k where X k are the existentially quantified variables from the prenex normal form of Υ(α k ). Lemma 4.7 Let U be an unfolding of an automaton A = (D, Σ, X, Q, ι, F, ∆) such that α = a 1 , a 2 , ..., a n ∈ DOM(U ) and (I 0 , I 1 , ..., I n ) be a GLI for α. The mapping U : DOM(U ) → FORM + (Q, ∅) defined as:

• U (α k ) = U (α k ) ∧ J k , for all k ∈ [1, n],
where J k is the formula obtained from I k by replacing each time-stamped predicate symbol q(k) by q and existentially quantifying each free variable in I k ;

• U (β) = U (β) if β ∈ DOM(U ) and β α;
is an unfolding of A.

The proof of Lemma 4.7 is not complicated. The new set of formulae U (α 0 ), U (α 1 ), ..., U (α n ) complies with Definition 4.5, because:

• U (α 0 ) ≡ ι, since, by point 2 of Definition 4.7, we have ι [0] |= I 0 , thus ι |= J 0 and

U (α 0 ) = U (α 0 ) ∧ J 0 ≡ ι ∧ J 0 ≡ ι;
• by point 3 of Definition 4.7, we have, for all k ∈ [1, n -1]:

I k ∧ q(y) a k (X)
----→ψ∈∆ ∀y 1 , ∀y 2 , ..., ∀y #(q) .q [k] (y) → ψ [k+1] |= I k+1

We write I j k for the formula in which each predicate symbol q [k] is replaced by q [j] . Then the following entailment holds:

I 0 k ∧ q(y) a k (X)
----→ψ∈∆ ∀y 1 , ∀y 2 , ..., ∀y #(q) .q [0] (y) → ψ [1] |= I 1 k+1

Because J k is obtained by removing the time stamps from the predicate symbols and existentially quantifying all the free variables of I k , we also obtain, by applying Fact 4.4 below:

J [0] k ∧ q(y) a k (X)
----→ψ∈∆ ∀y 1 , ∀y 2 , ..., ∀y #(q) .q [0] (y) → ψ [1] |= J [START_REF]Smt2 format[END_REF] k+1

Since U satisfies the labelling condition of Definition 4.5 and U (α k ) = U (α k ) ∧ J k , we obtain, as required:

U (α k ) [0] ∧ q(y) a k (X)
----→ψ∈∆ ∀y 1 , ∀y 2 , ..., ∀y #(q) .q [0] (y) → ψ [1] |= U (α k+1 ) [1] Fact 4.4 Given formulae φ(x, y) and ψ(x) such that φ(x, y) |= ψ(x), we also have ∃x.φ(x, y) |= ∃x.ψ(x).

The proof of Fact 4.4 is quite simple. For each choice of a valuation for the existentially quantified variables on the left-hand side, we chose the same valuation for the variables on the right-hand side.

Observe that, by Lemma 4.6, the set of free variables of a GLI formula I k consists of (i) variables X [≤k] keeping track of data values seen in the input at some earlier moment in time, and (ii) variables that track past choices made within the transition rules. Basically, it is not important when exactly in the past a certain input has been read or when a choice has been made, as only the value of the variable determines the future behaviour. Intuitively, existential quantification of these variables does the job of ignoring when in the past these values have been seen.

The last ingredient of the lazy annotation semi-algorithm based on unfoldings consist in the implementation of the coverage check, when the unfolding of an automaton is labelled with conjunctions of existentially quantified formulae with predicate symbols, obtained from interpolation. By Definition 4.6, checking whether a given node α ∈ DOM(U ) is covered amounts to finding a prefix α α and a node β ∈ DOM(U ) such that U (α ) |= U (β), or equivalently, the formula U (α ) ∧ ¬U (β) is unsatisfiable. However, the latter formula, in prenex form, has quantifier prefix in the language ∃ * ∀ * and, as previously mentioned, the satisfiability problem for such formulae becomes undecidable when the data theory subsumes Presburger arithmetic [START_REF] Joseph | Presburger arithmetic with unary predicates is π11 complete[END_REF].

Nevertheless, if we require just a yes/no answer (i.e. not an interpolant) recently developed quantifier instantiation heuristics [START_REF] Reynolds | Solving quantified linear arithmetic by counterexample-guided instantiation[END_REF] perform rather well in answering a large number of queries in this class. Observe, moreover, that coverage does not need to rely on a complete decision procedure. If the prover fails in answering the above satisfiability query, then the semi-algorithm assumes that the node is not covered and continues exploring its successors. Failure to compute complete coverage may lead to divergence (non-termination) and ultimately, to failure to prove emptiness, but does not affect the soundness of the semi-algorithm (real counter-examples will still be found).

Chapter 5 Applications

The main application of first-order alternating data automata (FOADA) is checking inclusions between various classes of automata extended with variables ranging over infinite domains that recognise languages over infinite alphabets. The most widely known such classes are timed automata [START_REF] Alur | A theory of timed automata[END_REF] and finite-memory automata [START_REF] Kaminski | Finite-memory automata[END_REF] (also called register automata). In both cases, complementation is not possible inside the class and inclusion is undecidable. Our contribution is providing a systematic semi-algorithm for these decision problems. In addition, the method described in Section 4.4 can extend generic register automata inclusion checking framework [START_REF] Iosif | Abstraction refinement and antichains for trace inclusion of infinite state systems[END_REF], by allowing monitor (right-hand side) automata to have local variables, that are not visible in the language.

Another application is checking safety (mutual exclusion, absence of deadlocks, etc.) and liveness (termination, lack of starvation, etc.) properties of parameterised concurrent programs, consisting of an unbounded number of replicated threads that communicate via a fixed set of global variables (locks, counters, etc.). The verification of parametric programs has been reduced to checking the emptiness of a (possibly infinite) sequence of first order alternating automata, called predicate automata [START_REF] Farzan | Proof spaces for unbounded parallelism[END_REF][START_REF] Farzan | Proving liveness of parameterized programs[END_REF], encoding the inclusion of the set of traces of a parametric concurrent program into increasingly general proof spaces, obtained by generalisation of counter-examples. The program and the proof spaces are first order alternating automata over the infinite alphabet of pairs consisting of program statements and thread identifiers.

Application on Timed Automata

The standard definition of a finite timed word is a sequence of pairs (a 1 , τ 1 ), (a 2 , τ 2 ), ..., (a n , τ n ) ∈ (Σ × R) * , where R is the set of real numbers, such that 0

≤ τ i < τ i+1 , for all i ∈ [1, n -1].
Intuitively, τ i is the moment in time where the input event a i occurs. Given a set C of clocks, the set Φ(C) of clock constraints is defined inductively as the set of formulae x ≤ c, x ≥ c, ¬δ, δ 1 ∧ δ 2 , where x ∈ C, c ∈ Q is a rational constant and δ, δ 1 , δ 2 ∈ Φ(X).

A timed automaton is a tuple T = (Σ, S, S 0 , F, C, E) where:

• Σ is a finite set of input events;

• S is a finite set of states;

• S 0 ⊆ S is the set of initial states;

• F ⊆ S is the set of final states;

• C is a finite set of clocks;

• E ⊆ S × Σ × S × 2 C × Φ(C)
is the set of transitions (s, a, s , λ, δ) from state s to state s with symbol a, where λ is the set of clocks to be reset and δ is a clock constraint.

A run of T over a timed word w = (a 1 , τ 1 ), (a 2 , τ 2 ), ..., (a n , τ n ) is a sequence (s 0 , γ 0 ), (s 1 , γ 1 ), ..., (s n , γ n ), where s i ∈ S, γ i : C → R are clocks valuations, for all i ∈ [1, n] and:

• s 0 ∈ S 0 and γ 0 (x) = 0 for all x ∈ C;

• for all i ∈ [1, n], there exists a transition (s i , a i , s i+1 , λ i , δ i ) ∈ E such that γ i +τ i+1 -τ i |= δ i , and for all x ∈ C, γ i+1 (x) = 0 if x ∈ λ i and γ i+1 (x) = γ i (x) + τ i+1 -τ i , otherwise.

Here τ 0 def = == = 0 and γ i + τ i+1 -τ i is the valuation mapping each x ∈ C to γ i (x) + τ i+1 -τ i . The run is accepting if and only if s n ∈ F , in which case T accepts w. As usual, we denote by L(T ) the set of finite words accepted by T . It is well-known that, in general, there is no timed automaton accepting the complement language (Σ × R) * \ L(T ) and, moreover, the language inclusion problem is undecidable [START_REF] Alur | A theory of timed automata[END_REF].

Given a timed automaton T = (Σ, S, S 0 , F, C, E), we define a first-order alternating automaton (FOADA) A T = (R, Σ, {t}, Q T , ι T , F T , ∆ T ), with a single input variable t, ranging over R, such that each timed word w = (a 1 , τ 1 ), (a 2 , τ 2 ), ..., (a n , τ n ) corresponds to a unique data word d(w) = (a 1 , v 1 ), (a 2 , v 2 ), ..., (a n , v n ) such that v i (t) = τ i for all i ∈ [1, n] and L(A T ) = {d(w) | w ∈ L(T )}. The only difficulty here is capturing the fact that all the clocks of T evolve at the same pace, which is easily done using a technique from [START_REF] Fribourg | A closed-form evaluation for extended timed automata[END_REF], which replaces each clock x i of T by a variable y i tracking the difference between the values of t and x i .

Formally, if C = {x 1 , x 2 , ..., x k } and S = {s 1 , s 2 , ..., s m }, we define Q T def = == = {q 1 , q 2 , ..., q m } where #(q i ) = k + 1 for all i ∈ [1, m], ι T def = == = si∈S0 q i (0, 0, ..., 0), F T def = == = {q i | s i ∈ F }
and, for each transition (s i , a, s j , λ, δ) ∈ E, ∆ T contains the rule:

q i (y 1 , y 2 , ..., y k , z) a(t) --→ t > z ∧ δ(z -y 1 , z -y 2 , ..., z -y k ) ∧ q j (y 1 , y 2 , ..., y k , t)
where y i stands for z if x i ∈ λ and for y i , otherwise. Moreover, nothing else is in ∆ T . We establish the following connection between a timed automaton and its corresponding first order alternating automaton. Proposition 5.1 Given a timed automaton T = (Σ, S, S 0 , F, C, E), the first-order alternating data automaton (FOADA) A T = (R, Σ, {t}, Q T , ι T , F T , ∆ T ) recognises the language L(A T ) = {d(w) | w ∈ L(T )}.

• q 0 ∈ S is the initial state;

• U = u 1 , u 2 , ..., u r is the initial assignment;

• ρ : S → [1, r] is the re-assignment partial function;

• µ ⊆ S × [1, r] × S is the transition relation;

• F ⊆ S is the set of final states.

A run of R over an input word a 1 , a 2 , ..., a n ∈ Σ * is a sequence (s 0 , V 0 ), (s 1 , V 1 ), ..., (s n , V n ) such that V 0 = U and, for all i ∈ [1, n], exactly one of the following holds:

• if there exists k ∈ [1, r] such that a i = (V i-1 ) k then V i = V i-1 and (s i-1 , k, s i ) ∈ µ; • otherwise a i ∈ [V i-1 ], ρ(s i-1 ) is defined, (V i ) ρ(si-1) = a i , for each k ∈ [1, r] \ {ρ(s i-1 )}, we have (V i ) k = (V i-1 ) k and (s i-1 , ρ(s i-1 ), s i ) ∈ µ.
Intuitively, if the input symbol is already stored in some register, the automaton moves to the next state if, moreover, the transition relation allows it, otherwise it copies the input to the register indicated by the re-assignment, erasing the previous value, and moves according to the transition relation.

The translation of register automata to first order alternating automata is quite natural, because registers can be encoded as arguments of predicate atoms. Formally, given a register automaton R = (S, s 0 , U, ρ, µ, F ) over a data domain D, such that S = {s 0 , s 1 , ..., s m }, we define the first-order alternating data automaton (FOADA) A R = (D, {α}, {x}, Q R , ι R , F R , ∆ R ) where:

• α ∈ Σ; • Q R def = == = {q 0 , q 1 , ..., q m }; • #(q i ) = r for all i ∈ [1, m]; • ι R def = == = q 0 (U ); • F R def = == = {q i | s i ∈ F };
• for each transition (s i , k, s j ) ∈ µ, ∆ R contains the rule:

q i (y 1 , y 2 , ..., y t ) α(x) ---→ y k = x∧q j (y 1 , y 2 , ..., y r )∨ r i=1
x = y i ∧q j (y 1 , y 2 , ..., y k-1 , x, y k+1 , y k+2 , ..., y r ) Moreover, nothing else is in ∆ R . The connection between register automata and first order alternating data automata (FOADA) is stated below. Proposition 5.2 Given a register automaton R = (S, s 0 , U, ρ, µ, F ) over a data domain D, the first-order alternating data automaton (FOADA) A R = (D, {α}, {x}, Q R , ι R , F R , ∆ R ) recognises the language:

L(A R ) = {(α, a 1 ), (α, a 2 ), ..., (α, a n ) | a 1 , a 2 , ..., a n ∈ L(R)}
Here is the proof of Proposition 5.2:

⊆ Let w = (α, a 1 ), (α, a 2 ), ..., (α, a n ) ∈ L(A R ). First, it is easy to show that each ex- ecution of A R , that starts in some cube c ∈ C([[ι R ]] µ )
, is a linear tree with labels q 0 (V 0 ), q 1 (V 0 ), ..., q n (V 0 ) such that V 0 = U . Second by induction on n ≥ 0, we prove that A R has a run as above over w only if R has a run (q 0 , V 0 ), (q 1 , V 1 ), ..., (q n , V n ) over a 1 , a 2 , ..., a n .

⊇ Let w = a 1 , a 2 , ..., a n ∈ L(R) and q 0 (V 0 ), q 1 (V 0 ), ..., q n (V 0 ) be a run of R over w, such that V 0 = U . By induction on n ≥ 0, we can build an execution of A R over (α, a 1 ), (α, a 2 ), ..., (α, a n ) that is a linear tree with labels q 0 (V 0 ), q 1 (V 1 ), ..., q n (V n ).

Consequently, the language inclusion problem "given register automata R 1 and R 2 , does L(R 1 ) ⊆ L(R 2 ) ?" is reduced in polynomial time to emptiness problem L(A R1 ) ∩ L(A R2 ) = ∅, for which Section 4.4 provides a semi-algorithm. Notice further that the encoding of register automata as first-order alternating data automata (FAODA) uses no transition quantifiers.

Application on Predicate Automata

The model of predicate automata [START_REF] Farzan | Proof spaces for unbounded parallelism[END_REF][START_REF] Farzan | Proving liveness of parameterized programs[END_REF] has emerged recently as a tool for checking safety and liveness properties of parameterised concurrent programs, in which there is an unbounded number of replicated threads that communicate via global variables. Predicate automata recognise finite sequences of actions that are pairs (σ, i) where σ is from a finite set Σ of program statements and i ∈ N ranges over an unbounded set of thread identifiers. To avoid clutter, we shall view a pair (σ, i) as a data symbol (σ, v) where v(x) = i, for a designated input variable x.

Since thread identifiers can only be compared for equality, the data theory of predicate automata is the first order theory of equality. Moreover, transition quantifiers are only needed for checking termination and, generally, liveness properties [START_REF] Farzan | Proving liveness of parameterized programs[END_REF].

However, the execution semantics of predicate automata differs from that of first order automata with respect to the following detail: initial configurations and successors of predicate automata are defined using the entire sets of models of the initial sentence and transition rules, not just the minimal ones, as in our case.

Formally, a run of a predicate automaton P = (Σ, {x}, Q, ι, F, ∆) over a word (a 1 , v 1 ), (a 2 , v 2 ), ..., (a n , v n ) is a sequence of interpretations I 0 , I 1 , ..., I n such that I 0 ∈ [[ι]] and for each i ∈ [1, n], each q ∈ Q and each tuple (d 1 , d 2 , ..., d #(q) ) ∈ I i-1 (q), we have

I i ∈ [[ψ]] v , for each rule q(y 1 , y 2 , ..., y #(q) ) ai(x) ---→ ψ ∈ ∆, where v = v i [y 1 ← d 1 , y 2 ← d 2 , ..., y #(q) ← d #(q)
]. The run is accepting if and only if I(q) = ∅ for all q ∈ Q \ F .

In fact, as shown next, this more simple execution semantics is equivalent, from the language point of view, with the semantics given by Definition 4.1 and Definition 4.2. We believe that the semantics of first-order alternating data automata based on minimal models is important for its relation to the textbook semantics of Boolean alternating automata [START_REF] Ashok | [END_REF]. Proposition 5.3 Given a predicate automaton P = (Σ, {x}, Q, ι, F, ∆), let A P be the first-order alternating automaton that has the same description as P. Then L(P) = L(A P ).

Here is the proof of Proposition 5.3:

⊆ Let w = (a 1 , v 1
), (a 2 , v 2 ), ..., (a n , v n ) ∈ L(P) be a word and I 0 , I 1 , ..., I n be an accepting execution of P over w. Let I

[i] j be the interpretation that associates each predicate q [i] the set I j (q), for i, j ∈ [1, n]. Then one builds, by induction on n ≥ 0, an execution T of A P such that

I T ⊆ n i=0 I [i]
i , where I T is the unique interpretation associated with T . Since I 0 , I 1 , ..., I n is accepting, we have I

[n] n (q [n]) = ∅, for all q ∈ Q \ F and hence I T (q [n] ) = ∅, for all q ∈ Q \ F and, consequently w ∈ L(A P ).

⊇ Let w = (a 1 , v 1 ), (a 2 , v 2 ), ..., (a n , v n ) ∈ L(A P ) be a word and T be an accepting execution of A P over w. We define the sequence of interpretations I 0 , I 1 , ..., I n as I i (q) = I T (q [i] ), for each i ∈ [1, n] and each q ∈ Q. By induction on n ≥ 0 one shows that I 0 , I 1 , ..., I n is an execution of P. Moreover, since T is accepting, we have I n (q) = I T (q [n] ) = ∅, for each q ∈ Q \ F , thus w ∈ L(P).

As before, this result enables using the semi-algorithm from Section 4.4 for checking emptiness of predicate automata. We point out that, although quantifier-free predicate automata with predicates of arity one are decidable for emptiness [START_REF] Farzan | Proof spaces for unbounded parallelism[END_REF], currently there is no method for checking emptiness of predicate automata with predicates of arity greater than one, other than the explicit enumeration of cubes. Moreover, no method for dealing with emptiness in the presence of transition quantifiers is known to exist.

Chapter 6

FOADA Checker

Besides the theoretical parts, we also have developed a tool -FOADA Checker [START_REF] Xu | Foada checker[END_REF], mainly used for checking inclusion between two automata or checking emptiness of an automaton. The tool is written in Java, via Java-SMT interface [START_REF]Java smt[END_REF] and using Z3 SMT solver [START_REF]Z3 smt solver[END_REF] for spuriousness, coverage queries and interpolant generation. The IMPACT semi-algorithm has been implemented in the tool to check the emptiness of an automaton. The supported input automata (can be parsed by our own parser written in ANTLR4 [START_REF] Parr | Antlr4[END_REF]) are: (i) predicate automata [START_REF] Farzan | Proof spaces for unbounded parallelism[END_REF][START_REF] Farzan | Proving liveness of parameterized programs[END_REF], (ii) alternating data automata and (iii) first-order alternating data automata.

In the first section, we show how to install the tool and use it to check inclusion of two automata or emptiness of an automaton. And then, we show the input format of first-order alternating data automata, which is the default data structure of the tool. After that, we introduce the input formats of alternating data automata and predicate automata, and explain how to transform them into the default data structure of the tool, hence first-order alternating data automata. In the end, we show some experimental results.

Brief User Guide

Installation

FOADA Checker can be downloaded via [START_REF] Xu | Foada checker[END_REF] and it only supports two operating systems: (i) Mac-OS and (ii) Linux. Once it has been downloaded, the installation can be simply done by typing following command in terminal under the downloaded folder:

1 sudo make install After the installation, we can verify whether all the solvers (SMT Interpol [49], Z3 SMT Solver [START_REF]Z3 smt solver[END_REF], MathSAT 5 [37] and Princess [START_REF] Ruemmer | Princess[END_REF]) are successfully integrated with JavaSMT, by simply typing following command:

Emptiness Checking

FOADA Checker is able to check whether the language of a given automaton is empty, by simply typing following command:

1 foada -e example . foada
We have implemented a version of IMPACT semi-algorithm [START_REF] Kenneth | Lazy abstraction with interpolants[END_REF] in the tool for emptiness checking. We have two cases:

• if the given automaton is empty, then the termination is not guaranteed; but if the tool terminates by reporting "empty" (Figure 6.2), then the given automaton is truly empty, hence the correctness of the result is guaranteed;

• if the given automaton is not empty, then the termination is guaranteed algorithmically1 , and the tool reports "not empty" together with a counter-example (Figure 6.3), which is a word from the language of the given automaton. The counter-example reported by the tool consists of different lines, where each line contains:

• an event symbol (for example, "a" in Figure 6.3)

• a valuation of variables (for example, "any any any any any -4357 4642 4260 6054 5464" in Figure 6.3)

Inclusion Checking

FOADA Checker can also check the language inclusion between two given automata, by simply typing following command:

1 foada -i example1 . foada example2 . foada

The inclusion checking implemented in the tool is also based on IMPACT semi-algorithm [START_REF] Kenneth | Lazy abstraction with interpolants[END_REF]. We have two cases:

• if the inclusion holds, then the termination is not guaranteed; but if the tool terminates by reporting "inclusion holds", then the inclusion truly holds, hence the correctness of the result is guaranteed;

• if the inclusion does not hold, then the termination is guaranteed algorithmically2 , and the tool reports "inclusion does not hold" together with a counter-example, which is a word from the language of the first given automaton that is not accepted by the second given automaton.

We have implemented Boolean operations of intersection and complement, so L(A) ⊆ L(B) is transformed into L(A) ∩ L(B) = ∅, which is an emptiness problem. The inclusion checking of FOADA Checker calls the emptiness checking function. Hence, the counter-example of inclusion checking reported by the tool is in the same format as the one for emptiness checking, consisting of different lines, where each line contains an event symbol and a valuation of variables.

Input Format -First-Order Alternating Data Automata (FOADA)

A FOADA input file describing a FOADA A = (D, Σ, X, Q, ι, F, ∆) contains:

• declaration of states (Q): (pred (q 0 q 1 ... q |Q| ))

• declaration of event symbols (Σ): (event (a 1 a 2 ... a |Σ| ))

• declaration of initial configuration (ι): (initial ι)

• declaration of final states (F ): (final (f 1 f 2 ... f k ))

• declaration of transition rules (∆) in the format:

(trans (q i ((d where:

q i ∈ Q; d 1 , d 2 , ..., d #(qi) are the arguments of q i ; -Sort m is the sort of m; a j ∈ Σ; x 1 , x 2 , ..., x |X| ∈ X; ψ ∈ FORM + (Q, X ∪ {d 1 , d 2 , ..., d #(qi) }) is a positive formula in SMT2 format [START_REF]Smt2 format[END_REF],

where X ∩ {d 1 , d 2 , ..., d #(qi) } = ∅.

Example 6.1 The source code below describes a FOADA A = (D, Σ, X, Q, ι, F, ∆) where:

• D = Z, Σ = {a}, X = {x}, Q = {p, q}, ι = p(0), F = {q},

• and there are two transitions:

p(d) a(x)
---→ q(x) ∧ x ≥ 0 q(d)

a(x)
---→ q(x) ∧ d ≥ 0

( pred ( p q ) ) ( event ( a ) ) ( initial ( p 0) ) ( final ( q ) ) ( trans ( p (( d Int ) ) ) ( a (( x Int ) ) ) ( and ( q x ) ( >= x 0) ) ) ( trans ( q (( d Int ) ) ) ( a (( x Int ) ) ) ( and ( q x ) ( >= d 0) ) )

6.3 Input Format -Alternating Data Automata (ADA)

An ADA input file describing an ADA A = (D, Σ, X, Q, ι, F, ∆) contains:

• declaration of states (Q): STATES q 0 q 1 ... a i1 , a i2 , ..., a i |∆| ∈ Σ;

q j1 , q j2 , ..., q j |∆| ∈ Q;

ψ k1 , ψ k2 , ..., ψ k |∆| ∈ FORM + (Q, X ∪ X) are formulae in SMT2 format [START_REF]Smt2 format[END_REF], where X denotes {x | x ∈ X}.

Example 6.2 The source code below describes an ADA A = (D, Σ, X, Q, ι, F, ∆) where:

• D = Z, Σ = {a}, X = {x, y}, Q = {q 0 , q 1 , q 2 }, ι = q 0 ∧ q 2 , F = {q 1 },

• and there are three transitions:

∆(q 0 , a) ≡ q 1 ∧ x 1 = 0 ∧ y 1 = 0 ∆(q 1 , a) ≡ q 1 ∧ x 1 = x 0 + 1 ∧ y 1 = y 0 + 1 ∆(q 2 , a) ≡ q 2 ∨ ¬(x 1 = y 1 ) Once an ADA has been read by FOADA Checker as the input, it is stored as a FOADA that is equivalent to the original ADA, hence recognising the same language. Example 6.3 The ADA A in Example 6.2 is transformed into a FOADA A = (D , Σ , X , Q , ι , F , ∆ ) that is equivalent to A once it has been read as the input, where:

STATES

• D = D = Z, Σ = Σ = {a}, X = X = {x, y}, Q = Q = {q 0 , q 1 , q 2 }, F = F = {q 1 },

• ι = q 0 (0, 0) ∧ q 2 (0, 0),

• and there are three transitions in ∆ :

q 0 (x 0 , y 0 ) a(x1,y1) -----→ q 1 (x 1 , y 1 ) ∧ x 1 = 0 ∧ y 1 = 0 q 1 (x 0 , y 0 ) a(x1,y1) -----→ q 1 (x 1 , y 1 ) ∧ x 1 = x 0 + 1 ∧ y 1 = y 0 + 1 q 2 (x 0 , y 0 ) a(x1,y1) -----→ q 2 (x 1 , y 1 ) ∨ ¬(x 1 = y 1 )

Input Format -Predicate Automata (PA)

FOADA Checker supports predicate automata [START_REF] Farzan | Proof spaces for unbounded parallelism[END_REF][START_REF] Farzan | Proving liveness of parameterized programs[END_REF] as inputs. Once a PA has been read by the tool as the input, it is stored as a FOADA that is equivalent to the original PA, hence recognising the same language.

Example 6.4 The source code below is a predicate automaton from an example set [START_REF] Kincaid | Predicate automata[END_REF]. It is an example for the tool "Duet" [START_REF] Kincaid | Duet[END_REF], which is a static analysis tool designed for analysing concurrent programs. ---→ true

Experimental Results

We have done experiments with several sources:

• predicate automata models [START_REF] Farzan | Proof spaces for unbounded parallelism[END_REF][START_REF] Farzan | Proving liveness of parameterized programs[END_REF][START_REF] Kincaid | Predicate automata[END_REF]:

incdec.pa The advantage of using FOADA Checker over the INCLUDER [START_REF] Iosif | Includer[END_REF] tool from [START_REF] Iosif | Abstraction refinement and antichains for trace inclusion of infinite state systems[END_REF] is the possibility of having infinite alphabet automata with hidden (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.

Chapter 7

Conclusions

Summary of Contributions

In order to face the two challenges mentioned in the beginning of this thesis: (i) non-determinism and (ii) infinite alphabets, we propose two models of alternating automata over infinite alphabets: (i) alternating data automata (ADA) and (ii) first-order alternating data automata (FOADA). They both recognise the data words over infinite alphabets consisting of pairs (a, v) where a is an input event from a finite set and v is a valuation of a finite set of variables that range over a possibly infinite data domain.

In ADA model, the control states are Booleans and the transition rules are specified by a set of formulae in a combined first-order theory of states (Booleans) and data that relate past values of variables with current values of variables. But a restriction of the ADA model is that, there is not hidden variable, hence all the data values taken by the variables are visible in the input. But in FOADA model, the arguments of a predicate atom track the values of the internal variables associated with the state, and these values are invisible in the input sequence, which overcomes the restriction of the ADA model. With these two alternating models, Boolean operations of union, intersection and complement can be done in linear time, thus matching the complexity of performing these operations in the finite-alphabet case.

However, the price to be paid here is that the emptiness checking becomes undecidable. For this reason, we provide two efficient semi-algorithms for emptiness checking: (i) lazy predicate abstraction [START_REF] Henzinger | Lazy abstraction[END_REF] and (ii) IMPACT method [START_REF] Kenneth | Lazy abstraction with interpolants[END_REF]. These semi-algorithms are proven to terminate by returning a word from the language of the given automaton if one exists; but if the language of the given automaton is empty, then the termination is not guaranteed.

The main application of these two models is checking inclusions between various classes of automata extended with variables ranging over infinite domains that recognise languages over infinite alphabets. The most widely known such classes are (i) timed automata [START_REF] Alur | A theory of timed automata[END_REF] and (ii) finite-memory automata [START_REF] Kaminski | Finite-memory automata[END_REF]. In both cases, complementation is not possible inside the class and inclusion is undecidable. Our contribution here is providing a systematic semi-algorithm for these decision problems. In addition, we can extend generic register automata [START_REF] Iosif | Abstraction refinement and antichains for trace inclusion of infinite state systems[END_REF] inclusion checking framework by allowing monitor (right-hand side) automata to have local (hidden) variables that are not visible in the language.

Another application is checking safety (mutual exclusion, absence of deadlocks, etc.) and liveness (termination, lack of starvation, etc.) properties of parameterised concurrent programs, consisting of an unbounded number of replicated threads that communicate via a fixed set of global variables (locks, counters, etc.). The verification of parametric programs has been reduced to checking the emptiness of a possibly infinite sequence of first-order alternating data automata, called predicate automata [START_REF] Farzan | Proof spaces for unbounded parallelism[END_REF][START_REF] Farzan | Proving liveness of parameterized programs[END_REF], encoding the inclusion of the set of traces of a parametric concurrent program into increasingly general proof spaces, obtained by generalisation of counterexamples. The program and the proof spaces are first-order alternating data automata over the infinite alphabet of pairs consisting of program statements and thread identifiers.

Besides the theoretical parts, we also have developed a tool -FOADA Checker [START_REF] Xu | Foada checker[END_REF], mainly used for checking inclusion between two automata or checking emptiness of an automaton. FOADA Checker is written in Java, via Java-SMT interface [START_REF]Java smt[END_REF] and using Z3 SMT solver [START_REF]Z3 smt solver[END_REF] for spuriousness, coverage queries and interpolant generation. The IMPACT semi-algorithm [START_REF] Kenneth | Lazy abstraction with interpolants[END_REF] has been implemented in the tool to check the emptiness of an automaton. The supported input automata are: (i) predicate automata [START_REF] Farzan | Proof spaces for unbounded parallelism[END_REF][START_REF] Farzan | Proving liveness of parameterized programs[END_REF], (ii) alternating data automata and (iii) first-order alternating data automata. These input automata can be parsed by our own parser written in ANTLR4 [START_REF] Parr | Antlr4[END_REF], and they are all stored as FOADA once they have been parsed by the tool.

The advantage of using FOADA Checker over the INCLUDER [START_REF] Iosif | Includer[END_REF] tool from [START_REF] Iosif | Abstraction refinement and antichains for trace inclusion of infinite state systems[END_REF] is the possibility of having infinite alphabet automata with hidden (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.

Future Work

For the moment, the examples of alternating data automata (ADA) and first-order alternating data automata (FOADA) for timed automata (TA) inclusion problems, array logic entailments, hardware circuit verification problems and parametric verification problems are produced manually from some existing classical examples written in C/C++, such as abp.ada, train.ada, rr-crossing.foada, array rotation.ada, train-simple1.foada, etc. (see Section 6.5 ). This excludes the possibility of using huge classical examples as the inputs of our tool (FOADA Checker) since the manual transformation requires too much work and some errors might occur during the manual transformation. We are thinking of studying those C/C++ examples, and extending the parser in our tool so that the tool can directly parse those examples and generate corresponding ADA or FOADA.

We are also going to apply our models and tool to more kinds of verification problems, such as parametric system verification [START_REF] Bozga | Structural invariants for parametric verification of systems with almost linear architectures[END_REF], which asks whether a system composed of n replicated processes is safe, for all n ≥ 2. By safety we mean that every execution of the system stays clear of a set of global error configurations, such as deadlocks or mutual exclusion violations. Even if we assume each process to be finite-state and every interaction to be a synchronization of actions without data exchange, the problem remains challenging because we want a general proof of safety, that works for any number of processes. In general, parametric verification is undecidable if unbounded data is exchanged [START_REF] Apt | Limits for automatic verification of finite-state concurrent systems[END_REF], while various restrictions of communication (rendez-vous) and architecture (ring, clique) define decidable sub-problems [START_REF] Aminof | Parameterized model checking of rendezvous systems[END_REF][START_REF] Clarke | Reasoning about networks with many identical finite-state processes[END_REF][START_REF] Emerson | Reasoning about rings[END_REF][START_REF] German | Reasoning about systems with many processes[END_REF]. Seminal works consider rendez-vous communication, allowing a fixed number of participants [START_REF] Clarke | Reasoning about networks with many identical finite-state processes[END_REF][START_REF] Emerson | Reasoning about rings[END_REF][START_REF] German | Reasoning about systems with many processes[END_REF], placed in a ring [START_REF] Clarke | Reasoning about networks with many identical finite-state processes[END_REF][START_REF] Emerson | Reasoning about rings[END_REF] or a clique [START_REF] German | Reasoning about systems with many processes[END_REF]. Recently, MSO-definable graphs (with bounded tree and clique-width) and point-to-point rendez-vous communication were considered in [START_REF] Aminof | Parameterized model checking of rendezvous systems[END_REF].

Figure 1 . 1 :

 11 Figure 1.1: An FSA for a Chemical Production System

Figure 1 . 2 :

 12 Figure 1.2: An FSA for a Safe Production Specification of the System in Example 1.1

Figure 1 . 3 :

 13 Figure 1.3: A Technique to Solve the Language Inclusion Problem

Figure 1 . 4

 14 Figure 1.4: From System Verification to Emptiness Problem

Figure 1 . 5 :

 15 Figure 1.5: Complement an NFA in a Wrong Way

Example 1 . 4 Figure 1 . 6 :

 1416 Figure 1.6: A 3-State NFA to an 8-State DFA by Subset Construction

Figure 1 . 7 : 5 Example 1 . 6 repair 2 ≤Figure 1 . 8 :

 17516218 Figure 1.7: Arrays and Specification in Example 1.5

Figure 1 . 9 :

 19 Figure 1.9: An Alternating Finite Automaton

Figure 1 .

 1 Figure 1.10: A Non-Complementable Timed Automaton

Figure 1 .

 1 Figure 1.13: A Data Automaton

Figure 1 . 14 :

 114 Figure 1.14: An Instance of the Trace Inclusion Problem

Figure 1 . 15 :

 115 Figure 1.15: An Alternating Data Automata

•

  |S| : Given a set S, |S| denotes the cardinality of S; • [a, b] : Given two integers a and b such that a ≤ b, [a, b] denotes the integer set {i ∈ Z | a ≤ i ≤ b}; • A B : Given two sets A and B, A B denotes the set of all functions f : A → B.

Figure 2 . 2 :

 22 Figure 2.2: Determinisation of NFA in Example 2.1 in Page 31

  where f is the characteristic vector of F 2.5 Data Automata (DA) 2.5.1 Definition of DA Data Automata (DA) are extensions of NFA with variables ranging over an infinite data domain D, equipped with a first-order theory T(D).

Figure 3 . 1 :

 31 Figure 3.1: An Alternating Data Automaton

  r, Λ, ) be an ART 2: let Π be a set 3: let WorkList be a list 4: N := ∅ 5: E := ∅ 6: Λ := {(r, ι)} 7: := ∅ 8: add {⊥} into Π 9: add r into WorkList 10: while WorkList = ∅ do 11: dequeue n from WorkList 12:

Figure 3 . 2 : 1 Example 3 . 3

 32133 Figure 3.2: Proving Emptiness of the ADA in Figure 3.1 by Semi-Algorithm 1

9 :

 9 r, Λ, R, T, ) be an ART 2: let WorkList be a list3: N := ∅ 4: E := ∅ 5: Λ := {(r, ι)} 6: R := FV Boolean (ι[Q 0 /Q]) 7: T := ∅ add r intoWorkList 10: while WorkList = ∅ do 11: dequeue n from WorkList 12: N := N ∪ {n} 13:

else 18 :

 18 let ( , I 0 , I 1 , ..., I k , ⊥) be an interpolant for Θ(a 1 , a 2 , ..., a k )

33 :

 33 let e = (n, a, s) be a new edge 34:E := E ∪ {e} 35: Λ := Λ ∪ {(s, )} 36: T := T ∪ {(e, θ k )} 37: R := R ∪ {(s, q∈R(n)FV Boolean (∆(q, a)))} end while 42: return true Function 1 CLOSE Input: a node x Output:

Figure 3 . 3 :

 33 Figure 3.3: Proving Emptiness of the ADA in Figure 3.1 by Semi-Algorithm 2

For a formula φ

  and a valuation v, we define [[φ]] v def = == = {I | I, v |= φ} and drop the v subscript for sentences.A sentence φ is satisfiable if [[φ]] = ∅ and φ is unsatisfiable if [[φ]] = ∅. An element of [[φ]] is called a model of φ. A formula φ is valid if I, v |= φfor every interpretation I and every valuation v. For two formulae φ and ψ, we write φ |= ψ for [[φ]] ⊆ [[ψ]], in which case we say that φ entails ψ. Interpretations are partially ordered by the point-wise subset order, defined as I 1 ⊆ I 2 if and only if p I1 ⊆ p I2 for each predicate p ∈ PRED. Given a set S of interpretations, a minimal element I ∈ S is an interpretation such that for no other interpretation I ∈ S \ {I} do we have I ⊆ I. For a formula φ and a valuation v, we denote by [[φ]] µ v and [[φ]] µ the set of minimal interpretations from [[φ]] v and [[φ]], respectively.

  For a set S of interpretations, we define C(S) def = == = {C(I) | I ∈ S}.

Definition 4 . 2

 42 And an execution T over w, starting with c, is accepting if and only if:

Lemma 4 . 3

 43 For any input event sequence α = a 1 , a 2 , ..., a n and each valuation v : X [≤n] → D, the following hold:• for all interpretations I, if I, v |= Υ(α) then I, v |= Υ(α);

Example 4 . 2

 42 The result of the elimination of predicate atoms from the acceptance formula in Example 4.1 is shown below:

Lemma 4 . 4

 44 For any input event sequence α = a 1 , a 2 , ..., a n and each valuation v : X [≤n] → D, there exists an interpretation I such that I, v |= Υ(α) if and only if v |= Υ(α).

  then

Theorem 4 . 2

 42 If an automaton A has a non-empty safe closed unfolding then L(A) = ∅.

  strictly] monotonic if and only if for each n < m we have ξ(n) ≤ ξ(m) [ξ(n) < ξ(m)] and (ii) finite-range if and only if for each n ∈ N the set {m | ξ(m) = n} is finite. If ξ is finite-range, we denote by ξ -1 max (n) ∈ N the maximal value m such that ξ(m) = n. The lemma below gives the proof of correctness for the construction of non-local GLI.

  (y) → ψ [k+1] |= φ k for all k ∈ [1, n]. Consequently, we obtain: ι [0] |= Φ 0 |= I 0 , by Theorem 4.3;

Figure 6 . 1 :

 61 Figure 6.1: Screenshot of a Successful Installation on Mac-OS

Figure 6 . 2 :Figure 6 . 3 :

 6263 Figure 6.2: Screenshot of an Empty Automaton

•

  q |Q| • declaration of initial configuration (ι): INITIAL ι declaration of final states (F ): FINAL f 1 f 2 ... f k • declaration of event symbols (Σ): SYMBOLS a 1 a 2 ... a |Σ| • declaration of variables (X): VARIABLES x 1 x 2 ... x |X| • declaration of transition rules (

  (= x1 (+ x0 1) ) (= y1 (+ y0 1) ) ) # a q2 ( or q2 ( not (= x1 y1 ) ) ) #

  start : { a }() /\ { b }() . final : none . { a }() --( a1 : i ) -> { c }( i ) . { b }() --( a1 : i ) -> { d }( i ) . { c }( i ) --( a2 : j ) -> { e }( i ) . { d }( i ) --( a2 : j ) -> { e }( j ) . { e }( i ) --( a3 : j ) -> true .Example 6.5 The PA in the source code above is stored as a FOADA A = (D, Σ, X, Q, ι, F, ∆) accepting the same language once it has been read by FOADA Checker as the input, where:• D = Z, Σ = {a1, a2, a3}, X = {x}, Q = {{a}, {b}, {c}, {d}, {e}}, ι = {a}()∧{b}(), F = ∅,• and there are five transitions in ∆:

-

  localdec.pa ticket.pa count thread0.pa count thread1.pa -local0.pa -local1.pa • timed automata inclusion problems: abp.ada train.ada rr-crossing.foada • array logic entailments: array rotation.ada array simple.ada array shift.ada • hardware circuit verification [34]: -hw1.ada -hw2.ada • parametric verification problems checking inclusions of the form N i=1 L(A i ) ⊆ L(B): train-simple1.foada train-simple2.foada train-simple3.foada fischer-mutex2.foada fischer-mutex3.foada The experiments were carried out on a Mac-OS x64 -1.3 GHz Intel Core i5 -8 GB 1867 MHz LPDDR3 machine, and the experimental results are reported in

  t 1 , t 2 , ..., t #(f ) are terms;

1

  Sort d1 ) (d 2 Sort d2 ) ... (d #(qi) Sort d #(q i ) ))) (a j ((x 1 Sort x1 ) (x 2 Sort x2 ) ... (x |X| Sort x |X| ))) (ψ) )

Table 6 .

 6 1.

	Example	|A| (bytes)	L(A) = ∅?	Nodes Expanded Nodes Visited Time (ms)
	incdec.pa	499	no	21	17	779
	localdec.pa	678	no	49	35
	ticket.pa	4250	no	229	91
	count thread0.pa	9767	no	154	128
	count thread1.pa	10925	no	766	692	76771
	local0.pa	10595	no	73	27
	local1.pa	11385	no	1135	858	101042
	array rotation.ada	1834	yes	9	8
	array simple.ada	3440	yes	11	10
	array shift.ada	874	yes	6	5	413
	abp.ada	6909	no	52	47
	train.ada	1823	yes	68	67
	hw1.ada	322	Solver Error	/	/	/
	hw2.ada	674	yes	20	22
	rr-crossing.foada	1780	yes	67	67
	train-simple1.foada	5421	yes	43	44
	train-simple2.foada	10177	yes	111	113
	train-simple3.foada	15961	yes	196	200	15041
	fischer-mutex2.foada	3000	yes	23	23	808
	fischer-mutex3.foada	4452	yes	33	33

Table 6 .

 6

1: Experiments with First-Order Alternating Data Automata

Some input word can block the computation, but the computation is still unique for DFA.

Theoretically, any DFA is also a NFA. But here in this chapter, we use "NFA" in a narrower sense, referring to those NFA who are not DFA.

It becomes decidable if restricted to having at most one clock.

We omit specifying the signature of a function when it is not necessary.

We omit specifying the sort of a constant when it is not necessary.

We omit specifying the sort of a variable if it is not necessary.

We omit specifying the sort of a term when it is not necessary.

The proof is in[START_REF] Iosif | Abstraction refinement and antichains for trace inclusion of infinite state systems[END_REF].

The theory T(S, I) is the set of valid formulae written in the signature S, with the interpretation I. A decision procedure for T(S, I) is an algorithm that takes a formula φ in the signature S and returns yes if and only if φ ∈ T(S, I).

foada -c

Any error of the solver might break the program. But besides that, the termination is guaranteed.

Any error of the solver might break the program. But besides that, the termination is guaranteed.

Acknowledgements

I must start by thanking my supervisor, Radu Iosif, whose patience, guidance, encouragement, support and trust were key to achieving this thesis. I got precious experiences from both theoretical and practical aspects. I am also indebted to my co-supervisor, Susanne Graf, who spent precious time in helping me.

Besides my supervisors, I would like to thank the rest of my thesis committee: Mr. VOJNAR Thomas, Mr. PODELSKI Andreas, Mr. VEANES Margus and Mr. BOUAJJANI Ahmed, for their encouragement, insightful comments and hard questions.

Last but not the least, I would like to thank my family, especially my dear wife, Taoran YAN, for supporting me.

13:

let λ(n) = a 1 , a 2 , ..., a k be the label of the path from r to n 14:

if ACC A (λ(n)) is satisfiable then 16:

get model (β, v 1 , v 2 , ..., v k ) of ACC # A (λ(n))

17:

return w = (a 1 , v 1 ), (a 2 , v 2 ), ..., (a k , v k ) v := LeastInfeasibleSuffix(λ(n), T )

Π := Π ∪ {I 0 , I 1 , ..., I k } where ( , I 0 , I 1 , ..., I k , ⊥) is an interpolant for Ψ(v)

22:

let S = (N , E , p, Λ , ) be the sub-tree of T rooted at p 23:

for (m, q) ∈ such that q ∈ N do 24:

remove m from N and enqueue m into WorkList for a ∈ Σ do 31:

if exist m ∈ N such that φ |= Λ(m) then 33:

let s be a fresh node

36:

Λ := Λ ∪ {(s, φ)} for (m, r) ∈ do end for 51:

end if 52: end while 53: return true Semi-Algorithm 1 uses a work-list iteration to build an ART. We keep newly expanded nodes of T in a queue WorkList, thus implementing a breadth-first exploration strategy, which guarantees that the shortest counter-examples are explored first. When the search encounters a counter-example candidate u, it is checked for spuriousness. If the counter-example is feasible, if Υ(α)(X [1] , X [2] , ..., X [k] ) is satisfiable then

get model v of Υ(α)(X [1] , X [2] , ..., X [k] )

return w = (a 1 , v(X [1] )), (a 2 , v(X [2] )), ..., (a k , v(X [k] ))

for m ∈ Uncover such that m is a leaf of U do if n is not covered then ⊆ Let w = (a 1 , v 1 ), (a 2 , v 2 ), ..., (a n , v n ) ∈ L(A T ) be a data word. We show the existence of a timed word (a 1 , τ 1 ), (a 2 , τ 2 ), ..., (a n , τ n ) ∈ L(T ) such that v i (t) = τ i , for all i ∈ [1, n], by induction on n ≥ 0. In fact we shall prove the following stronger statements:

(1) each execution of A T over w starting with a cube c ∈ C([[ι T ]] µ ) is a linear tree, in which each node has at most one child;

(2) for each execution q i0 (d 0 1 , d 0 2 , ..., d 0 k , τ 0 ), q i1 (d 1 1 , d 1 2 , ..., d 1 k , τ 1 ), ..., q in (d n 1 , d n 2 , ..., d n k , τ n ) of A T , T has an execution (s i0 , γ 0 ), (s i1 , γ 1 ), ..., (s in , γ n ) over the timed word (a 1 , τ 1 ), (a 2 , τ 2 ), ..., (a n , τ n ), such that, for all i ∈ [1, n] and all l ∈ [1, k], we have

The first point above is by inspection of ι T = si∈S0 q i (0, 0, ..., 0) and of the rules from ∆ T . Indeed, each minimal model of ι T corresponds to a cube q(0, ..., 0) and each rule has exactly one predicate atom on its right-hand side, thus each node of the execution will have at most one successor. The second point is by induction on n ≥ 0.

⊇ Let w = (a 1 , τ 1 ), (a 2 , τ 2 ), ..., (a n , τ n ) ∈ L(T ) be a time word. By induction on n ≥ 0, we show that for each run (s i0 , γ 0 ), (s i1 , γ 1 ), ..., (s in , γ n ) of T over w, A T has a linear execution

An easy consequence is that the timed language inclusion problem "given timed automata T 1 and T 2 , does L(T 1 ) ⊆ L(T 2 ) ?" is reduced in polynomial time to the emptiness problem L(A T1 ) ∩ L(A T2 ) = ∅, for which Section 4.4 provides a semi-algorithm. Observe, moreover, that no transition quantifiers are needed to encode timed automata as first-order alternating data automata (FOADA).

Application on Register Automata

Finite-memory automata, most commonly referred to as register automata [START_REF] Kaminski | Finite-memory automata[END_REF] are among the first attempts at lifting the finite alphabet restriction of classical automata. In a nutshell, a register automaton is a finite-state automaton (FSA) equipped with a finite set of registers x 1 , x 2 , ..., x r able to copy input values and compare them with subsequent input. Consequently, basic results from classical automata theory, such as the pumping lemma or the closure under complement do not hold in this model and, moreover, inclusion of languages recognised by register automata is undecidable [START_REF] Neven | Finite state machines for strings over infinite alphabets[END_REF].

Let Σ be an infinite alphabet, # be a symbol not in Σ and r > 0 be an integer constant, denoting the number of registers. An assignment is a word V = v 1 , v 2 , ..., v r such that if v i = v j and i = j then v i = #, for all i, j ∈ [1, r]. We write [V ] for the set {v i | i ∈ [1, r]} of values in the assignment V . A finite-memory (register) automaton is a tuple R = (S, q 0 , U, ρ, µ, F ) where:

• S is a finite set of states;