Lukáš Holík
email: holik@fit.vut.cz

Iosif ¨adam Rogalewicz

Tomáš Vojnar
email: vojnar@fit.vut.cz

R Iosif
email: radu.iosif@univ-grenoble-alpes.fr

A Rogalewicz

Abstraction Refinement and Antichains for Trace Inclusion of Infinite State Systems

Keywords:

A generic register automaton is a finite automaton equipped with variables (which may be viewed as counters or, more generally, registers) ranging over infinite data domains. A trace of a generic register automaton is an alternating sequence of alphabet symbols and values taken by the variables during an execution of the automaton. The problem addressed in this paper is the inclusion between the sets of traces (data languages) recognized by such automata. Since the problem is undecidable in general, we give a semi-algorithm based on a combination of abstraction refinement and antichains, which is proved to be sound and complete, but whose termination is not guaranteed. Moreover, we further enhance the proposed algorithm by exploiting a concept of data simulations, i.e., simulation relations aware of the data associated with the words. We have implemented our technique in a prototype tool and show promising results on multiple non-trivial examples.

Introduction

Many results in formal languages and automata theory rely on the assumption that the alphabet over which languages are defined is finite. The finite alphabet hypothesis is crucial for the existence of determinization, complementation and decidability of language inclusion problems for the language acceptor class under consideration. However, this assumption prevents the use of automata as models of real-time systems or infinite-state programs. In general, traditional attempts to generalize classical finite-state automata to infinite alphabets, such as timed automata [START_REF] Alur | A theory of timed automata[END_REF] or finite-memory register automata [START_REF] Kaminski | Finite-memory automata[END_REF] face the complement closure problem: there exists automata for which the complement language cannot be recognized by automata in the same class. This prevents encoding language inclusion problems LpAq Ď LpBq as the emptiness of the language LpAq X LpBq, because the complement LpBq of the language LpBq cannot be computed within the class of A and B. Moreover, the language inclusion problem is proved to be undecidable, in general, for timed [START_REF] Alur | A theory of timed automata[END_REF] and finite-memory [START_REF] Kaminski | Finite-memory automata[END_REF] automata, unless severe restrictions are applied.

In this paper, we consider a generalization of finite-state automata, by adding finitely many variables that range over an infinite data domain and whose values are part of the language of the automaton. We address the trace inclusion problem between (i) a network of generic register automata 1 A " xA 1 , . . . , A N y that communicate via a set of input events Σ A and a set of shared variables x A , ranging over an infinite data domain, and (ii) a generic register automaton B whose set of variables x B is a subset of x A and whose set of input events is Σ B . Here, by a trace, we understand an alternating sequence of valuations of the variables from the set x B and input events from the set Σ A X Σ B , starting and ending with a valuation.

Typically, the automata network A models the implementation of a concurrent system and B is a specification of the set of good behaviors of the system. Then, a positive answer to the above inclusion problem means that the behavior of the implementation conforms to the specification, which is a natural verification problem.

Consider, for instance, the network xA 1 , . . . , A N y of generic register automata equipped with the integer-valued variables x and v shown in Fig. 1-left. The automata synchronize on the init symbol and interleave their a 1,...,N actions. Each automaton A i increases the shared variable x and writes its identifier i into the shared variable v as long as the value of x is in the interval rpi ´1q∆, i∆ ´1s, and it is inactive outside this interval, where ∆ ě 1 is an unbounded parameter of the network. A possible specification for this network might require that each firing sequence is of the form init a 1,...,N a 2 a 2,...,N . . . a i a i for some 1 ď i ď N, and that v is increased only on the first occurrence of the events a 2 , . . . , a i , in this order. This condition is encoded by the automaton B (Fig. 1-right). Observe that only the v variable is shared between the network xA 1 , . . . , A N y and the specification automaton B-we say that v is observable in this case. An example of a trace, for ∆ " 2 and N ě 3, is: pv " 0q init pv " 1q a 1 pv " 1q a 1 pv " 1q a 2 pv " 2q a 2 pv " 2q a 3 pv " 3q. Our problem is to check that this, and all other traces of the network, are included in the language of the specification automaton, called the observer. The trace inclusion problem has multiple applications, e.g.:

-Decision procedures for logics describing array structures within imperative programs [START_REF] Habermehl | What else is decidable about integer arrays? In[END_REF][START_REF] Habermehl | A logic of singly indexed arrays[END_REF] that use a translation of array formulae to integer counter automata which encode the set of array models of a formula. The expressiveness of such logics is currently limited by the undecidability of the emptiness (reachability) problem for counter automata. If we give up on decidability, we can reduce an entailment between two array

p 0 q i 0 p 1 v 1 " 1 init a 2 a 1...N v 1 " v `1 a 2...N a N a N v 1 " v `1 p N . . . q i 1 x 1 " 0 init v 1 " 1 v 1 " v p 2 v 1 " v v 1 " v a i ą ą A i"1,...,N B pi ´1q∆ ď x ă i∆ ∆ 1 " ∆ v 1 " i x 1 " x `1
Fig. 1 An instance of the trace inclusion problem.

formulae to the trace inclusion of two integer counter automata, and use the method presented in this paper as a semi-decision procedure. To corroborate this claim, we have applied our trace inclusion method to several verification conditions for programs with unbounded arrays of integers [START_REF] Bozga | Automatic verification of integer array programs[END_REF].

-Timed automata and regular specifications of timed languages [START_REF] Alur | A theory of timed automata[END_REF] can be both represented by finite automata extended with real-valued variables [START_REF] Fribourg | A closed-form evaluation for extended timed automata[END_REF]. The verification problem boils down to the trace inclusion of two real-valued generic register automata.

In this context, our method has been tested on several timed verification problems, including communication protocols and boolean circuits [32].

When developing a method for checking the inclusion between trace languages of automata extended with variables ranging over infinite data domains, the first problem is the lack of determinization and/or complementation results. In fact, certain classes of infinite state systems, such as finite-memory (register) [START_REF] Kaminski | Finite-memory automata[END_REF] or timed automata [START_REF] Alur | A theory of timed automata[END_REF], cannot be determinized and are provably not closed under complement. This is the case due to the fact that the values of the variables (registers, clocks) in such models of automata are not observable in the recognized language, that is determined by a series of internal computations.

However, if we allow the values of all variables of a generic register automaton to be part of its trace language, we obtain a determinization result, which generalizes the classical subset construction by taking into account the data valuations. Building on this first result, we define the complement of a trace language as an effectively computable generic register automaton. Thus, we can reduce the trace inclusion problem to the emptiness of a generic register product automaton LpA ˆBq " H, just as in the finite alphabet case. However, the reduction of the trace inclusion to the emptiness problem crucially relies on the fact that the variables x B of the right-hand side generic register automaton B (the one being determinized) are also controlled by the left-hand side automaton A, in other words, that B has no hidden variables. It is still an open problem whether and in which circumstances this reduction can be achieved in the presence of hidden variables.

The language emptiness problem for generic register automata is, in general, undecidable [START_REF] Minsky | Computation: Finite and Infinite Machines[END_REF]. Nevertheless, several semi-algorithms and tools for this problem, better known as the reachability problem, have been developed [START_REF] Bardin | Fast: Fast acceleration of symbolic transition systems[END_REF][START_REF] Henzinger | Software Verification with Blast[END_REF][START_REF] Mcmillan | Lazy abstraction with interpolants[END_REF][START_REF] Grebenshchikov | Synthesizing software verifiers from proof rules[END_REF]. Among those, the technique of lazy predicate abstraction [START_REF] Henzinger | Software Verification with Blast[END_REF] combined with counterexample-driven refinement using interpolants [START_REF] Mcmillan | Lazy abstraction with interpolants[END_REF] has been shown to be particularly successful in proving emptiness of infinite-state systems. Moreover, this technique shares similar aspects with antichain-based algorithms for language inclusion in the case of a finite alphabet [33,[START_REF] Abdulla | When simulation meets antichains[END_REF]. An important similarity is that both techniques use partial orders over the set of symbolic states, to prune the search space, by storing only incomparable such states. In other words, the successors of a covered state (in the sense of the partial order) are never explored, because any counterexample that could potentially arise from that state, can also be discovered by expanding the state that covers it.

Even if the trace inclusion problem can be reduced, under some conditions, to the emptiness of a counter automaton for which practical semi-algorithms exist, building the entire product counter automaton before checking its emptiness is usually not feasible. This is because the size of the product automaton is exponentially larger than the sum of the sizes of A and B, even when the trace alphabet is finite. Having, moreover, an infinite alphabet adds to the size of the product automaton, obtained by a generalization of the classical subset construction, used for determinization, in the finite alphabet case. Altogether, this prevents us from directly applying state-of-the-art methods and tool for checking emptiness of counter automata, or equivalently, nondeterministic integer programs, such as constrained Horn clause solvers [START_REF] Bjørner | Horn Clause Solvers for Program Verification[END_REF].

To tackle this problem, we developed a semi-algorithm that builds the product automaton on-the-fly, while checking its emptiness. We achieve practical efficiency by combining the principle of antichain-based language inclusion algorithms [33, 1] with the interpolantbased abstraction refinement semi-algorithm [START_REF] Mcmillan | Lazy abstraction with interpolants[END_REF], via a general notion of language-based subsumption relation. This semi-algorithm has been first presented in our work [START_REF] Iosif | Abstraction refinement and antichains for trace inclusion of infinite state systems[END_REF]. Compared with that work, this paper includes more details and also proofs of the results.

Moreover, here we introduce a notion of data simulations, i.e., simulation relations on generic register automata, inspired by [START_REF] Milner | An algebraic definition of simulation between programs[END_REF], and provide an algorithm to compute them. Further, we show how data simulations can be integrated into our trace inclusion semialgorithm in order to improve its performance as done previously in the context of classical finite-alphabet automata [START_REF] Abdulla | When simulation meets antichains[END_REF].

We have implemented the trace inclusion semi-algorithm as well as its combination with data simulations in a prototype tool INCLUDER2 and carried out a number of experiments, involving hardware, real-time systems, and array logic problems. The advantage of having a trace inclusion semi-algorithm is that we can write small automata-like specifications of the sets of good traces, instead of using, generally more complex, specifications of sets of erroneous behaviors.

An Overview of the Approach

We introduce the reader to our trace inclusion method by means of an example. Let us consider the network of generic register automata xA 1 , A 2 y and the generic register automaton B from Fig. 1. We prove that, for any value of ∆, any trace of the network xA 1 , A 2 y, obtained as an interleaving of the actions of A 1 and A 2 , is also a trace of the observer B. To this end, our procedure will fire increasingly longer sequences of input events, in search for a counterexample trace. We keep a set of predicates associated with each state pxq 1 , q 2 y, Pq of the product automaton where q i is a state of A i and P is a set of states of B. These predicates3 are formulae that define over-approximations of the data values reached simultaneously by the network, when A i is in the state q i , and by the observer B, in every state from P.

The first input event is init, on which A 1 and A 2 synchronize, moving together from the initial state xq 1 0 , q 2 0 y to xq 1 1 , q 2 1 y. In response, B can chose to either (i) move from tp 0 u to tp 1 u, matching the only transition rule from p 0 , or (ii) does not match the transition rule and move to the empty set. In the first case, the values of v match the relation of the rule p 0 init,v 1 "1 Ý ÝÝÝ Ñ p 1 , while in the second case, these values match the negated relation pv 1 " 1q.

pxq 1 1 , q 2 1 y, H, Jq ∆ ă x pxq 1 1 , q 2 1 y, H, v " 1q v " 2 init a 1 a 2 pxq 1 1 , q 2 1 y, H, ∆ ă xq a 1 pxq 1 1 , q 2 1 y, tp 2 u, ∆ ă x ^v " 2q v " 1 pxq 1 1 , q 2 1 y, tp 1 u, Jq a 1 pxq 1 1 , q 2 1 y, tp 1 u, v " 1q a 2 a 1 pivot pxq 1 1 , q 2 1 y, tp 1 u, v " 1q pxq 1 1 , q 2 1 y, tp 2 u, Jq (b) (a) a 1 pxq 1 1 , q 2 1 y, tp 1 u, v " 1q pxq 1 1 , q 2 1 y, tp 2 u, ∆ ă xq a 2 pxq 1 1 , q 2 1 y, tp 1 u, v " 1q pivot pxq 1 1 , q 2 1 y, tp 1 u, v " 1q pxq 1 1 , q 2 1 y, tp 2 u, pxq 1 1 , q 2 1 y, tp 1 u, v " 1q a 2 a 2 ∆ ă x ^v " 2q (c) (d)
init pxq 1 0 , q 2 0 y, tp 0 u, Jq pxq 1 0 , q 2 0 y, tp 0 u, Jq pxq 1 0 , q 2 0 y, tp 0 u, Jq pxq 1 0 , q 2 0 y, tp 0 u, Jq init init Fig. 2 A sample run of the proposed semi-algorithm.

The second case is impossible because the action of the network requires x 1 " 0 ^v1 " 1.

The only successor state is thus pxq 1 1 , q 2 1 y, tp 1 uq in Fig. 2 (a). Since no predicates are initially available at this state, the best over-approximation of the set of reachable data valuations is the universal set, denoted as J.

The second input event is a 1 , on which A 1 moves from q 1 1 back to itself, while A 2 makes an idle step because no transition with a 1 is enabled from q 2 1 . Again, B has the choice between moving from tp 1 u either to H or tp 1 u. Let us consider the first case, in which the successor state is pxq 1 1 , q 2 1 y, H, Jq. Since q 1 1 and q 2 1 are final states of A 1 and A 2 , respectively, and no final state of B is present in H, we say that the state is accepting. If the accepting state (in dashed boxes in Fig. 2) is reachable according to the transition constraints along the input sequence init.a 1 , we have found a counterexample trace that is in the language of xA 1 , A 2 y but not in the language of B.

To verify the reachability of the accepting state, we check the satisfiability of the path formula corresponding to the composition of the transition constraints θ 1 " x 1 " 0 ^v1 " 1 (init) and θ 2 " 0 ď x ă ∆ ^x1 " x `1 ^v1 " 1 ^ pv 1 " vq (a 1 ) in Fig. 2 (a). The formula θ 1 ^θ2 is unsatisfiable, and the proof of infeasibility provides the interpolant xv " 1y. This formula is an explanation for the infeasibility of the path because it is implied by the con-straint θ 1 and it is unsatisfiable in conjunction with the constraint θ 2 . By associating the new predicate v " 1 with the state pxq 1 1 , q 2 1 y, tp 1 uq, we ensure that the same spurious path will never be explored again.

We delete the spurious counterexample and recompute the states along the input sequence init.a 1 with the new predicate. In this case, pxq 1 1 , q 2 1 y, Hq is unreachable, and the outcome is pxq 1 1 , q 2 1 y, tp 1 u, v " 1q. However, this state was first encountered after the sequence init, so there is no need to store a second occurrence of this state in the tree. We say that the node init.a 1 is subsumed by init, and indicate this by a dashed arrow in Fig. 2 (b).

We continue with a 2 from the state pxq 1 1 , q 2 1 y, tp 1 u, v " 1q. In this case, A 1 makes an idle step and A 2 moves from q 2 1 to itself. In response, B has the choice between moving from tp 1 u to either (i) tp 1 u with the constraint v 1 " v, (ii) tp 2 u with the constraint v 1 " v `1, (iii) tp 1 , p 2 u with the constraint v 1 " v ^v1 " v `1 (this constraint is unsatisfiable, hence this case is discarded), (iv) H for data values that satisfy pv 1 " vq ^ pv 1 " v `1q. The first and the last cases are also discarded because the value of v after init constrained to 1 and the A 2 imposes further the constraint v 1 " 2 and v " 1 ^v1 " 2 ^v1 " v Ñ K for the first case and v " 1 ^v1 " 2 ^ pv 1 " vq ^ pv 1 " v `1q Ñ K. Hence, the only a 2 -successor of

pxq 1 1 , q 2 1 y, tp 1 u, v " 1q is pxq 1 1 , q 2
1 y, tp 2 u, Jq, in Fig. 2 (b). By firing the event a 1 from this state, we reach pxq 1 1 , q 2 1 y, H, v " 1q, which is, again, accepting. We check whether the path init.a 2 .a 1 is feasible, which turns out not to be the case. For efficiency reasons, we find the shortest suffix of this path that can be proved infeasible. It turns out that the sequence a 2 .a 1 is infeasible starting from the state pxq 1 1 , q 2 1 y, tp 1 u, v " 1q, which is called the pivot. This proof of infeasibility yields the interpolant xv " 1, ∆ ă xy, and a new predicate ∆ ă x is associated with pxq 1 1 , q 2 1 y, tp 2 uq. The refinement phase rebuilds only the subtree rooted at the pivot state, in Fig. 2

(b).

The procedure then builds the tree in Fig. 2 (c) starting from the pivot node and finds the accepting state pxq 1 1 , q 2 1 y, H, ∆ ă xq as the result of firing the sequence init.a 2 .a 2 . This path is spurious, and the new predicate v " 2 is associated with the location pxq 1 1 , q 2 1 y, tp 2 uq.

The pivot node is the same as in Fig. 2 (b), and, by recomputing the subtree rooted at this node with the new predicates, we obtain the tree in Fig. 2 (d), in which all frontier nodes are subsumed by their predecessors. Thus, no new event needs to be fired, and the procedure can stop reporting that the trace inclusion holds.

Related Work

Extending automata to deal with infinite alphabets is the purpose of the seminal work of Kaminski and Francez [START_REF] Kaminski | Finite-memory automata[END_REF], who introduce finite-memory automata that accept languages over infinite alphabets using a finite set of registers that can be overwritten and compared for equality with the input. In addition, our model of generic register automata is parametric in the theory of the data used and allows comparisons between adjacent elements in the input stream. For instance, generic register automata can easily specify increasing sequences of integers, which is out of the scope of finite-memory automata. Moreover, the language inclusion problem is undecidable for finite-memory automata, if the right-hand side has more than 2 registers, while decidability is proved for at most 2 registers. The trace inclusion problem has also been addressed in the context of timed automata [START_REF] Ouaknine | On the language inclusion problem for timed automata: Closing a decidability gap[END_REF]. Although the problem LpAq Ď LpBq is undecidable in general [START_REF] Alur | A theory of timed automata[END_REF], decidability is recovered when the B automaton has at most one clock, or the only constant appearing in the clock constraints is zero. These are essentially the only known decidable cases of language inclusion for timed automata.

The study of data automata [START_REF] Bojańczyk | Two-variable logic on data words[END_REF][START_REF] Decker | Ordered navigation on multi-attributed data words[END_REF] usually deals with the complexity of decision problems in logics describing data languages for simple theories, typically infinite data domains with equality. Here, we focus on undecidable language inclusion problems between data automata controlled by generic first-order theories, by providing a semi-algorithm that proves to be effective, in practice. Data words have also been considered in the context of symbolic visibly pushdown automata (SVPA) [START_REF] D'antoni | Symbolic visibly pushdown automata[END_REF]. Language inclusion is decidable for SVPAs with transition guards from a decidable theory because SVPAs are closed under complement and the emptiness can be reduced to a finite number of queries expressible in the underlying theory of guards. Decidability comes here at the cost of reducing the expressivity and forbidding comparisons between adjacent positions in the input -here only comparisons between matching call/return positions of the input nested words are allowed.

Although trace inclusion cannot be reduced to the emptiness problem of automata from the same class in linear time, due to the exponential blowup caused by determinization, this is possible if one considers an alternating automaton model, such as the one introduced in [START_REF] Iosif | Abstraction refinement for emptiness checking of alternating data automata[END_REF]. This work generalizes from the trace inclusion problems considered in this paper, by considering unrestricted alternation. As an advantage, one can complement in linear time without the need for determinization. On the negative side, however, the emptiness check for alternating automata with variables is heavier than in our case because it relies on the ability of the SMT solver to answer queries in a combined theory of data and booleans. Due to this reason, on some test cases, the semi-algorithm [START_REF] Iosif | Abstraction refinement for emptiness checking of alternating data automata[END_REF] performs slower than the trace inclusion semi-algorithm presented here.

Several works on model checking infinite-state systems against CTL [START_REF] Beyene | Solving existentially quantified horn clauses[END_REF] and CTL* [START_REF] Cook | On automation of ctl* verification for infinite-state systems[END_REF] specifications are related to our problem as they check inclusion between the set of computation trees of an infinite-state system and the set of trees defined by a branching temporal logic specification. First, the verification of existential CTL formulae [START_REF] Beyene | Solving existentially quantified horn clauses[END_REF] is reduced to solving forall-exists quantified Horn clauses by applying counterexample guided refinement to discover witnesses for existentially quantified variables. It is however not clear whether and how Horn clause solvers could be used for trace inclusion, which is a typical linear-time property, that requires an unbounded number of computation branches to synchronize on the same input word. To a very limited extent, for alphabets consisting of one symbol, one can encode the (non-)emptiness of alternating automata as the existence of solutions of a system of Horn clauses [?, Section 7.2.3]. However this encoding fails for alphabets of size two or more, let alone for infinite data alphabets. Moreover, we have not encountered a polynomial-time encoding of trace inclusion as a system of Horn clauses in the existing literature 4 .

Finally, the work [START_REF] Cook | On automation of ctl* verification for infinite-state systems[END_REF] on CTL* verification of infinite systems is based on partial symbolic determinization, using prophecy variables to summarize the future program execution. For finite alphabets, automata are a strictly more expressive formalism than temporal logics 5 . Such a comparison is, however, non-trivial for languages over infinite alphabets. However, in practice, we found the generic register automata considered in this paper to be a natural tool for specifying verification conditions of array programs [START_REF] Habermehl | What else is decidable about integer arrays? In[END_REF][START_REF] Habermehl | A logic of singly indexed arrays[END_REF][START_REF] Bozga | Automatic verification of integer array programs[END_REF] and regular properties of timed languages [START_REF] Alur | A theory of timed automata[END_REF].

Organization of the Paper

The rest of the paper is organized as follows: Section 2 describes preliminaries. Section 3 discusses closure properties of the considered class of generic register automata. Section 4 describes the trace inclusion semi-algorithm. Section 5 presents a concept of simulation relations on register automata and their integration into the proposed trace inclusion algorithm. Section 6 is an overview of our experimental evaluation, and, finally, Section 7 concludes the paper.

Preliminary Definitions

Let N denote the set of non-negative integers including zero. For any k, P N, k ď , we write rk, s for the set tk, k `1, . . . , u. We write K and J for the boolean constants false and true, respectively. Given a possibly infinite data domain D, we denote by FormpDq " xD, f 1 , . . . , f m y the set of syntactically correct first-order formulae with function symbols f 1 , . . . , f m . A variable x is said to be free in a formula φ, denoted as φpxq, iff it does not occur under the scope of a quantifier. Let x " tx 1 , . . . , x n u be a finite set of variables. A valuation ν : x Ñ D is an assignment of the variables in x with values from D. We denote by D x the set of such valuations. For a formula φpxq, we denote by ν |ù φ the fact that substituting in φ each variable x P x by νpxq yields a valid formula in the first-order theory of FormpDq. In this case, ν is said to be a model of φ. A formula is said to be satisfiable iff it has a model. For a formula φpx, x 1 q where x 1 " x 1 | x P x ( and two valuations ν, ν 1 P D x , we denote by pν, ν 1 q |ù φ the fact that the formula obtained from φ by substituting each x with νpxq and each x 1 with ν 1 px 1 q is valid in the first-order theory of FormpDq.

Generic Register Automata

Generic register automata6 (GRA) are extensions of non-deterministic finite automata with variables ranging over an infinite data domain D with the first-order theory of FormpDq.

Formally, a GRA is a tuple A " xD, Σ, x, Q, ι, F, ∆y, where:

-Σ is a finite alphabet of input events and ˛P Σ is a special padding symbol, -x " tx 1 , . . . , x n u is a set of variables, -Q is a finite set of states, ι P Q is an initial state, F Ď Q are final states, and -∆ is a set of rules of the form q σ,φpx,x 1 q Ý ÝÝÝ Ñ q 1 where σ P Σ is an alphabet symbol and φpx, x 1 q is a formula in FormpDq. A configuration of A is a pair pq, νq P Q ˆDx . We say that a configuration pq 1 , ν 1 q is a successor of pq, νq if and only if there exists a rule q σ,φ Ý Ñ q 1 P ∆ and pν, ν 1 q |ù φ. We denote the successor relation by pq, νq σ,φ Ý Ñ A pq 1 , ν 1 q, and we omit writing φ and A when no confusion may arise. We denote by succ A pq, νq " tpq 1 , ν 1 q | Dσ P Σ : pq, νq σ Ý Ñ A pq 1 , ν 1 qu the set of successors of a configuration pq, νq.

For any n ě 0, a trace is a finite sequence w " pν 0 , σ 0 q, . . . , pν n´1 , σ n´1 q, pν n , ˛q of pairs pν i , σ i q taken from the infinite alphabet D x ˆΣ [if n " 0, the trace is just pν 0 , ˛q]. A run of A over the trace w is a sequence of configurations π : pq 0 , ν 0 q

σ 0 Ý Ñ pq 1 , ν 1 q σ 1 Ý Ñ . . . σ n´1
ÝÝÑ pq n , ν n q [for n " 0, the run is pq 0 , ν 0 q only]. We say that the run π is accepting if and only if q n P F, in which case A accepts w. The language of A, denoted LpAq, is the set of traces accepted by A.

Generic Register Automata Networks

A generic register automata network (GRAN) is a non-empty tuple A " xA 1 , . . . , A N y of generic register automata A i " xD, Σ i , x i , Q i , ι i , F i , ∆ i y, i P r1, Ns whose sets of states are pairwise disjoint. A GRAN is a succint representation of an exponentially larger GRA

A e " xD, Σ A , x A , Q A , ι A , F A , ∆ A y,
called the expansion of A, where:

-Σ A " Σ 1 Y . . . Y Σ N and x A " x 1 Y . . . Y x N , -Q A " Q 1 ˆ. . . ˆQN , ι A " xι 1 , . . . , ι N y and F A " F 1 ˆ. . . ˆFN , -xq 1 , . . . , q N y σ,ϕ Ý Ñ xq 1 1 , . . . , q 1
N y if and only if there exists a set of indices I Ď r1, Ns such that (i) for all i P I, q i σ,ϕ i ÝÑ q 1 i , (ii) for all i R I, q i " q 1 i , and (iii) ϕ " Ź iPI ϕ i ^Ź jRI τ j , where I " ti P r1, Ns | q i σ,ϕ i ÝÑ q 1 i P ∆ i u is the set of GRA that can move from q i to q 1 i while reading the input symbol σ, and τ j "

Ź xPx j zp Ť iPI xiq x 1 "
x propagates the values of the local variables in A j that are not updated by tA i u iPI . Intuitively, all automata that can read an input symbol synchronize their actions on that symbol whereas the rest of the automata make an idle step and copy the values of their local variables which are not updated by the active automata. The language of the GRAN A is defined as the language of its expansion GRA, i.e., LpAq " LpA e q.

Trace Inclusion

Let A be a GRAN and A e " xD, Σ, x A , Q A , ι A , F A , ∆ A y be its expansion. For a set of variables y Ď x A , we denote by νÓ y the restriction of a valuation ν P D x A to the variables in y. For a trace w " pν 0 , σ 0 q, . . . , pν n , ˛q P pD x A ˆΣA q ˚, we denote by wÓ y the trace pν 0 Ó y , σ 0 q, . . . , pν n´1 Ó y , σ n´1 q, pν n Ó y , ˛q P pD y ˆΣq ˚. We lift this notion to sets of words in the natural way, by defining LpAqÓ y " wÓ y | w P LpAq ( . We are now ready to define the trace inclusion problem on which we focus in this paper.

Given a GRAN A as before and a GRA B " xD, Σ, x B , Q B , ι B , F B , ∆ B y such that x B Ď x A , the trace inclusion problem asks whether LpAqÓ xB Ď LpBq? The right-hand side GRA B is called observer, and the variables in x B are called observable variables.

Boolean Closure Properties of Generic Register Automata

We show first that generic register automata are closed under the boolean operations of union, intersection and complement and that they are amenable to determinization. Clearly, the emptiness problem is, in general, undecidable, due to the result of Minsky on 2-counter machines with integer variables, increment, decrement and zero test [START_REF] Minsky | Computation: Finite and Infinite Machines[END_REF].

Let A " xD, Σ, x, Q, ι, F, ∆y be a GRA for the rest of this section. A is said to be deterministic if and only if, for each trace w P LpAq, A has at most one run over w. The first result of this section is that, interestingly, any GRA can be determinized while preserving its language. The determinization procedure is a generalization of the classical subset construction for Rabin-Scott word automata on finite alphabets. The reason why determinization is possible for automata over an infinite data alphabet D x ˆΣ is that the successive values taken by each variable x P x are tracked by the language LpAq Ď pD x ˆΣq ˚. This assumption is crucial: a typical example of automata over an infinite alphabet, that cannot be determinized, are timed automata [START_REF] Alur | A theory of timed automata[END_REF], where only the elapsed time is reflected in the language, and not the values of the variables (clocks).

Formally, the deterministic GRA accepting the language LpAq is defined as

A d " xD, Σ, x, Q d , ι d , F d , ∆ d y, where Q d " 2 Q , ι d " tιu, F d " tP Ď Q | P X F ‰ Hu and ∆ d is the set of rules P σ,θ
Ý Ñ P 1 such that the formula: 7 . The main difference with the classical subset construction for Rabin-Scott automata is that here we consider all sets P 1 of states that have a predecessor in P, not just the maximal such set. This refined subset construction takes into account not just the alphabet symbols in Σ, but also the valuations of the variables in x. Observe, moreover, that A d can be built for any first-order theory of FormpDq that is closed under conjunction, disjunction, and negation. The following lemma states the main properties of A d .

θpx, x 1 q " ľ p 1 PP 1 ł p σ,ψ Ý Ñp 1 P∆ pPP ψ ^ľ p 1 PQzP 1 ľ p σ,ϕ Ý Ñp 1 P∆ pPP ϕ is satisfiable
Lemma 1 Given a GRA A " xD, Σ, x, Q, ι, F, ∆y, (1) for any w P pD x ˆΣq ˚and P P Q d , A d has exactly one run on w that starts in P, and (2) LpAq " LpA d q.

Proof (1) Let w " pν 0 , σ 0 q, . . . , pν n´1 , σ n´1 q, pν n , ˛q be an arbitrary trace and P Ď Q be a state of A d . We first build a run π " pP 0 , ν 0 q σ 0 ,θ 0

Ý Ý Ñ pP 1 , ν 1 q . . . σ n´1 ,θ n´1
Ý ÝÝÝÝ Ñ pP n , ν n q of A d such that P 0 " P, by induction on n ě 0. If n " 0, then w " pν 0 , ˛q and π " pP 0 , ν 0 q is trivially a run of A d over w. For the induction step, let n ą 0 and suppose that A d has a run pP 0 , ν 0 q σ 0 ,θ 0 Ý Ý Ñ . . . pP n´1 , ν n´1 q such that P 0 " P. We extend this run to a run over w by considering:

P n " ! p P Q | Dq P P n´1 . q σ n´1 ,φ Ý ÝÝ Ñ p P ∆ and pν n´1 , ν n q |ù φ ) , θ n " Ź p 1 PPn Ž p σ,ψ Ý Ñp 1 P∆ pPP n´1 ψ ^Źp 1 PQzPn Ź p σ,ϕ Ý Ñp 1 P∆ pPP n´1 ϕ.
It is not hard to see that pν n´1 , ν n q |ù θ n , thus pP 0 , ν 0 q σ 0 ,θ 0 Ý Ý Ñ . . .

σn ,θn

Ý Ý Ñ pP n , ν n q is indeed a run of A d over w. To show that π is unique, suppose, by contradiction, that there exists a different run π 1 " pR 0 , ν 0 q σ 0 ,ω 0 ÝÝÑ pR 1 , ν 1 q . . .

σ n´1 ,ω n´1
Ý ÝÝÝÝ Ñ pR n , ν n q such that P 0 " R 0 " P. Notice that the relation labeling any transition rule P i σ i ,θ i Ý Ý Ñ P i`1 is entirely determined by the sets P i and P i`1 , so two runs are different iff they differ in at least one state, i.e., P j ‰ R j for some j P r1, ns. Let i denote the smallest such j and suppose that there exists p P P i such that p R R i (the symmetrical case p P R i and p R P i is left to the reader). By the definition of ∆ d , there exists q P P i´1 " R i´1 such that q

σ i´1 ,ψ Ý ÝÝ Ñ p P ∆. Since pν i´1 , ν i q |ù θ i´1 ^ωi´1 , we obtain that pν i´1 , ν i q |ù Ž tψ | q σ i´1 ,ψ Ý ÝÝ Ñ p P ∆, q P P i´1 u and pν i´1 , ν i q |ù Ź t ψ | q σ i´1 ,ψ
Ý ÝÝ Ñ p P ∆, q P P i´1 u, contradiction. Thus π is the only run of A d over w starting in P.

(2) Let w " pν 0 , σ 0 q, . . . , pν n´1 , σ n´1 q, pν n , ˛q be a trace. "Ď" If w P LpAq, then A has

a run pq 0 , ν 0 q σ 0 ,φ 0 Ý Ý Ñ . . . σ n´1 ,φ n´1
Ý ÝÝÝÝ Ñ pq n , ν n q such that q 0 " ι and q n P F. By Point 1, A d has a unique run pP 0 , ν 0 q

σ 0 ,θ 0 Ý Ý Ñ . . . σ n´1 ,θ n´1
Ý ÝÝÝÝ Ñ pP n , ν n q over w. We prove that q i P P i by induction on i P r0, ns. For i " 0, we have P 0 " tιu by the definition of A d . For the induction step, suppose that i P r1, ns and q i´1 P P i´1 . By contradiction, assume that q i R P i . Since pν i´1 , ν i q |ù θ i´1 , we obtain pν i´1 , ν i q |ù φ i´1 , contradiction. Thus q i P P i for all i P r0, ns, and q n P P n , hence P n X F ‰ H. Then P n P F d , and w P LpA d q. "Ě" If w P LpA d q, then A d has a (unique) run

pP 0 , ν 0 q σ 0 ,θ 0 Ý Ý Ñ pP 1 , ν 1 q . . . σ n´1 ,θ n´1
Ý ÝÝÝÝ Ñ pP n , ν n q over w such that P 0 " tιu and P n X F ‰ H. Then there exists p n P P n X F, and, by the definition of A d , there exists p n´1 P P n´1 such that p n´1 σ n´1 ,ψ n´1 Ý ÝÝÝÝ Ñ p n P ∆ and pν n´1 , ν n q |ù ψ n´1 . Continuing this argument backwards, we can find a run pq 0 , ν 0 q σ 0 ,ψ 0 ÝÝÑ . . .

σ n´1 ,ψ n´1
Ý ÝÝÝÝ Ñ pq n , ν n q of A over w such that q i P P i for all i P r0, ns.

Since P 0 " tιu and q n P F, we obtain that w P LpAq.

[ \ The construction of a deterministic GRA recognizing the language of A is key to defining a GRA that recognizes the complement of A.

Let A " xD, Σ, x, Q d , ι d , Q d zF d , ∆ d y.
In other words, A has the same structure as A d , and the set of final states consists of those subsets that contain no final state, i.e., tP Ď Q | P X F " Hu. Using Lemma 1, it is not difficult to show that LpAq " pD x ˆΣq ˚zL pAq.

Next, we show closure of GRA under intersection. Let B " xD, Σ, x, Q 1 , ι 1 , F 1 , ∆ 1 y be a GRA and define A ˆB " xD, Σ, x, Q ˆQ1 , pι, ι 1 q, F ˆF1 , ∆ ˆy where pq, q 1 q σ,ϕ Ý Ñ pp, p 1 q P ∆ îf and only if q σ,φ Ý Ñ p P ∆, q 1 σ,ψ Ý Ñ p 1 P ∆ 1 and ϕ " φ ^ψ. It is easy to show that LpA ˆBq " LpAq X LpBq. GRA are also closed under union since LpAq Y LpBq " LpA ˆBq.

Let us turn now to the trace inclusion problem. The following lemma shows that this problem can be effectively reduced to an equivalent language emptiness problem. However, note that this reduction does not work when the trace inclusion problem is generalized by removing the condition x B Ď x A . In other words, if the observer uses local variables not shared with the network8 , i.e., x B zx A ‰ H, the generalized trace inclusion problem LpAqÓ xAXxB Ď LpBqÓ xAXxB has a negative answer iff there exists a trace w " pν 0 , σ 0 q, . . . , pν n , ˛q P LpAq such that, for all valuations µ 0 , . . . , µ n P D xBzxA , we have w 1 " pν 0 Ó xAXxB Y µ 0 , σ 0 q, . . . , pν n Ó xAXxB Y µ n , ˛q R LpBq. This kind of quantifier alternation cannot be easily accommodated within the framework of language emptiness, in which only one type of (existential) quantifier occurs. The trace inclusion problem is undecidable, which can be shown by reduction from the language emptiness problem for GRA (take B such that LpBq " H). However, the above lemma shows that any semi-decision procedure for the language emptiness problem can also be used to deal with the trace inclusion problem.

Lemma 2 Given GRA A " xD, Σ, x A , Q A , ι A , F A , ∆ A y and B " xD, Σ, x B , Q B , ι B , F B , ∆ B y such that x B Ď x A .

Abstract, Check, and Refine for Trace Inclusion

This section describes our semi-algorithm for checking the trace inclusion between a given network A and an observer B. Let A e denote the expansion of A, defined in Section 2. In the light of Lemma 2, the trace inclusion problem LpAqÓ xB Ď LpBq, where the set of observable variables x B is included in the set of network variables, can be reduced to the language emptiness problem LpA e ˆBq " H.

Although language emptiness is in general undecidable for generic register automata [START_REF] Minsky | Computation: Finite and Infinite Machines[END_REF], several cost-effective semi-algorithms and tools [START_REF] Henzinger | Lazy abstraction[END_REF][START_REF] Mcmillan | Lazy abstraction with interpolants[END_REF][START_REF] Grebenshchikov | Synthesizing software verifiers from proof rules[END_REF][START_REF] Bardin | Fast: Fast acceleration of symbolic transition systems[END_REF] have been developed, showing that it is possible, in many practical cases, to provide a yes/no answer to this problem. However, to apply one of the existing off-the-shelf tools to our problem, one needs to build the product automaton A e ˆB prior to the analysis. Due to the inherent state explosion caused by the interleaving semantics of the network as well as by the complementation of the observer, such a solution would not be efficient in practice.

To avoid building the product automaton, our procedure builds on-the-fly an overapproximation of the (possibly infinite) set of reachable configurations of A e ˆB. This overapproximation is defined using the approach of lazy predicate abstraction [START_REF] Henzinger | Lazy abstraction[END_REF], combined with counterexample-driven abstraction refinement using interpolants [START_REF] Mcmillan | Lazy abstraction with interpolants[END_REF]. We store the explored abstract states in a structure called an antichain tree. In general, antichain-based algorithms [33,1] store only states which are incomparable wrt a partial order called subsumption. Our method can be thus seen as an extension of the antichain-based language inclusion algorithms [33,1] to infinite state systems by means of predicate abstraction and interpolation-based refinement. Since the trace inclusion problem is undecidable in general, termination of our procedure is not guaranteed; in the following, we shall, however, call our procedure an algorithm for the sake of brevity.

Antichain Trees

In this section, we define antichain trees, which are the main data structure of the trace inclusion (semi-)algorithm. Let A " xA 1 , . . . , A N y be a network of automata where

A i " xD, Σ i , x i , Q i , ι i , F i , ∆ i y, for all i P r1, Ns, and let B " xD, Σ, x B , Q B , ι B , F B , ∆ B y be an observer such that x B Ď Ť N i"1 x i . We also denote by A e " xD, Σ A , x A , Q A , ι A , F A , ∆ A y
the expansion of the network A and by A e ˆB " xD, Σ A , x A , Q p , ι p , F p , ∆ p y the product automaton used for checking language inclusion. An antichain tree for the network A and the observer B is a tree whose nodes are labeled by product states (see Fig. 2 for examples) 9 . Intuitively, a product state is an overapproximation of the set of reachable configurations of the product automaton A e ˆB that share the same control state. Formally, a product state for A and B is defined as a tuple s " pq, P, Φq where (i) pq, Pq is a state of A e ˆB with q " xq 1 , . . . , q N y being a state of the network expansion A e and P being a set of states of the observer B, and (ii) Φpx A q P FormpDq is a formula which defines an over-approximation of the set of valuations of the variables x A that reach the state pq, Pq in A e ˆB. A product state s " pq, P, Φq is a finite representation of a possibly infinite set of configurations of A e ˆB, denoted as rrsss " tpq, P, νq | ν |ù Φu. 10To build an over-approximation of the set of reachable states of the product automaton, we need to compute, for a product state s, an over-approximation of the set of configurations that can be reached in one step from s. To this end, we define first a finite abstract domain of product states, based on the notion of predicate map. A predicate map is a partial function that associates sets of facts 11 about the values of the variables used in the product automaton with components of a product state. Facts are called predicates and components of a product state are called substates. Formally, a substate of a state pxq 1 , . . . , q N y, Pq P Q p of the product automaton A e ˆB is a pair pxq i1 , . . . , q ik y, Sq such that (i) xq i1 , . . . , q ik y is a subsequence of xq 1 , . . . , q N y, and (ii) S ‰ H only if S X P ‰ H.

The reason behind the distribution of predicates over substates is two-fold. First, we would like the abstraction to be local, i.e., the predicates needed to define a certain subtree in the antichain must be associated with the labels of that subtree only. Second, once a predicate appears in the context of a substate, it should be subsequently reused whenever that same substate occurs as part of another product state.

We denote the substate relation by pxq i1 , . . . , q ik y, Sq Ÿ pxq 1 , . . . , q N y, Pq. The substate relation requires the automata A i1 , . . . , A ik of the network A to be in the control states q i1 , . . . , q ik simultaneously, and the observer B to be in at least some state of S provided S ‰ H (if S " H, the state of B is considered to be irrelevant). Let S xA,By " tr | Dq P Q p . r Ÿ qu be the set of substates of a state of A e ˆB.

A predicate map Π : S xA,By Ñ 2 FormpD q associates each substate pr,

Sq P Q i1 ˆ. . . ˆQik 2QB
with a set of formulae πpxq where (i)

x " x i1 Y . . . Y x ik Y x B if S ‰ H, and (ii) x " x i1 Y . . . Y x ik if S " H.
Notice that a predicate associated with a substate refers only to the local variables of those network components A i1 , . . . , A ik and of the observer B that occur in the particular substate.

Example 1 The antichain in Fig. 2 (d) uses the predicate map pxq 1 1 , q 2 1 y, tp 1 uq Þ Ñ tv " 1u,

pxq 1 1 , q 2 1 y, tp 2 uq Þ Ñ t∆ ă x, v " 2u.
We are now ready to define the abstract semantics of the product automaton A e ˆB, induced by a given predicate map. For convenience, we define first a set Postpsq of concrete successors of a product state s " pq, P, Φq such that pr, S, Ψq P Postpsq if and only if (i) the product automaton A e ˆB has a rule pq, Pq σ,θ Ý Ñ pr, Sq P ∆ p and Ψpx A q " Dx 1 A . Φpx 1

A q θpx 1 A , x A q is satisfiable. The set of concrete successors does not contain states with empty set of valuations because these states are unreachable in A e ˆB.

Given a predicate map Π, the set Post Π psq of abstract successors of a product state s is defined as follows: pr, S, Ψ 7 q P Post Π psq if and only if (i) there exists a product state pr, S, Ψq P Postpsq and (ii) Ψ 7 px A q " Ź rŸpr,Sq Ź tπ P Πprq | Ψ Ñ πu. In other words, the set of data valuations reachable by an abstract successor is the tightest over-approximation of the concrete set of reachable valuations, obtained as the conjunction of the available predicates from the predicate map that over-approximate this set.

Example 2 (Continued from Ex. 1) Consider the antichain from Fig. 2 (d). The concrete successors of s " pxq 1 1 , q 2 1 y, tp 1 u, v " 1q are pxq 1 1 , q 2 1 y, tp 1 u, Ψ 1 q and pxq 1 1 , q 2 1 y, tp 2 u, Ψ 2 q:

Ψ 1 " Dv 1 , x 1 , ∆ 1 . v 1 " 1 ^x " x 1 `1 ^v " 1 ^∆ " ∆ 1 ^0 ď x 1 ă ∆ ^v " v 1 , Ψ 2 " Dv 1 , x 1 , ∆ 1 . v 1 " 1 ^x " x 1 `1 ^v " 2 ^∆ " ∆ 1 ^∆ ď x 1 ă 2∆ ^v " v 1 `1.
With predicate map Π from Ex. 1, Post Π psq " tpxq 1 1 , q 2 1 y, tp 1 u, Ψ 7

1 q, pxq 1 1 , q 2 1 y, tp 2 u, Ψ 7
2 qu:

pΨ 1 Ñ v " 1q Ñ pΨ 7 1 " v " 1q, pΨ 2 Ñ v " 2 and Ψ 2 Ñ ∆ ă xq Ñ pΨ 7 2 " v " 2 ^∆ ă xq.
Finally, an antichain tree (or, simply antichain) T for A and B is a tree whose nodes are labeled with product states and whose edges are labeled by input symbols and concrete transition relations. Let N ˚be the set of finite sequences of natural numbers that denote the positions in the tree. For a tree position p P N ˚and i P N, the position p.i is a child of p.

A set S Ď N ˚is said to be prefix-closed if and only if, for each p P S and each prefix q of p, we have q P S as well. The root of the tree is denoted by the empty sequence ε. Each antichain node n " ps, d 1 . . . d k q P T is naturally associated with a path from the root to itself ρ :

n 0 σ 1 ,θ 1 Ý Ý Ñ n 1 σ 2 ,θ 2 Ý Ý Ñ . . . σ k θ k Ý Ý Ñ n k .
We denote by ρ i the node n i for each i P r0, ks, and by |ρ| " k the length of the path. The path formula associated with ρ is Θpρq "

Ź k i"1 θ i px i´1 A , x i A q where x i A " x i | x P x A (
is a set of indexed variables for each i P r0, ks.

Example 3 Consider the following path ρ : pxq 1 0 , q 2 0 y, tp 0 u, Jq

init Ý Ñ pxq 1 1 , q 2 1 y, tp 1 u, v " 1q a 2 Ý Ñ pxq 1 1 , q 2 1 y, tp 2 u, ∆ ă xq a 2
Ý Ñ pxq 1 1 , q 2 1 y, H, ∆ ă xq in the antichain from Fig. 2 (c). The path formula of ρ is Θpρq " θ 1 ^θ2 ^θ3 where:

θ 1 " v 1 " 1 ^x1 " 0 ^0 ă ∆ 1 , θ 2 " v 2 " v 1 `1 ^∆2 " ∆ 1 ^v2 " 2 ^x2 " x 1 `1 ^∆1 ď x 1 ă 2∆ 1 ^ pv 2 " v 1 q, θ 3 " v 3 " 2 ^∆3 " ∆ 2 ^x3 " x 2 `1 ^∆2 ď x 2 ă 2∆ 2 ^ pv 3 " v 2 q.

Counterexample-driven Abstraction Refinement

A counterexample is a path from the root of the antichain to a node which is labeled by an accepting product state. A product state pq, P, Φq is said to be accepting iff pq, Pq is an accepting state of the product automaton A e ˆB, i.e., q P F A and P X F B " H. A coun- terexample is said to be spurious if its path formula is unsatisfiable, i.e., the path does not correspond to a concrete execution of A e ˆB. In this case, we need to (i) remove the path ρ from the current antichain and (ii) refine the abstract domain in order to exclude the occurrence of ρ from future state space exploration.

Let ρ : root xA,By " pq 0 , P 0 , Φ 0 q

θ 1 Ý Ñ pq 1 , P 1 , Φ 1 q θ 2 Ý Ñ . . . θ k
Ý Ñ pq k , P k , Φ k q be a spurious counterexample in the following. For efficiency reasons, we would like to save as much work as possible and remove only the smallest suffix of ρ which caused the spuriousness. For some j P r0, ks, let Θ j pρq " Φ j px 0 A q ^Źk i" j θ i px i´j A , x i´j`1 A q be the formula defining all sequences of data valuations that start in the set Φ j and proceed along the suffix pq j , P j , Φ j q Ý Ñ . . . Ý Ñ pq k , P k , Φ k q of ρ. The pivot of a path ρ is the maximal position j P r0, ks such that Θ j pρq is unsatisfiable, and ´1 if ρ is not spurious.

Example 4 (Continued from Ex.

3) The path formula Θpρq " θ 1 ^θ2 ^θ3 from Ex. 3 is unsatisfiable, thus ρ is a spurious counterexample. Moreover, we have unsatisfiable Θ 1 pρq " J ^θ2 ^θ3 because of the unsatisfiable subformula v 2 " 2 ^v3 " 2 ^ pv 3 " v 2 q. Since Θ 2 pρq is satisfiable, the pivot of ρ is 1.

Finally, we describe the refinement of the predicate map, which ensures that a given spurious counterexample will never be found in a future iteration of the abstract state space exploration. The refinement is based on the notion of interpolant [START_REF] Mcmillan | Lazy abstraction with interpolants[END_REF].

Definition 2 Given a formula Φpxq and a sequence xθ 1 px, x 1 q, . . . , θ k px, x 1 qy of formulae, an interpolant is a sequence of formulae I " xI 0 pxq, . . . , I k pxqy where: (1) Φ Ñ I 0 , (2) I k Ñ K, and (3) I i´1 pxq ^θi px, x 1 q Ñ I i px 1 q for all i P r1, ks.

Any given interpolant is a witness for the unsatisfiability of a (suffix) path formula Θ j pρq. Dually, if Craig's Interpolation Lemma [START_REF] Craig | Three uses of the herbrand-gentzen theorem in relating model theory and proof theory[END_REF] holds for the considered first-order data theory, any infeasible path formula is guaranteed to have an interpolant. The interpolant can be computed by means of Satisfiability Modulo Theories (SMT) solvers [START_REF] Cimatti | The MathSAT5 SMT Solver[END_REF][START_REF] Mcmillan | Interpolants from z3 proofs[END_REF].

Example 5 (Continued from Ex. 4) Let Φ " J (variables initially unconstraint) and the sequence of formula be xθ 1 , θ 2 , θ 3 y from Ex. 3. An interpolant is a sequence I " xJ, v " 2, Ky.

Given a spurious counterexample ρ " pq 0 , P 0 , Φ 0 q θ 1 Ý Ñ . . . θ k Ý Ñ pq k , P k , Φ k q with pivot j ě 0, an interpolant I " xI 0 , . . . , I k´j y for the infeasible path formula Θ j pρq can be used to refine the abstract domain by augmenting the predicate map Π. A simple possible refinement is to add the formula I i into Πppq j`i , P j`i qq for each 0 ď i ď pk ´jq. As an effect of this refinement, the antichain construction algorithm will avoid every path with the suffix pq j , P j , Φ j q Ý Ñ . . . Ý Ñ pq k , P k , Φ k q in a future iteration. We use an improved version of this simple refinement in order to obtain more reusable predicates. If I i " C 1 i py 1 q ^. . . ^Cmi i py mi q is a conjunctive normal form (CNF) of the ith component of the interpolant, we consider the substate pr i , S i q for each C i py q where P r1, m i s:

-r i " xq i1 , . . . , q ih y where 1 ď i 1 ă . . . ă i h ď N is the largest sequence of indices such that x ig X y ‰ H for each g P r1, hs and the set x ig of variables of the network component GRA A ig , -S i " P i if x B X y ‰ H, and S i " H, otherwise.

A predicate map Π is said to be compatible with a spurious path ρ :

s 0 θ 1 Ý Ñ . . . θ k
Ý Ñ s k with pivot j ě 0 if s j " pq j , P j , Φ j q and there is an interpolant I " xI 0 , . . . , I k´j y of the suffix xθ j , . . . , θ k y wrt. Φ j such that, for each clause C of some equivalent CNF of I i , i P r0, k ´js, it holds that C P Πprq for some substate r Ÿ s i`j . The following lemma proves that, under a predicate map compatible with a spurious path ρ, the antichain construction will exclude further paths that share the suffix of ρ starting with its pivot.

Lemma 3 Let ρ : pq 0 , P 0 , Φ 0 q θ 0 Ý Ñ pq 1 , P 1 , Φ 1 q θ 1 Ý Ñ . . . θ k´1
Ý Ý Ñ pq k , P k , Φ k q be a spurious counterexample and Π a predicate map compatible with ρ. Then, there is no sequence of product states pq j , P j , Ψ 0 q, . . . , pq k , P k , Ψ k´j q such that: (1) Ψ 0 Ñ Φ j and (2) pq i`1 , P i`1 , Ψ i´j`1 q P Post Π ppq i , P i , Ψ i´j qq for all i P r j, k ´1s.

Proof Let j P r0, ks be the pivot of ρ. Since ρ is spurious, there exists an interpolant I " xI 0 , . . . , I k´j y for Φ j and xθ j , . . . , θ k y. It is sufficient to prove that Ψ i Ñ I i for all i P r0, k js.

Since I k´j " K, we obtain Ψ k´j " K, and consequently pq k´j , P k´j , Kq P Post Π ppq k´j´1 , P k´j´1 , Ψ k´j´1 qq. By the definition of Post Π , we have pq k´j , P k´j , Kq P Postppq k´j´1 , P k´j´1 , Ψ k´j´1 qq, which contradicts with the definition of Post. We show that Ψ i Ñ I i for all i P r0, k ´js, by induction on k ´j. For the base case k ´j " 0, we have Ψ 0 Ñ Φ j Ñ I 0 . For the induction step, we assume Ψ i Ñ I i for all i P r0, k ´j ´1s and prove Ψ k´j Ñ I k´j . By the induction hypothesis, we have: Ψ k´j´1 px A q Ñ I k´j´1 px A q and Ψ k´j´1 px A q ^θk´j´1 px A , x 1 A q Ñ I k´j´1 px A q ^θk´j´1 px A , x 1 A q Ñ I k´j px 1 A q.

Let C 1 ^. . . ^C be the CNF of I k´j . Since Π is compatible with ρ, for each clause C i , there exists a substate r Ÿ pq k , P k q such that C i P Πprq. By the definition of Post Π , we obtain that Ψ k´j Ñ C i for each i P r1, s, hence Ψ k´j Ñ I k´j .

[ \

Observe that the refinement induced by interpolation is local since Π associates sets of predicates with substates of the states in A e ˆB, and the update impacts only the states occurring within the suffix of that particular spurious counterexample.

Subsumption

The main optimization of antichain-based algorithms [START_REF] Abdulla | When simulation meets antichains[END_REF] for checking language inclusion of automata over finite alphabets is that product states that are subsets of already visited states are never stored in the antichain. On the other hand, language emptiness semi-algorithms, based on predicate abstraction [START_REF] Mcmillan | Lazy abstraction with interpolants[END_REF] use a similar notion to cover newly generated abstract successor states by those that were visited sooner and that represent larger sets of configurations. In this case, state coverage does not only increase efficiency but also ensures termination of the semi-algorithm in many practical cases.

In this section, we generalize the subset relation used in classical antichain algorithms with the notion of coverage from predicate abstraction, and we define a more general notion of subsumption for generic register automata. Given a state pq, Pq of the product automaton A e ˆB and a valuation ν P D xA , the residual language L pq,P,νq pA e ˆBq is the set of traces w accepted by A e ˆB from the state pq, Pq such that ν is the first valuation which occurs on w. This notion is then lifted to a product state s " pq, P, Φq as follows: L s pA e ˆBq " Ť pq,P,νqPrrsss L pq,P,νq pA e ˆBq where rrsss " tpq, P, νq | ν |ù Φu-i.e. the set of configurations of the product automaton A e ˆB represented by the given product state s. Definition 3 Given a GRAN A and a GRA B, a partial order Ď is a subsumption provided that, for any two product states s and t, we have s Ď t only if L s pA e ˆBq Ď L t pA e ˆBq.

A procedure for checking the emptiness of A e ˆB needs not continue the search from a product state s if it has already visited a product state t that subsumes s. The intuition is that any counterexample discovered from s can also be discovered from t. The trace inclusion semi-algorithm described below in Section 4.4 works, in principle, with any given subsumption relation. In practice, our implementation uses the subsumption relation defined by the lemma below: Lemma 4 The relation defined such that pq, P, Φq Ď img pr, S, Ψq ðñ q " r, P Ě S, and Φ Ñ Ψ is a subsumption. Proof For any valuation ν P D xA , we have L pq,P,νq pA e ˆBq " L pq,νq pA e q X L pP,νq pBq. Since P Ě S, we have L pP,νq pBq Ě L pS,νq pBq, thus L pP,νq pBq Ď L pS,νq pBq. We obtain that L pq,P,νq pA e Bq Ď L pr,νq pA e q X L pS,νq pBq " L pr,S,νq pA e ˆBq. Since moreover Φ Ñ Ψ, we have that L pq,P,Φq pA e ˆBq Ď L pr,S,Φq pA e ˆBq Ď L pr,S,Ψq pA e ˆBq.

[ \ Algorithm 1 Trace Inclusion Semi-algorithm input:

1. A GRAN A " xA 1 , . . . , A N y such that A i " xD, Σ i , x i , Q i , ι i , F i , ∆ i y for all i P r1, Ns. 2. A GRA B " xD, Σ, x B , Q B , ι B , F B , ∆ B y such that x B Ď Ť N i"

24:

i Ð i `1

25:

for n P Visited such that n has a successor m P rem do

26:

add pn, succq to Subsume

27:

for pn, mq P Subsume such that m P rem do 1 , q 2 1 y, tp 1 u, v " 1q Ď img pxq 1 1 , q 2 1 y, tp 1 u, v " 1q because xq 1 1 , q 2 1 y " xq 1 1 , q 2 1 y, tp 1 u Ě tp 1 u, and v " 1 Ñ v " 1.

The language inclusion algorithm for non-deterministic automata on finite alphabets [START_REF] Abdulla | When simulation meets antichains[END_REF] uses also a more sophisticated subsumption relation based on a pre-computed simulation [START_REF] Milner | An algebraic definition of simulation between programs[END_REF] between the states of the automata. We have defined a similar notion of simulation for generic register automata and an algorithm for computing such simulations. Details concerning data simulations and their integration within the framework of antichain-based abstraction refinement are described in Section 5.

The Trace Inclusion Semi-algorithm

With the previous definitions, Algorithm 1 describes the procedure for checking trace inclusion. It uses a classical worklist iteration loop (lines 2-30) that builds an antichain tree by simultaneously unfolding the expansion A e of the network A and the complement B of the the observer B, while searching for a counterexample trace w P LpA e ˆBq. Both A e and B are built on-the-fly, during the abstract state space exploration.

Within Algorithm 1, the antichain is represented as a set of nodes. Each node is a tuple xs, py where s is a product state and p is a position in the tree. The processed antichain nodes are kept in the set Visited, and their abstract successors, not yet processed, are kept in the set Next. Initially, Visited " H and Next " xroot A,B , εy ( . The algorithm uses a predicate map Π, which is initially empty (line 1).

We keep a set of subsumption edges Subsume Ď Visited ˆpVisited Y Nextq with the following meaning: pxs, py, xt, qyq P Subsume for two antichain nodes, where s,t are product states and p, q P N ˚are tree positions, if and only if there exists an abstract successor s 1 P Post Π psq such that s 1 Ď t (Definition 3). Observe that we do not explicitly store a subsumed successor of a product state s from the antichain; instead, we add a subsumption edge between the node labeled with s and the node that subsumes that particular successor. The algorithm terminates when each abstract successor of a node from Next is subsumed by some node from Visited.

An iteration of Algorithm 1 starts by choosing a current antichain node curr " xs, py from Next and moving it to Visited (line 3). If the product state s is accepting (line 5), we check the counterexample path ρ, from the root of the antichain to curr, for spuriousness, by computing its pivot k (see Section 4.2). If k ě 0, then ρ is a spurious counterexample (line 7), and the path formula of the suffix of ρ, which starts with position k, is infeasible. In this case, we compute an interpolant for the suffix and refine the current predicate map Π by adding the predicates from the interpolant to the corresponding substates of the product states from the suffix (line 8).

The function REFINEPREDICATEMAPBYINTERPOLATION updates the predicate map using the principle described in Section 4.2. Subsequently, we remove (line 12) from the current antichain the subtree rooted at the pivot node ρ k , i.e., the k-th node on the path ρ (line 9), and add ρ k to Next in order to trigger a recomputation of this subtree with the new predicate map. Moreover, all nodes with a successor previously subsumed by a node in the removed subtree are moved from Visited back to Next in order to reprocess them (line 11).

On the other hand, if the counterexample ρ is found to be real (k " ´1), any valuation

ν P Ť |ρ| i"0 D x i
A that satisfies the path formula Θpρq yields a counterexample trace w P LpAqÓ xB zLpBq, obtained by ignoring all variables from x A zx B (line 15). If the current node is not accepting, we generate its abstract successors (line 18). In order to keep in the antichain only nodes that are incomparable wrt the subsumption relation Ď, we add a successor t of s to Next (lines 23 and 30) only if it is not subsumed by another product state from a node m P Visited. Otherwise, we add a subsumption edge pcurr, mq to the set Subsume (line 20). Furthermore, if t is not subsumed by another state in Visited, we remove from Next all nodes xt 1 , p 1 y such that t strictly subsumes t 1 (lines 22 and 29) and add subsumption edges to the node storing t from all nodes with a removed successor (line 26) or a removed subsumption edge (line 28).

The following theorem states the soundness of our trace inclusion semi-algorithm. The dual question "if there exists a counterexample trace w P LpAq Ó xB zLpBq, will Algorithm 1 discover it?" can also be answered positively, using an implementation that enumerates the abstract paths in a systematic way, e.g., by using a breadth-first path exploration. This can be done using a queue to implement the Next set in Algorithm 1.

Theorem 1 Let A " xA 1 , . . . , A N y be a GRAN such that A i " xD, Σ i , x i , Q i , ι i , F i , ∆ i y for all i P r1, Ns, and let B " xD, Σ, x B , Q B , ι B , F B , ∆ B y be a GRA such that x B Ď Ť N i"1 x i . If Algorithm

Proof of Theorem 1

Given a network A " xA 1 , . . . , A N y where A i " xD, Σ i , x i , Q i , ι i , F i , ∆ i y for all i P r1, Ns and an observer B " xD, Σ, x B , Q B , ι B , F B , ∆ B y, we recall that a configuration of the product automaton A e ˆB is a tuple pxq 1 , . . . , q N y, P, νq P Q 1 ˆ. . . ˆQN ˆ2QB ˆDxA , and a node of the antichain T is a pair xs, py where s is a product state for A and B and p P N ˚is a tree position. Moreover, root xA,By " pxι 1 , . . . , ι N y, tι B u, Jq is the product state that labels the root of T . In the following, let Γ " pΠ, Visited, Next, Subsumeq be an antichain state where Π is the predicate map, and Visited, Next, and Subsume are the sets of antichain nodes handled by Algorithm 1.

We say that Γ is a closed antichain state if and only if, for all nodes xs, py P Visited and every successor pq, P, νq P succ A e ˆBprrsssq of a configuration of the product automaton A e ˆB represented by the product state s, there exists a node xt, ry P Visited Y Next such that L pq,P,νq pA e ˆBq Ď L t pA e ˆBq and one of the following holds:

r " p.i for some i P N, i.e., xt, ry is a child of xs, py in the antichain T " Visited Y Next, or pxs, py, xt, ryq P Subsume.

In other words, the current antichain T , defined as the union of the sets Visited and Next, is in a closed state if the residual language of every successor of a configuration of the product automaton A e ˆB that is covered by a visited product state must be included in the residual language of a product state stored in the antichain, either as a direct successor in the tree or via a subsumption edge.

For a product state s, we define Distpsq " min |w| | w P L s pA e ˆBq ( , and Distpsq " 8 if and only if L s pA e ˆBq " H. For a finite non-empty set of antichain nodes S, we define DistpSq " min tDistpsq | xs, py P Su with DistpHq " 8.

We now prove several auxiliary lemmas.

Lemma 5 Given a network A and an observer B, for any product state s of A and B, we have succ A e ˆBprrsssq " Ť tPPostpsq rrtss.

Proof Let s " pq, P, Φq. "Ď" Let pr, S, µq P succ A e ˆBprrsssq be a configuration of A e ˆB for which there exists pq, P, νq P rrsss such that pq, P, νq σ,θ Ý Ñ pr, S, µq. Then there exists a unique rule pq, Pq σ,θ Ý Ñ pr, Sq P ∆ p such that pν, µq |ù θ. Moreover, if pq, P, νq P rrsss, we have ν |ù Φ. Let t " pr, S, Ψq P Postpsq where Ψpx A q " Dx 1 A . Φpx 1

A q ^θpx 1 A , x A q. We have µ |ù Ψ, hence pr, S, µq P rrtss. "Ě" Let pr, S, µq P rrtss for some t P Postpsq. Then we have t " pr, S, Ψq where that DistpVisited new q " Distpsq ă 8. Let w " pν 0 , σ 0 q, pν 1 , σ 1 q, . . . , pν n , ˛q P L s pA e Bq be a trace such that DistpVisited new q " n. Then there exists a run pq 0 , P 0 , ν 0 q

Ψpx A q " Dx 1 A . Φpx 1 A q ^θpx 1 A , x A q. Since µ |ù Ψ,
σ 0 Ý Ñ pq 1 , P 1 , ν 1 q σ 1 Ý Ñ . . . σ n´1
ÝÝÑ pq n , P n , ν n q of A e ˆB over w such that pq 0 , P 0 , ν 0 q P rrsss and pq n , P n q a final state of A e ˆB. Since Γ new is closed due to (Inv 1 ) and pq 1 , P 1 , ν 1 q P succ A e ˆBprrsssq, there exists a node xs 1 , p 1 y P Visited new Y Next new such that L pq1,P1,ν1q pA e ˆBq Ď L s1 pA e ˆBq. If xs 1 , p 1 y P Next new , we obtain that DistpNext new q ď n ´1, and we are done. Otherwise, xs 1 , p 1 y P Visited new , and we can repeat the same argument inductively, to discover a sequence of nodes xs 1 , p 1 y, . . . , xs n , p n y P Visited new such that L pqi,Pi,νiq pA e ˆBq Ď L sn pA e ˆBq for all i P r1, ns. Since pq n , P n q is a final state of A e ˆB, we have pν n , ˛q P L pqi,Pi,νiq pA e ˆBq, thus pν n , ˛q P L sn pA e ˆBq, and s n is an accepting product state. But this contradicts with the fact that accepting product states are never stored in the antichain.

[ \ With the above lemmas at hand, we can finally prove Theorem 1:

Proof If Algorithm 1 terminates and reports true, this is because Next " H, hence DistpNextq " 8. By Lemma 8 (Inv 2 ), we obtain that Distproot xA,By q " 8. Suppose, by contradiction, that LpAqÓ xB Ę LpBq. By Lemma 2, there exists a trace w " pν 0 , σ 0 qpν 1 , σ 1 q . . . pν n , ˛q P LpA e ˆBq.

Thus we have a run of A e ˆB over w:

pq 0 , P 0 , ν 0 q σ 0 Ý Ñ pq 1 , P 1 , ν 1 q σ 1 Ý Ñ . . . σ n´1
ÝÝÑ pq n , P n , ν n q where q 0 " xι 1 , . . . , ι N y, P 0 " tι B u, q n is final in A e , P n X F B " H. But, since pq 0 , P 0 , ν 0 q P rrroot xA,By ss, we have w P L root xA,By pA e ˆBq. Hence, Distproot xA,By q ď n, which is in contradiction with the fact that Distproot xA,By q " 8. Consequently, it must be the case that LpAqÓ xB Ď LpBq.

[ \

Simulations on Generic Register Automata

In the classical setting of finite state automata over finite alphabets, a simulation [START_REF] Milner | An algebraic definition of simulation between programs[END_REF] is a relation on the states of an automaton which is invariant with respect to its transition relation. The simulation-based approach to checking language inclusion between two automata A and B first computes a simulation relation on the union of the states of A and B, and then checks whether the pair of initial states is a member of the simulation relation. Note that this is not a complete decision procedure for language inclusion, because there exist automata such that LpAq Ď LpBq, but the initial state of A is not simulated by the initial state of B.

However, a pre-computed simulation relation can be used to speed up the convergence of the antichain-based method, by weakening (i.e. generalizing) the subsumption relation used by the antichain construction algorithm [START_REF] Abdulla | When simulation meets antichains[END_REF]. In practice, the experimental evaluation in [START_REF] Abdulla | When simulation meets antichains[END_REF] shows a significant improvement of running times, when simulations are used.

In the below subsection, we first introduce a concept of data simulations suitable for GRAs, together with an algorithm that computes useful under-approximations of the largest data simulation on a given GRA. In the next subsection, we then propose a way of using data simulations to enhance the convergence of Algorithm 1 between a GRAN and a GRA in a similar way as classical simulations are integrated with the antichain-based language inclusion algorithm for automata over finite alphabets [START_REF] Abdulla | When simulation meets antichains[END_REF].

We note that, in the context of classical automata, an approach going beyond the combination of antichains and simulation relations has been proposed [START_REF] Bonchi | Checking nfa equivalence with bisimulations up to congruence[END_REF]. It is based on using congruence relations instead of antichains. However, their usage in the context of generic register automata is so far unclear, and we leave it as an interesting subject for future work.

Data Simulations and Their Computation

Our notion of data simulations is defined as follows.

Definition 4 A relation R Ď QˆD x ˆQ is a data simulation for a GRA A " xΣ, D,x,Q,ι,F,∆y
if and only if the following holds for all pq, ν, q 1 q P R: 1. q P F ùñ q 1 P F, and 2. for all σ P Σ and all pr, ν 1 q P Q ˆDx such that pq, νq σ Ý Ñ A pr, ν 1 q there exists r 1 P Q such that pq 1 , νq σ Ý Ñ A pr 1 , ν 1 q and pr, ν 1 , r 1 q P R.

Observe that, while a classical simulation is a binary relation on states, a data simulation is a ternary relation that involves also a valuation of the variables. The following lemma shows that a data simulation preserves the residual languages of GRAs: Lemma 9 Given a GRA A " xΣ, D,x,Q,ι,F,∆y and a data simulation R Ď Q ˆDx ˆQ for A, we have L pq,νq pAq Ď L pq 1 ,νq pAq for any tuple pq, ν, q 1 q P R.

Proof Let pν 0 , σ 0 q, . . . , pν n , ˛q P L pq,νq pAq be a trace and pq, νq " pq 0 , ν 0 q σ 0 Ý Ñ . . .

σ n´1
ÝÝÑ pq n , ν n q be a run of A. By induction on n ě 0, it is easy to find a run pq 1 , νq " pq 1 0 , ν 0 q σ 0 Ý Ñ . . .

σ n´1
ÝÝÑ pq 1 n , ν n q of A such that, for all i P r0, ns, pq i , ν i , q 1 i q P R and moreover, q i P F ùñ q 1 i P F. Thus, pν 0 , σ 0 q, . . . , pν n , ˛q P L pq 1 ,νq pAq.

[ \ Let A " xΣ, D,x,Q,ι,F,∆y, where Q " tq 1 , . . . , q k u for some k ą 0, be a GRA for the rest of this section. The data simulation algorithm (Algorithm 2) given in this section manipulates sets of valuations from D x that are definable by first-order formulae in FormpDq. A relation R Ď QˆD x ˆQ is said to be definable if and only if there exists a matrix Φ " rφ i j s k i, j"1

Algorithm 2 Data Simulation Algorithm input: A generic register automaton A " xΣ, D,x,Q,ι,F,∆y, where Q " tq 1 , . . . , q k u, and a constant K ą 0.

output: A data simulation R Ď Q ˆDx ˆQ for A.
global vars rSim i j s k i, j"1 , rPrevSim i j s k i, j"1 , rCnt i j s k i, j"1

1: for i " 1, . . . , k do 2: for j " 1, . . . , k do 3:

PrevSim i j Ð J 4:

Cnt i j Ð K 5:

for j " 1, . . . , k do 6:

if q i P F and q j R F then 7:

Sim i j Ð K 8: else 9:

Sim i j Ð Ź σPΣ Ź q Ppost σ pq i q PreSim σ pi, j, , PrevSimq 10: while D P r1, ks such that Sim ı PrevSim do 11:

TempSim Ð Sim 12:

pick P r1, ks such that Sim ı PrevSim 13:

for σ P Σ do 14:

for q i P pre σ pq q do 15:

for j " 1, . . . , k do 16:

Sim i j Ð Sim i j ^PreSim σ pi, j, , Simq 17:
for all j " 1, . . . , k such that Sim j ı PrevSim j do 18:

if Cnt j " 0 then 19:

Sim j Ð K 20: else 21:

Cnt j Ð Cnt j ´1 22:

PrevSim Ð TempSim 23: return Sim of formulae φ i j pxq P FormpDq such that pq i , ν, q j q P R ðñ ν |ù φ i j . For P r1, ks, we denote by Φ the -th row of the matrix Φ.

Algorithm 2 is a refinement algorithm which handles two matrices of formulae that define the relations Sim, PrevSim Ď Q ˆDx ˆQ. Below, we shall use the same names to denote the relations and their matrix representations. Intuitively, PrevSim is the previous candidate for simulation, whereas Sim is an entry-wise stronger relation that refines PrevSim. The refinement step is performed backwards wrt each transition rule q i σ,φ Ý Ñ q of the automaton as follows. The tuple pq i , ν, q j q is added to the newly created relation Sim if pq i , ν, q j q P PrevSim and there exist a valuation ν 1 , a state q m P Q, and a formula ψ such that pν, ν 1 q |ù φ, q j σ,ψ Ý Ñ q m , pq , ν 1 , q m q P PrevSim, and pν, ν 1 q |ù ψ. This update guarantees that, for every transition pq i , νq σ Ý Ñ A pq , ν 1 q where pq i , ν, q j q P Sim, there exists a state q m such that pq j , νq σ Ý Ñ A pq m , ν 1 q and pq , ν 1 , q m q P PrevSim. The algorithm stops when Sim and PrevSim define the same relation. Moreover, this relation is guaranteed to be a data simulation.

To define the update, we use the following function, where σ P Σ is an input event, i, j, P r1, ks are state indices such that q i σ,φ Ý Ñ q j P ∆ is a transition rule and R is k ˆk matrix of formulae:

PreSim σ pi, j, , Rq " @x 1 . φpx, x 1 q Ñ ł q j σ,ψ Ý Ñqm ψpx, x 1 q ^R m px 1 q .
We also define the sets post σ pqq " tq 1 | q σ,φ Ý Ñ q 1 P ∆u and pre σ pqq " tq 1 | q 1 σ,φ Ý Ñ q P ∆u. With this notation, Algorithm 2 describes the procedure that computes a data simulation for a given data automaton.

Initially, the matrix PrevSim is true everywhere (line 3). The current simulation candidate Sim is initialized to false for all i, j P r1, ks such that q i P F and q j R F (line 7). Observe that, in this case, q j cannot simulate q i , by Definition 4 (1). Otherwise, we initialize Sim i j to the strongest pre-simulation with respect to PrevSim (line 9). In the iterative loop (lines 10-22), the algorithm chooses a state q for which the current simulation candidate Sim is not equivalent to the previous one PrevSim (line 13) and sharpens the set Sim i j with respect to the transition rule q i σ,φ Ý Ñ q for all input symbols σ P Σ and all peer states q j , j P r1, ks (line 16). The following invariants are key to proving the correctness of Algorithm 2.

Lemma 10

The following invariants hold each time Algorithm 2 reaches line 10:

-(SimInv 1 ) for all i, j P r1, ks, the entailment Sim i j Ñ PrevSim i j is valid.

-(SimInv 2 ) for all σ P Σ, all i, j, P r1, ks and all ν, ν 1 P D x , if ν |ù Sim i j and pq i , νq σ Ý Ñ pq , ν 1 q then there exists m P r1, ks such that pq j , νq σ Ý Ñ pq m , ν 1 q and ν 1 |ù PrevSim m .

Proof Let Sim 1 and PrevSim 1 denote the global matrices after one iteration of the loop on lines 10-22.

(SimInv 1 ) When line 10 is reached for the first time, PrevSim i j " J for all i, j P r1, ks, thus SimInv 1 holds initially. Since Sim is modified on lines 16 or 19 only, we have Sim 1 i j Ñ Sim i j for all i, j P r1, ks. Moreover, for each i, j P r1, ks either (i) PrevSim 1 i j " TempSim i j " Sim i j (line 22) and Sim 1 i j Ñ Sim i j Ñ PrevSim 1 i j holds, or (ii) PrevSim 1 i j " PrevSim i j (no update) and Sim 1 i j Ñ Sim i j Ñ PrevSim i j Ñ PrevSim 1 i j holds, by the inductive hypothesis.

(SimInv 2 ) We show that this invariant holds the first time the control reaches line 10. Let σ P Σ, i, j, P r1, ks and ν, ν 1 P D x such that ν |ù Sim i j and pq i , νq σ Ý Ñ pq , ν 1 q. Since ν |ù Sim i j (thus Sim i j ‰ K) and q P post σ pq i q, we have that ν |ù PreSim σ pi, j, , PrevSimq where q i σ,φ Ý Ñ q P ∆. Since pq i , νq σ Ý Ñ pq , ν 1 q, we obtain that pν, ν 1 q |ù φpx, x 1 q, and, consequently, pν, ν 1 q |ù ψpx, x 1 q^PrevSim m px 1 q for some m P r1, ks such that q j σ,ψ Ý Ñ q m P ∆. Hence, SimInv 2 holds when the control first reaches line 10.

For the induction step, let us assume that SimInv 2 holds on line 10, and we prove that it also holds after executing line 22. Let σ P Σ, i, j, P r1, ks and ν, ν 1 P D x such that ν |ù Sim 1 i j and pq i , νq σ Ý Ñ pq , ν 1 q. We distinguish two cases: 1. If Sim ı PrevSim on line 10 since q i P pre σ pq q, then Sim 1 i j was updated on line 16. Since ν |ù Sim 1 i j , we obtain ν |ù PreSim σ pq i , q j , q , Simq. Moreover, PrevSim 1 is updated to TempSim " Sim on line 22, hence ν |ù PreSim σ pq i , q j , q , PrevSim 1 q as well. Since pq i , νq σ Ý Ñ pq , ν 1 q, we obtain that pν, ν 1 q |ù ψpx, x 1 q ^PrevSim 1 m px 1 q for some m P r1, ks such that q j σ,ψ Ý Ñ q m P ∆, thus pν, ν 1 q |ù ψpx, x 1 q and ν 1 |ù PrevSim 1 m . Thus SimInv 2 holds for Sim 1 and PrevSim 1 . 2. Otherwise Sim " PrevSim on line 10. Moreover, PrevSim 1 " PrevSim because the update on line 22 is skipped, and, for all q i P pre σ pq q and all j P r1, ks, we have Sim 1 i j " Sim i j . Then, by the induction hypothesis, SimInv 2 holds for Sim 1 and PrevSim 1 because it holds for Sim and PrevSim.

[ \

The algorithm iterates the loop on lines [START_REF] Cook | On automation of ctl* verification for infinite-state systems[END_REF][START_REF] Craig | Three uses of the herbrand-gentzen theorem in relating model theory and proof theory[END_REF][START_REF] D'antoni | Symbolic visibly pushdown automata[END_REF][START_REF] Decker | Ordered navigation on multi-attributed data words[END_REF][START_REF] Dhar | Algorithms for model-checking flat counter systems[END_REF][START_REF] Fribourg | A closed-form evaluation for extended timed automata[END_REF][START_REF] Grebenshchikov | Synthesizing software verifiers from proof rules[END_REF][START_REF] Habermehl | A logic of singly indexed arrays[END_REF][START_REF] Habermehl | What else is decidable about integer arrays? In[END_REF][START_REF] Henzinger | Lazy abstraction[END_REF][START_REF] Henzinger | Software Verification with Blast[END_REF][START_REF] Henzinger | Symbolic model checking for real-time systems[END_REF][START_REF] Iosif | Abstraction refinement and antichains for trace inclusion of infinite state systems[END_REF] until Sim and PrevSim define the same relation. Since, in general, the data constraints Sim i j obtained from different iteration steps might form an infinitely decreasing sequence, we use the matrix Cnt of integer counters, initially set to some input value K ą 0 (line 4). 12 Observe that each entry Cnt i j decreases every time Sim i j ı PrevSim i j (line 21). When the counter Cnt i j reaches zero, we set Sim i j to false (line 19), which guarantees that Sim i j " PrevSim i j always in the future. Since the number of entries in the counter matrix is finite, the algorithm is guaranteed to terminate. The following theorem summarizes the main result of this section.

Theorem 2 Algorithm 2 terminates on any GRA A " xΣ, D,x,Q,ι,F,∆y, and its output is a data simulation R Ď Q ˆDx ˆQ for A.

Proof Let Sim n and PrevSim n denote the matrices Sim and PrevSim at the n-th iteration of the loop on lines 10-22, for n ě 0. Algorithm 2 terminates whenever Sim n i j " PrevSim n i j for all i, j P r1, ks (line 10). Suppose, by contradiction, that this never happens, thus there exist i, j P r1, ks such that Sim n i j ı PrevSim n i j for all n ě 0. Then Cnt K i j " 0 (line 21) and Sim K`1 i j

"

PrevSim K`2 i j " K (lines 19 and 22). Since Sim n i j Ñ PrevSim n i j , by Lemma 10 (SimInv 1 ), we obtain that Sim K`2 i j " PrevSim K`2 i j , a contradiction. To prove that the output of Algorithm 2 is a data simulation for A, we use Lemma 10 (SimInv 2 ) and the fact that, upon termination, we have Sim i j " PrevSim i j , for all i, j P r1, ks.

[ \

Simulation and Subsumption

Finally, we explain how a data simulation relation computed by Algorithm 2 can be used to optimize the trace inclusion semi-algorithm. Let A " xA 1 , . . . , A N y be a GRAN where A i " xD, Σ i , x i , Q i , ι i , F i , ∆ i y for all i P r1, Ns, and let

B " xD, Σ, x B , Q B , ι B , F B , ∆ B y be an observer GRA such that x B Ď Ť N i"1 x i .
The main problem for using data simulations to enhance the convergence of our trace inclusion semi-algorithm is related to the fact that simulation relations are, in general, not compositional wrt the interleaving semantics of the network. In other words, if we have N data simulations R i Ď Q i ˆDxi ˆQi for i P r1, Ns, then their cross-product R Ď Q A ˆDx A QA defined as:

@q 1 , r 1 P Q 1 . . . @q N , r N P Q N @ν P D x A : pxq 1 , . . . , q N y, ν, xr 1 , . . . , r N yq P R ðñ pq i , νÓ xi , r i q P R i

is not necessarily a simulation on the network expansion A e . The reason for this can be seen for N " 2. Let σ 1 , σ 2 P Σ A such that σ 1 R Σ 2 and σ 2 R Σ 1 . The execution of A e on the sequence of input symbols σ 1 σ 2 is pxq 1 , q 2 y, νq σ 1

Ý Ñ pxq 1 1 , q 2 y, ν 1 q σ 2 Ý Ñ pxq 1 1 , q 1 2 y, ν 2 q. Suppose that pq i , νÓ xi , r i q P R i , for all i " 1, 2. Then there exists r 1 1 P Q 1 such that pxr 1 , r 2 y, νq σ 1

Ý Ñ pxr 1 1 , r 2 y, ν 1 q and pq 1 1 , ν 1 Ó x1 , r 1 1 q P R 1 . In order to use the simulation and build the continuation

pxr 1 1 , r 2 y, ν 1 q σ 2 Ý Ñ pxr 1
1 , r 1 2 y, ν 2 q, we would need that pq 2 , ν 1 Ó x2 , r 2 q P R 2 , which is not necessarily ensured by the hypothesis pq 2 , νÓ x2 , r 2 q P R 2 .

We propose a partial solution to this problem, based on a restriction concerning the distribution of the network variables x A " Ť N i"1 x i over the components A 1 , . . . , A N : for each i P r1, Ns, we have x i " x g Y x i where x g is a set of global variables and x i are the local variables of A i . In other words, the only variables shared between more than one component are the global variables x g , which, moreover, are visible to all components. 13 Then the problem can be bypassed if none of the simulation relations R i Ď Q i ˆDxi ˆQi may constrain the global variables: Assumption 3 For each i P r1, Ns and each pq i , ν, r i q P R i , we also have pq i , ν 1 , r i q P R i for each ν 1 P D xi such that νÓ x i " ν 1 Ó x i .

Under this assumption, we use pre-computed data simulations R i Ď Q i ˆDx g ˆQi and R B Ď Q B ˆDxB ˆQB to generalize the basic subsumption relation between product states (defined by Lemma 4), which may speed up the convergence of Algorithm 1.

Lemma 11 Under Assumption 3, the relation defined as pxq 1 , . . . , q N y, P, Φq Ď sim pxr 1 , . . . , r N y, S, Ψq ðñ @i P r1, Ns @ν P D xA : ν |ù Φ ùñ ν |ù Ψ and " pq i , νÓ xi , r i q P R i p1q @s P S Dp P P : ps, νÓ xB , pq P R B p2q is a subsumption relation.

Proof Let s " pxq 1 , . . . , q N y, P, Φq and t " pxr 1 , . . . , r N y, S, Ψq be two product states such that s Ď sim t. According to Definition 3, we need to prove that L s pA e ˆBq Ď L t pA e ˆBq. For that, it is sufficient to prove that, for each ν P D x A such that ν |ù Φ, the following two points hold: 1. L pxq1,...,qN y,νq pA e q Ď L pxr1,...,rN y,νq pA e q, and 2. for all p P S there exists q P P such that L pp,νÓ x B q pBq Ď L pq,νÓ x B q pBq. Indeed, assuming that the above statements hold, we have L s pA e ˆBq " Ť ν|ùΦ ´Lpxq1,...,qNy,νq pA e q X Ş qPP L pq,νÓ x B q pBq Ď Ť ν|ùΦ ´Lpxr1,...,rNy,νq pA e q X Ş rPS L pr,νÓ x B q pBq Ď Ť ν|ùΨ ´Lpxr1,...,rNy,νq pA e q X Ş rPS L pr,νÓ x B q pBq " L t pA e ˆBq, and we are done. Moreover, the second point above is a direct consequence of the second point of the definition of Ď sim and Lemma 9. We are left with proving the first point.

To prove the first point, assume that we are given configurations pxq 1 0 , . . . , q N 0 y, ν 0 q and pxr 1 0 , . . . , r N 0 y, ν 0 q of A e such that @i P r1, Ns : pq i 0 , ν 0 Ó xi , r i 0 q P R i . We show that if there is a run pxq 1 0 , . . . , q N 0 y, ν 0 q σ 0 Ý Ñ . . .

σ n´1
ÝÝÑ pxq 1 n , . . . , q N n y, ν n q for any n ě 0, then there is some run

pxr 1 0 , . . . , r N 0 y, ν 0 q σ 0 Ý Ñ . . . σ n´1
ÝÝÑ pxr 1 n , . . . , r N n y, ν n q where @i P r1, Ns : @ j P r0, ns : pq i j , ν j Ó xi , r i j q P R i ^pq i j P F i ùñ r i j P F i q, by induction on the length n of the run. The base case for n " 0 follows trivially from the assumption @i P r1, Ns : pq i 0 , ν 0 Ó xi , r i 0 q P R i and from the first point of the definition of data simulations (Def. 4). Now, assuming that the property holds for runs of length n, we show that it holds for runs of length n `1 too. Take a run pxq 1 0 , . . . , q N 0 y, ν 0 q σ 0 Ý Ñ . . .

σ n´1
ÝÝÑ pxq 1 n , . . . , q N n y, ν n q σn Ý Ñ pxq 1 n`1 , . . . , q N n`1 y, ν n`1 q. Further, take a configuration pxr 1 0 , . . . , r N 0 y, ν 0 q such that @i P r1, Ns : pq i 0 , ν 0 Ó xi , r i 0 q P R i . From the induction hypothesis, we immediately get that there exists a run pxr 1 0 , . . . , r N 0 y, ν 0 q σ 0 Ý Ñ . . .

σ n´1
ÝÝÑ pxr 1 n , . . . , r N n y, ν n q where @i P r1, Ns : @ j P r0, ns : pq i j , ν j Ó xi , r i j q P R i ^pq i j P F i ùñ r i j P F i q. Next, let I Ď r0, Ns be the set of indices of the GRAs that make a move during the step pxq 1 n , . . . , q N n y, ν n q σn Ý Ñ pxq 1 n`1 , . . . , q N n`1 y, ν n`1 q. For any i P I, from pq i n , ν n Ó xi , r i n q P R i and pq i n , ν n Ó xi q σn Ý Ñ pq i n`1 , ν n`1 Ó xi q, we get there there is some r

i n`1 such that pr i n , ν n Ó xi q σn Ý Ñ pr i n`1 , ν n`1 Ó xi q, pq i n`1 , ν n`1 Ó xi , r i
n`1 q P R i , and q i n`1 P F i Ñ r i n`1 P F i . Moreover, for any i P r1, NszI, the fact that ν n Ó x l i " ν n`1 Ó x l i , pq i n , ν n Ó xi , r i n q P R i , q i n`1 " q i n , r i n`1 " r i n , and Assumption 3, give us pq i n`1 , ν n`1 Ó xi , r i n`1 q P R i , and, consequently, q i n`1 P F i Ñ r i n`1 P F i too.

[ \

Experimental Results

We have implemented both Algorithm 1 (trace inclusion) and Algorithm 2 (data simulations) in a prototype tool INCLUDER14 using the MATHSAT SMT solver [START_REF] Cimatti | The MathSAT5 SMT Solver[END_REF] for answering the satisfiability queries and computing the interpolants. The results of the experiments with trace inclusion are given in Tables 1 and2. The results of experiments combining trace inclusion and simulations are given in Table 3. The results were obtained on an Intel i7-4770 CPU @ 3.40GHz machine with 32GB RAM.

Trace Inclusion

Table 1 contains experiments where the network A consists of a single component. We applied the tool on several verification conditions generated from imperative programs with arrays [START_REF] Bozga | Automatic verification of integer array programs[END_REF] (Array shift, Array rotation 1+2, Array split) available online [START_REF]Numerical Transition Systems Repository[END_REF]. Then, we applied it on models of hardware circuits (HW Counter 1+2, Synchronous LIFO) [START_REF] Smrcka | Verifying parametrised hardware designs via counter automata[END_REF]. Finally, we checked two versions (correct and faulty) of the timed Alternating Bit Protocol [34].

Table 2 provides a list of experiments where the network A has N ą 1 components.

First, we have the example of Fig. For the time being, our implementation is a proof-of-concept prototype that leaves plenty of room for optimization (e.g., caching of intermediate computation results) likely to improve the performance on more complicated examples. Despite that, we found the results from Tables 1 and 2 rather encouraging.

Combination of Trace Inclusion and Simulations

Unlike the computation of the most general simulation on a finite-alphabet automaton, which is possible in polynomial time [?], computing the weakest data simulation on a GRA is, in general, impossible due to the fact that the data constraints cannot be represented in a decidable logical domain, such as linear integer arithmetic. For this reason, our algorithm (Algorithm 2) is sound but incomplete, returning a possibly stronger simulation, in which the data constraint associated with certain pairs of states is set of K. Such simulations can be computed in reasonable time, but they could be of limited use in speeding up the antichainbased trace inclusion check.

Our implementation tries to achieve a balance between these opponent goals, as shown by the results in Table 3. We apply a timeout on each single call of the PreSim function in Algorithm 2. Moreover, we may also limit the size of the resulting formula 15 for a single call of the PreSim function. If the timeout or the size limit is exceeded, the result of PreSim will be safely underapproximated to K (i.e., no simulation).

The use of simulation-based subsumption has an impact on running times of the trace inclusion in the examples, where the system contains a nontrivial simulation relation, which could be discovered by Algorithm 2 at most K " 2 iterations on each pair of states and, moreover, some product states in the antichain tree are compatible with this simulation relation. This is clearly visible in the Fischer 2-serial and Fischer 2-branching models where the synchronization based on the Fischer protocol is used in non-minimalistic scenarios, i.e., scenarios not restricted to a single critical section. In particular, Fischer 2-serial is an abstract model of a system where a process uses the Fischer protocol to access a critical section twice in a row. Fischer 2-branching is an abstraction of a system where a single process contains two branches and each of these branches accesses a critical section using the Fischer's protocol. The parameters ∆ and Γ are parameters of the Fischer's protocol, and N is the number of parallel processes. Note that if the system contains a counterexample (e.g. Fischer 2-serial with parameters ∆ " 2, Γ " 1, N " 3), the simulation-based subsumption may also increase the running time. The reason is that the computation is stopped when an accepting product state is discovered and the rest of the antichain tree is not constructed. The simulation-based subsumption makes the whole antichain tree smaller (in terms of nodes), but the shortest counterexample path may be subsumed by a longer one resulting to a postpone of a counterexample discovery. Also note that we managed to compute nontrivial simulations 16 for all the examples from Tables 1 and2. However, in most of them, the use of the simulation has no impact on the time of checking the trace inclusion. The main reason is that most of the protocols are modeled by automata where very limited data simulations exist between pairs of states (i.e., the data constraints under which the simulation holds are quite strong), and product states in the antichain tree are incompatible with these simulations (cf. Points 1 and 2 of Lemma 11).

Conclusions

We have presented an interpolation-based abstraction refinement method for trace inclusion between a network of generic register automata and an observer where the variables used by the observer are a subset of those used by the network. The procedure builds on a new determinization result for GRAs and combines in a novel way predicate abstraction and interpolation with antichain-based inclusion checking. The efficiency of the basic method can be further enhanced by data simulations. The procedure has been successfully applied to several examples, including verification problems for array programs, real-time systems, and hardware designs.

For the future, it is interesting to extend the method to data tree automata and apply it to logics for heaps with data. Also, we foresee an extension of the method to handle infinite traces. Finally, it is also an open problem how to handle the case when the observer is allowed to have local variables. A Alternative Notions of the Product State Below, we briefly discuss two alternative notions of product states that we originally considered but dropped them since we were not able to build a sound antichain construction on them.

The first option we considered was to link predicates with the individual states involved in a product state. In that case, the predicate map linked particular states of automata A e and B to sets of formulas as follows: Π ind : Q A e Y Q B Ñ 2 FormpDq . The product state was then defined as s ind " pxq, Φ q y, Pq with q being a state of the automaton A e , Φ q Ď Π ind pqq, and P Ď txr, Φ r y | r P Q B and Φ r Ď Π ind prqu. The semantics of the product state s ind " pxq, Φ q y, Pq was that whenever the automaton A e is in the state q with a valuation ν |ù Φ q of the variables, then the automaton B can be in any state r such that xr, Φ r y P P and ν |ù Φ r . A product state s ind " pxq, Φ q y, Pq was considered accepting iff q P F A e and there existed ν |ù Φ q such that ν |ù Ž tΦ r | xr, Φ r y P P ^r P F B u. That implied existence of a trace accepted by A e at the state q with the final valuation ν, not covered by the automaton B. A problem with this product construction is that it cannot be used for soundly deciding the inclusion problem as shown in the following example: Take the product state s 1 " pxq 1 , x P t1, 2uy, txr 1 , x " 1y, xr 2 , x " 2yuq obtained for an automaton A e with the rule q 1 σ,x 1 "x`1

Ý ÝÝÝÝ Ñ q 2 and an automaton B with rules r 1 σ,x 1 ąx Ý ÝÝ Ñ r 3 and r 2 σ,x 1 "x`1^xą10 ÝÝÝÝÝÝÝÝÑ r 3 . Moreover, let q 2 be final in A e and r 3 be final in B. When one computes the post of s 1 , one gets s 2 " pxq 2 , x P t2, 3uy, txr 3 , x ą 1yuq, which is not accepting, because all configurations of A e are covered by configurations of B. However, the automaton A e can do a step pq 1 , x " 2q σ,x 1 "x`1

Ý ÝÝÝÝ Ñ pq 2 , x " 3q, which cannot be followed by B. Hence, an antichain construction based on this notion of product states could hide a real counterexample and provide an unsound answer.

In order to avoid the unsoundness of the above solution, we attempted to use predicates representing relations between successive values of variables within a step leading to a given product state. In this case, the predicate map was defined as Π rel : Q A e Y Q B Ñ 2 FormpDq ˆ2FormpDq . The product state was then defined as s rel " pxq, Φ q y, Pq with q being a state of the automaton A e , Φ q Ď Π rel pqq, and P Ď txr, Φ r y | r P Q B and Φ r Ď Π rel prqu. The semantics of the product state s rel " pxq, Φ q y, Pq was that whenever the last step of A e was p , νq Ý Ñ pq, ν 1 q such that pν, ν 1 q |ù Φ r , then the last step of B could have been p , νq Ý Ñ pr, ν 1 q where xr, Φ r y P P and pν, ν 1 q |ù Φ r . (The source states of the steps were not reflected in the product states, and hence are represented using the underscore sign.) A product state was considered final iff q P F A e and there existed a relation pν, ν 1 q |ù Φ r such that pν, ν 1 q |ù Ž tΦ r | xs, Φ r y ^r P F B u. The antichain tree could be used for sound checking of the inclusion in this case. However, a problem was to find a subsumption relation to soundly prune the antichain tree. A natural way of defining the subsumption relation following the approach of [START_REF] Abdulla | When simulation meets antichains[END_REF] is to define the subsumption as follows: pxq 1 , Φ 1 y, P 1 q Ď pxq 2 , Φ 2 y, P 2 q iff (i) q 1 " q 2 , (ii) Φ 1 Ñ Φ 2 , and (iii) for each xr, Φ r y P P 2 there exists xs, Φ s y P P 1 such that r " s and Φ r Ñ Φ s . Unfortunately, it turns out that using such a subsumption cannot be used for sound inclusion checking since comparing formulae representing solely the last step of the automata can lead to omitting counterexamples to inclusion that depend on longer traces. Existence of a suitable sound subsumption for this type of product states, which is needed to ensure termination of the antichain construction, is an open problem.

  the tree positions or alphabet symbols are not important.

28 :

 28 add pn, succq to Subsume29:remove rem from pVisited, Next, Subsumeq

Example 6

 6 In the antichain from Fig.2 (d), pxq1

1

  terminates and returns true on input A and B, then LpAqÓ xB Ď LpBq.

  32. Tripakis, S.: The analysis of timed systems in practice. Ph.D. thesis, Univ. Joseph Fourier, Grenoble (December 1998) 33. Wulf, M.D., Doyen, L., Henzinger, T.A., Raskin, J.: Antichains: A new algorithm for checking universality of finite automata. In: Proc. of CAV'06, LNCS, vol. 4144. Springer (2006) 34. Zbrzezny, A., Polrola, A.: Sat-based reachability checking for timed automata with discrete data. Fundamenta Informaticae 79, 1-15 (2007)

  Then LpAqÓ xB Ď LpBq if and only if LpA ˆBq " H. Proof We have LpAqÓ xB Ď LpBq iff LpAq Ó xB XLpBq " LpA ˆBqÓ xB " H iff LpA ˆBq " H.

	[ \

  Definition 1 Formally, an antichain T is a set of pairs xs, py, where s is a product state and p P N ˚is a tree position, such that (1) for each position p P N ˚there exists at most one product state s such that xs, py P T , (2) the set tp | xs, py P T u is prefix-closed, (3) proot xA,By , εq P T where root xA,By " pxι 1 , . . . , ι N y, tι B u, Jq is the label of the root, and (4) for each edge pxs, py, xt, p.iyq in T , there exists a predicate map Π such that t P Post Π psq. For the latter condition, if s " pq, P, Φq and t " pr, S, Ψq, there exists a unique rule pq, Pq Sq P ∆ p , and we shall sometimes denote the edge as s

	σ,θ Ý Ñ pr,

  1 x i . True if LpAqÓ x B Ď LpBq, otherwise a trace τ P LpAq Ó x B zLpBq. 1: Π Ð H, Visited Ð H, Next Ð xroot xA,By , εy, Subsume Ð H 2: while Next ‰ H do 3: choose curr P Next and move curr from Next to Visited if there exists m " xt 1 , p 1 y P Visited such that t Ď t 1 then

	4:	match curr with xs, py
	5:	if s is an accepting product state then
	6:	let ρ be the path from the root to curr and k be the pivot of ρ
	7:	if k ě 0 then
	8:	Π Ð REFINEPREDICATEMAPBYINTERPOLATIONpΠ, ρ, kq
	9:	rem Ð SUBTREEpρ k q
	10:	for pn, mq P Subsume such that m P rem do
	11:	move n from Visited to Next
	12:	remove rem from pVisited, Next, Subsumeq
	13:	add ρ k to Next
	14:	else
	15:	return EXTRACTCOUNTEREXAMPLEpρq
	16:	else
	17:	i Ð 0
	18:	for t P Post Π psq do
	19:
	20:	add pcurr, mq to Subsume
	21:

output: else 22: rem Ð tn P Next | n " xt 1 , p 1 y and t 1 < tu 23: succ Ð xt, p.iy

  Ψq P Postpsq. By the definition of Post Π , we have t 1 " pr, S, Ψ 7 q P Post Π psq, where Ψ Ñ Ψ 7 , thus rrtss Ď rrt 1 ss. Given a network A, an observer B, and a predicate map Π, for each product state s and each configuration pq, P, νq P succ A e ˆBprrsssq there exists a product state t P Post Π psq such that pq, P, νq P rrtss.(a) xs, py " curr. In this case, either (i) there is xt 1 , p 1 y P Visited old such that t Ď t 1 , and then we also have L pq,P,νq pA e ˆBq Ď L t 1 pA e ˆBq (Definition 3) and pxs, py, xt 1 , p 1 yq P Subsume new (added on line 20), or (ii) pt, p.iq P Next new for some i P N (added on lines 23 and 30). (b) Otherwise xs, py P Visited old . As Γ 1 is closed, there is xu, ry P Visited old Y Next old such that L pq,P,νq pA e ˆBq Ď L u pA e ˆBq and either r " p.i for some i P N or pxs, py, xu, ryq P Subsume old . We distinguish two sub-cases: (i) xu, ry P rem (line 22). Then L u pA e ˆBq Ď L t pA e ˆBq (Definition 3), hence L pq,P,νq pA e ˆBq Ď L t pA e ˆBq. If r " p.i, then pxs, py, xt, r 1 yq P Subsume new for some r 1 P N ˚(added on line Else, if pxs, py, xu, ryq P Subsume old , we have pxs, py, xt, r 1 yq P Subsume new for some r 1 P N ˚(added on line 28). In both cases, we obtain that Γ new is closed. (ii) xu, ry R rem. Then xu, ry P Visited new Y Next new . Since Subsume new " Subsume old X pVisited new ˆpVisited new Y Next new qq, we obtain that Γ new is closed. (Inv 2 ) We distinguish two cases: 1. If DistpVisited new q " 8, it is sufficient to show that DistpNext new q ă 8. Suppose, by contradiction, that DistpNext new q " 8, hence DistpVisited new Y Next new q " 8, and since root xA,By P Visited new Y Next new , we obtain Distproot xA,By q " 8, contradiction. 2. Otherwise, DistpVisited new q ă 8 and there exists a node xs, py P Visited new such

	[ \
	Lemma 7

there exists ν |ù Φ such that pq, P, νq σ,θ Ý Ñ pr, S, µq. Hence pq, P, νq P rrsss, thus pr, S, µq P succ A e ˆBprrsssq.

[ \ Lemma 6 Given a network A, an observer B, and a predicate map Π, for any product state s of A e ˆB and any product state t P Postpsq, there exists t 1 P Post Π psq such that rrtss Ď rrt 1 ss.

Proof Let t " pr, S,

Table 1

 1 Experiments with single-component networks.

	Example	A (|Q|/|∆|)	B (|Q|/|∆|)	Vars.	Res.	Time
	Arrays shift	3/3	3/4	5	ok	ă 0.1s
	Array rotation 1	4/5	4/5	7	ok	0.1s
	Array rotation 2	8/21	6/24	11	ok	34s
	Array split	20/103	6/26	14	ok	4m32s
	HW counter 1	2/3	1/2	2	ok	0.2s
	HW counter 2	6/12	1/2	2	ok	0.4s
	Synchr. LIFO	4/34	2/15	4	ok	2.5s
	ABP-error	14/20	2/6	14	cex	2s
	ABP-correct	14/20	2/6	14	ok	3s

Table 2

 2 Experiments with multiple-component networks (e.g., 2 ˆ2{2 `2 ˆ3{3 in column A means that A is a network with 4 components that includes 2 GRAs with 2 states and 2 rules and 2 GRAs with 3 states and 3 rules).

	Example	N	A (|Q|/|∆|)	B (|Q|/|∆|)	Vars.	Res.	Time
	Running	2	2ˆ2/2	3/4	3	ok	0.2s
	Running	10	10ˆ2/2	11/20	3	ok	25s
	Train (T " 5)	7	5ˆ3/3 + 4/4 + 4/4	2/38	1	ok	4s
	Train (T " 10)	12	10ˆ3/3 + 4/4 + 4/4	2/68	1	ok	29s
	Train (T " 20)	22	20ˆ3/3 + 4/4 + 4/4	2/128	1	ok	6m26s
	Fischer (∆ " 1, Γ " 2)	2	2ˆ5/6	1/10	4	ok	8s
	Fischer (∆ " 1, Γ " 2)	3	3ˆ5/6	1/15	4	ok	2m48s
	Fischer (∆ " 2, Γ " 1)	2	2ˆ5/6	1/10	4	cex	3s
	Fischer (∆ " 2, Γ " 1)	3	3ˆ5/6	1/15	4	cex	32s
	Stari (K " 1)	5	4/5 + 2/4 + 5/7 + 5/7 + 5/7	3/6	3	ok	0.5s
	Stari (K " 2)	8	4/5 + 2/4 + 2ˆ5/7 + 2ˆ5/7 + 2ˆ5/7	3/6	3	ok	0.5s
	Prod-Cons (B " 3)	2	4/4 + 4/4	2/7	2	ok	10s
	Prod-Cons (B " 6)	2	4/4 + 4/4	2/7	2	ok	2m32s
	Array init (∆ " 2)	5	5ˆ2/2	2/6	2	ok	3s
	Array init (∆ " 2)	15	15ˆ2/2	2/16	2	ok	3m15s
	Array copy (∆ " 20)	20	20ˆ2/2	2/21	3	ok	0.3s
	Array copy (∆ " 20)	150	150ˆ2/2	2/151	3	ok	43s
	Array join (∆ " 10)	4	2ˆ2/2 + 2ˆ3/3	2/3	2	ok	6s
	Array join (∆ " 10)	6	3ˆ2/2 + 3ˆ3/3	2/4	2	ok	23s
	Array join (∆ " 20)	6	3ˆ2/2 + 3ˆ3/3	2/4	2	ok	1m9s

Table 3

 3 Experiments with simulations. Time nosim inclusion represents the time of checking trace inclusion without using simulation, Time sim inclusion represents the time of checking trace inclusion while using simulation-based subsumption, and Time sim represents the time needed to compute data simulations. K is the parameter of Algorithm 2, Max size is a limit on the size of the result of the PreSim function, and TO is a timeout on a single call of the PreSim function.

	Example	Time nosim inclusion	Time sim inclusion	Time sim	K	Max size	TO
	Array rotation 2	27s	24s	38s	2	15	2s
	Array rotation 2	27s	24s	24s	2	15	1s
	Array Split	3m23s	2m37s	5m52s	2	15	2s
	Array Split	3m23s	2m37s	4m1s	2	15	1s
	Fischer 2-serial (∆ " 1, Γ " 2, N " 3)	17m43s	3m55s	2s	2	8	8
	Fischer 2-serial (∆ " 1, Γ " 2, N " 2)	27s	9s	2s	2	8	8
	Fischer 2-serial (∆ " 2, Γ " 1, N " 3) (cex)	50s	1m	2s	2	8	8
	Fischer 2-serial (∆ " 2, Γ " 1, N " 2) (cex)	3s	2s	2s	2	8	8
	Fischer 2-branch (∆ " 1, Γ " 2, N " 3)	25m57s	4m28s	2s	2	8	8
	Fischer 2-branch (∆ " 1, Γ " 2, N " 2)	24s	11s	2s	2	8	8
	Fischer 2-branch (∆ " 2, Γ " 1, N " 3) (cex)	1m49s	1m8s	2s	2	8	8
	Fischer 2-branch (∆ " 2, Γ " 1, N " 2) (cex)	10s	3s	2s	2	8	8

http://www.fit.vutbr.cz/research/groups/verifit/tools/includer/

Note that there is not a fixed set of predefined predicates. New predicates are discovered during refinement phase.

Our reduction to the emptiness of product automata is at least exponential.

For (in)finite words, the class of LTL-definable languages coincides with the star-free languages, which are a strict subclass of (ω-)regular languages.

Called data automata in[START_REF] Iosif | Abstraction refinement and antichains for trace inclusion of infinite state systems[END_REF].

Note that the empty disjunction is equivalent to K. Hence θpx, x 1 q satisfiable implies that for all p 1 P P 1 there exists p P P and a rule p σ,ψ Ý Ñ p 1 P ∆.

For timed automata, this is the case since the only shared variable is the time, and the observer may have local clocks.

The formal definition of antichain trees will be given as Definition 1 later in this section.

Note that the above choice of the product state in the form s " pq, P, Φq is not straightforward and resulted from several previous unsuccessful attempts. For example, if one chooses to associate separate formulae for the valuations of the variables with q and each of the states in P, which seems to be a quite natural choice, the construction becomes unsound. Intuitively, when a successor state of such a product state is computed, the disjunction of the formulae joint with the successors of P may entail the formula joint with the successor of q. However, that does not mean that all pairs of source/target valuations possible in A e are possible in B too. More details are provided in Appendix A.

A fact is a formula in FormpDq.

Taking a bigger K leads to a more precise Sim i j , but, on the other hand, it can significantly increase the computation time.

Many realistic systems comply with this restriction, take, for instance, shared-memory multithreading in Java.

http://www.fit.vutbr.cz/research/groups/verifit/tools/includer/

A simulation R is trivial iff @x, y P Q : x ‰ y Ñ px, K, yq P R.

Supported by the Czech Science Foundation project 16-17538S, The French National Research Agency project VECOLIB ANR-14-CE28-0018, the BUT FIT project FIT-S-17-4014, and the IT4IXS: IT4Innovations Excellence in Science project (LQ1602).

Proof We use the fact that succ A e ˆBprrsssq " Ť tPPostpsq rrtss (Lemma 5) and that for each t P Postpsq there exists t 1 P Post Π psq such that rrtss Ď rrt 1 ss (Lemma 6).

[ \ The proof of soundness of Algorithm 1 relies on the inductive invariants (Inv 1 ) and (Inv 2 ) from the following lemma.

Lemma 8

The following invariants hold each time line 2 is reached in Algorithm 1:

-(Inv 1 ) Γ " pΠ, Visited, Next, Subsumeq is closed, -(Inv 2 ) Distproot xA,By q ă 8 Ñ DistpVisitedq ą DistpNextq.

Proof Initially, when coming to line 2 for the first time, we have Visited " H, thus DistpVisitedq " 8, and both invariants hold trivially. For the case when coming to line 2 after executing the loop body, we denote by:

the antichain states before and after the execution of the main loop. We assume that both invariants hold for Γ old .

(Inv 1 ) Let xs, py P Visited new and pq, P, νq P succ A e ˆBprrsssq. We distinguish two cases according to the control path taken inside the main loop:

(1) If the test on line 5 is positive, the predicate map is augmented, i.e., Π new Ě Π old (line 8). Let Γ 1 " pΠ new , Visited old , Next old , Subsume old q be the next antichain state. Clearly Γ 1 is closed provided that Γ old is. Next, let n pivot P Visited old be the pivot of the path to the current node (line 6) and define the following sets of nodes:

T " SUBTREEpn pivot q, S " tn P Visited old | Dm P T . pn, mq P Subsume old u.

Then we obtain (lines 10-13): Post Π psq such that L pq,P,νq pA e ˆBq Ď L t pA e ˆBq (by Lemma 7). We distinguish two cases: