Véronique Bruyère

Marc Ducobu

Olivier Gauwin

Right-Universality of Visibly Pushdown Automata

Visibly pushdown automata (VPAs) express properties on structures with a nesting relation such as program traces with nested method calls. In the context of runtime verification, we are interested in the following problem: given u, the beginning of a program trace, and A, a VPA expressing a property to be checked on this trace, can we ensure that any extension uv of u will be accepted by A? We call this property right-universality w.r.t. u. We propose an online algorithm detecting at the earliest position of the trace, whether this trace is accepted by A. The decision problem associated with right-universality is ExpTime-complete. Our algorithm uses antichains and other optimizations, in order to avoid the exponential blow-up in most cases. This is confirmed by promising experiments conducted on a prototype implementation.

crementally check right-universality is an interesting issue. Third, the algorithm proposed in the deterministic case [GNT09] does not directly generalize to the non-deterministic case.

Our contributions are the following. We propose an efficient incremental algorithm checking right-universality of a non-deterministic VPA A. This algorithm relies on the progressive computation of safe sets of configurations, the configuration of a VPA being a state together with a stack content. It avoids to enterily determinize the given VPA. This algorithm uses antichains in order to get a compact representation of safe sets of configurations. We also propose efficient operators and data structures for saving useless computation. We report on some experiments, performed on randomly generated VPAs, and also on VPAs resulting from a translation from XPath expressions. These results exhibit the benefits of our optimizations.

Verification of traces with a nesting structure has already been addressed, through different aspects. Let us mention some of them. In [AEM04], the logic CaRet over words with a nesting structure is introduced, and a model checking algorithm is proposed. An extension is presented in [RCB08], with a corresponding monitor synthesis algorithm. VPAs are also sometimes used as an intermediate model to express properties on program traces [CA07,FJJ + 12].

The paper is structured as follows. In Section 2 we introduce VPAs and rightuniversality. Safe sets of configurations are defined in Section 3. Our antichainbased algorithm is described in Section 4, and further optimizations in Section 5. Experiments are reported in Section 6. Proofs are provided in Appendix.

Introduction

Program traces describe the control flows of program executions, including subroutine calls and returns. Some properties of program traces are specific to the nesting structure of calls and returns, as for instance reentrant locks [START_REF] Bultan | Modular verification of synchronization with reentrant locks[END_REF]. These properties are not captured by regular languages, but can be expressed by visibly pushdown languages [AM09]. These latter languages rely on a partitioning of the input alphabet into internal letters, call letters, and return letters, which naturally fits to program traces. A language over such a partitioned alphabet is visibly pushdown if there exists a visibly pushdown automaton (VPA) recognizing it. VPAs are pushdown automata, where operations on the stack are driven by the letter type: call letters can only push, return letters can only pop, while internal letters do not have access to the stack.

Runtime verification amounts to check a property during a program execution. In this paper we are interested in finding the earliest point during the execution where the property can be asserted, for properties defined by VPAs. More formally, given a word u over a partitioned alphabet and a VPA A, we say that A is right-universal w.r.t. u if, for every possible continuation v of u, the word uv is accepted by A. Hence, if u is a prefix of the trace w and A is known to be right-universal w.r.t. u, then it can be asserted that w verifies the property described by A, without reading w entirely. Our aim is to check rightuniversality incrementally after each incoming event of the trace w, as described Algorithm 1 Checking right-universality incrementally function Incremental-right-universality(A) u ← ǫ while trace w is not completely read do a ← next letter of w u ← ua if A is right-universal w.r.t. u then return True end if end while return False end function in Algorithm 1. By incremental, we mean that some information is propagated from one event (reading a letter in w) to the next one (reading the next letter in w), avoiding repeated identical computations. Note that our algorithm will not store u, but enough information for asserting right-universality of A w.r.t. u.

For safety properties, right-universality allows to know at the earliest time point, whether the execution is sure, and thus whether controls can be stopped. This is typically the case for properties looking for a pattern (potentially complicated) that must occur during the execution. For properties to be avoided, this permits to stop the program before it enters an unsafe configuration, hence avoiding potential attacks [START_REF] Benedikt | Stream Firewalling of XML Constraints[END_REF].

These questions started to be addressed in the context of XML through earliest query answering of XPath expressions [START_REF] Bar-Yossef | Buffering in query evaluation over XML streams[END_REF][START_REF] Gauwin | Earliest query answering for deterministic nested word automata[END_REF]. Indeed, XML documents also entail a nesting structure, similarly to program traces, and properties (or queries) over these documents can be expressed using VPAs. An algorithm asserting at the earliest time point, whether an XML document is accepted by a deterministic VPA has been proposed in [START_REF] Gauwin | Earliest query answering for deterministic nested word automata[END_REF]. This algorithm runs in polynomial time at each incoming event. For non-deterministic VPAs, however, the decision problem associated with right-universality (i.e. given A and u, is A right-universal w.r.t. u?) is known to be ExpTime-complete [START_REF] Gauwin | Earliest query answering for deterministic nested word automata[END_REF].

Algorithms that incrementally check right-universality of non-deterministic VPAs are challenging in several aspects. First, VPAs are usually an intermediate object, resulting from the translation of a property expressed in some logics, like XPath for XML documents. Such translations rely on non-determinism, as for instance when referring to any call inside a given procedure call (which corresponds to the descendant axis in XPath). Any VPA can be determinized, but the procedure yields VPAs of exponential size [AM09]. Second, right-universality w.r.t. u can be considered as a variant of universality, parameterized by u. Recent techniques have been proposed to check universality of non-deterministic VPAs efficiently [TO12,FKL13,BDG13]. Among them, antichains have been successfully applied to decision problems related to non-deterministic automata: universality and inclusion for finite word automata [START_REF] De Wulf | Antichains: A new algorithm for checking universality of finite automata[END_REF], and for non-deterministic bottom-up tree automata [BHH + 08]. Whether these techniques also apply to in-2 Visibly Pushdown Automata and Right-Universality Visibly pushdown automata (VPAs) are pushdown automata working on a partitioned alphabet where only call symbols can push, return symbols can pop, and internal symbols can fire transitions without considering the stack [START_REF] Alur | Visibly pushdown languages[END_REF]AM09].

In this paper, we consider trees, instead of words with a nesting structure (i.e. their linearization). Such a mapping is illustrated in Figure 1. Each call and its matching return are mapped to a node, and the calls and returns directly nested under this call correspond to the children of this node. These trees are unranked, as the number of children of a node is not determined by its label. We use VPAs as unranked tree acceptors, operating on their linearization [START_REF] Gauwin | Streaming tree automata[END_REF]. In particular these VPAs do not use internal symbols.

Unranked Trees

We here recall the standard definition of unranked trees, as provided for instance in [CDG + 07]. Let Σ be a finite alphabet, and Σ * (resp. Σ + ) be the set of all words (resp. non empty words) over Σ. The empty word is denoted by ǫ. Given two words v, w ∈ Σ * over Σ, v is a prefix (resp. proper prefix ) of w if there exists a word

v ′ ∈ Σ * (resp. v ′ ∈ Σ + ) such that vv ′ = w. g g g f call(g) call(g) return(g) call(g) call(f) return(f) return(g) return(g)
Fig. 1: Representation of a program trace as a tree t.

An unranked tree t over Σ is a tree such that its nodes are labeled by a letter of Σ and have an arbitrary number of children (the children are ordered from left to right). We call a-node a node with label a ∈ Σ. The set of all unranked trees over Σ is denoted by T Σ . A hedge h over Σ is a finite sequence (empty or not) of unranked trees over Σ. The empty hedge is denoted by ǫ, and the set of all hedges over Σ is denoted by H Σ .

Trees can be described by well-balanced words which correspond to a depthfirst traversal of the tree. An opening tag is used to notice the arrival on a node and a closing tag to notice the departure from a node. For each a ∈ Σ, let a itself represent the opening tag and a the related closing tag. The linearization

[t] of t ∈ T Σ is the well-balanced word over Σ ∪ Σ, with Σ = {a | a ∈ Σ}, inductively defined by: [t] = a [t 1 ] • • • [t n ]
a, with a is the label of the root and t 1 , . . . , t n are its n subtrees (from left to right). The linearization is extended to hedges as follows. Let

h = t 1 • • • t n be the sequence of trees t i , 1 ≤ i ≤ n. Then [h] = [t 1 ] • • • [t n ]. We denote by [T Σ ] (resp. [H Σ ]
) the set of linearizations of all trees in T Σ (resp. hedges in H Σ ). Consider for instance the tree t in Figure 1: its linearization is the word [t] = ggggf fgg. Let Pref (T Σ ) denote the set of all prefixes of [T Σ ]:

Pref (T Σ ) = {u ∈ (Σ ∪ Σ) * | ∃v ∈ (Σ ∪ Σ) * , uv ∈ [T Σ ]}.

Visibly Pushdown Automata Definition 1. A visibly pushdown automaton

A over a finite alphabet Σ is a tuple A = (Q, Σ, Γ, Q i , Q f , ∆) where Q is a finite set of states containing initial states Q i ⊆ Q and final states Q f ⊆ Q, a
finite set Γ of stack symbols, and a finite set ∆ of rules. Each rule in ∆ is of the form q a:γ --→ q ′ with a ∈ Σ ∪ Σ, q, q ′ ∈ Q, and γ ∈ Γ .

The left-hand side of a rule q a:γ --→ p ∈ ∆ is (q, a) if a ∈ Σ, and (q, a, γ) if a ∈ Σ. A VPA is deterministic if it has at most one initial state, and it does not have two distinct rules with the same left-hand side. We provide an example of deterministic VPA in Figure 2a.

A configuration of a VPA A is a pair (q, σ) where q ∈ Q is a state and

σ ∈ Γ * a stack content. A configuration is initial (resp. final ) if q ∈ Q i (resp. q ∈ Q f ) and σ = ǫ. For a ∈ Σ ∪ Σ, we write (q, σ) a -→ (q ′ , σ ′ ) if there is a transition q a:γ --→ q ′ in ∆ verifying σ ′ = γ • σ if a ∈ Σ, and σ = γ • σ ′ if a ∈ Σ. We extend this notation to words u = a 1 • • • a n , by writing (q 0 , σ 0 ) u -→ (q n , σ n ) 0 1 2 f : γ0 g : γ0 g : γ0 g : γ1 f : γ0 g : γ1 f : γ0 g : γ1 f /g : γ0 f /g : γ0 (a) VPA A over alphabet Σ = {f, g}. (0, ǫ) (1, γ0) (1, γ1γ0) (1, γ0) (1, γ1γ0) (2, γ0γ1γ0) (2, γ1γ0) (2, γ0) (2, ǫ) g g g g f f g g (b) Run of A on [t]
Fig. 2: An automaton and one of its runs.

whenever there exist configurations (q i , σ i ) such that (q i-1 , σ i-1 )

ai -→ (q i , σ i ) for all 1 ≤ i ≤ n. A run of a VPA A on a linearization [t] = a 1 • • • a n of t ∈ T Σ is a sequence (q 0 , σ 0 ) • • • (q n ,
σ n ) of configurations such that (q 0 , σ 0 ) is initial, and for every 1 ≤ i ≤ n, (q i-1 , σ i-1 ) ai -→ (q i , σ i ). Such a run is accepting if (q n , σ n ) is final. A tree t is accepted by A if there is an accepting run on its linearization [t]. The set of accepted trees is called the language of A and is written L(A). 3 For instance, given a tree t, the VPA of Figure 2a checks whether t has a g-node with an f -child. An accepting run on [t] for the tree t of Figure 1, is depicted in Figure 2b.

Universality and Right-Universality

We conclude the section of preliminaries with the notions of universality4 and right-universality, that we will study in the remainder of the paper. Definition 2. A VPA A over Σ is said universal if A accepts all trees t ∈ T Σ , i.e. L(A) = T Σ . Let u ∈ Pref (T Σ ) \ {ǫ} be a non empty prefix of [t 0 ] for some tree t 0 ∈ T Σ . The VPA A is said right-universal w.r.t. u if for all trees t ∈ T Σ , if u is a prefix of [t], then t is accepted by A.

In other words, right-universality w.r.t. u allows to assert that any tree linearization beginning with u is accepted by the automaton. In this definition, notice that when u = [t 0 ], then A is right-universal w.r.t. u iff t 0 is accepted by A. Moreover, as a universal VPA is right-universal w.r.t. all non empty words u ∈ Pref (T Σ ), we assume in the sequel that VPAs are not universal.

In this article, our objective is to propose an incremental algorithm for rightuniversality of a VPA A, in the sense described in the introduction (see Algorithm 1). More precisely, the linearization [t 0 ] of a given tree t 0 is read letter by letter5 , and while A is not right-universal w.r.t. the current read prefix u of [t 0 ], the next letter of [t 0 ] is read. When processing a new letter, we try to reuse prior computations as much as possible. In the sequel t 0 always refers to this particular tree.

We recall that the right-universality problem is ExpTime-complete for VPAs, but in PTime for deterministic VPAs [START_REF] Gauwin | Earliest query answering for deterministic nested word automata[END_REF]. A dual problem to right-universality w.r.t. u is to ask whether every word starting with u is rejected by a given VPA. This problem is in PTime, even when the VPA is not deterministic. Indeed, this amounts to check whether no configuration reached after reading u can reach a final configuration.

Towards an Algorithm

In this section we consider several approaches for addressing right-universality of VPAs, and justify our choice of considering safe sets of configurations. Readers not familiar with the related litterature can skip this section at first reading. As explained in the introduction, we discard the naive approach consisting in determinizing the VPA and then applying the algorithm in [START_REF] Gauwin | Earliest query answering for deterministic nested word automata[END_REF], in order to avoid state-space explosion.

The algorithm given in [START_REF] Gauwin | Earliest query answering for deterministic nested word automata[END_REF] for deterministic VPAs is a progressive computation of safe states, with the property that the VPA is right-universal w.r.t. u iff the state reached after reading u is safe. Note that safe states cannot be determined statically: a state can be safe at some position of the word, but not at another one. A first idea for the non-deterministic case is a subset construction, using sets of safe states instead of safe states, but this direct adaptation is not correct. Hence, safe sets of configurations will be the basis of our algorithm, instead of safe states. This point raises new questions, as the configuration space is infinite, unlike the state space. In fact we will see that at each event, safe sets of configurations have the same stack height as the depth of the word u leading to this event, and are thus of finite (but potentially huge) cardinality at each time point.

Recently, several authors have proposed efficient algorithms to check universality of VPAs [START_REF] Tang | On model checking for visibly pushdown automata[END_REF][START_REF] Friedmann | Ramsey goes visibly pushdown[END_REF]BDG13]. The method that we give in [BDG13] computes in an incremental way the set R of accessibility relations for all hedges (i.e. {rel h | h ∈ H Σ } in the present paper, also called summaries in [START_REF] Alur | Visibly pushdown languages[END_REF]). It uses antichains to get smaller objects to manipulate (in particular to limit R to a strict smaller subset) and to avoid an explicit determinization step. It can be easily adapted for checking right-universality of VPAs [BDG12, Section 3.4]. However we face the problem of computing the whole set R (instead of a strict subset): experiments indicate that this step is too much time consuming [BDG13]. For this reason we do not follow this approach, but use antichains over safe sets of configurations rather than accessibility relations. This approach is developed in the next section.

Safe Sets of Configurations

In this section, [t 0 ] is a fixed tree whose linearization is read letter by letter, and u denotes the current read prefix. We introduce the new notion of safe set of configurations related to u. We show how safe sets of configurations can be defined from such sets associated to smaller prefixes u ′ of [t 0 ]. This property will be useful to derive an incremental algorithm for checking right-universality of a VPA.

A Notion of Safety for Right-Universality

Definition 3. Let A be a VPA and

C ⊆ Q × Γ * be a non empty set of config- urations. Let u ∈ Pref (T Σ ) \ {ǫ} be a non empty prefix of t 0 . -C is safe for u if for every v such that uv ∈ [T Σ ], there exist (q, σ) ∈ C and p ∈ Q f such that (q, σ) v -→ (p, ǫ) in A. -C is leaf-safe for u if for every v = av ′ with a ∈ Σ such that uv ∈ [T Σ ], there exist (q, σ) ∈ C and p ∈ Q f such that (q, σ) v -→ (p, ǫ) in A. 6 Let Safe(u) = {C | C is safe for u} and LSafe(u) = {C | C is leaf-safe for u}.
Intuitively, as stated in Theorem 1 below, if C is the set of configurations reached in A after reading u, then A is right-universal w.r.t. u iff C is safe for u. Indeed, for every possible v, one can find in C at least one configuration leading to an accepting configuration after reading v. Before stating this theorem, let us give the next definition. Let Reach(u) denote the set of configurations (q, σ) such that (q 0 , σ 0 ) u -→ (q, σ) for some initial configuration (q 0 , σ 0 ) of A.

Theorem 1. A is right-universal w.r.t. u iff Reach(u) ∈ Safe(u).
Let us illustrate this on the VPA A depicted in Figure 2a. Recall that this VPA checks that the tree has a g-node with an f -child. After opening a g-root, the set of safe configurations is Safe(g) = {{(q 2 , γ 1 )}, {(q 2 , γ 0 )}}, which does not contain the set of reached configurations, as Reach(g) = {(q 1 , γ 0 )}. Indeed, A is not right-universal w.r.t. g, as no f -node has been encountered yet under a g-node. For the word gf , as expected, the situation differs: Safe(gf ) = {{(q 2 , γ 1 γ 0 )}, {(q 2 , γ 0 γ 0 )}}, and Reach(gf

) = {(q 2 , γ 0 γ 0 )} is a safe set of config- urations. By Theorem 1, A is right-universal w.r.t. gf .
Hence, an algorithm computing both Reach(u) and Safe(u) can decide rightuniversality w.r.t. u. The set Reach(u) is easy to compute, just by firing transitions of the VPA. In Sections 3.2-3.4, we detail how the set Safe(u) can be defined from the set Safe(u ′ ) with u ′ a proper prefix of u. In this way, while reading the linearization [t 0 ] of a given tree t 0 , the set Safe(u) with u = ǫ prefix of [t 0 ], can be incrementally defined. In Section 4, we turn this approach into an algorithm.

Starting Point

We begin with Safe(a) with a ∈ Σ, for which we recall the definition.

Safe(a) = {C ⊆ Q×Γ * | ∀h∈H Σ , ∃q f ∈Q f , ∃(q, σ)∈C : (q, σ) ha -→ (q f , ǫ)} (1)
3.3 Reading a Letter a ∈ Σ Suppose that we are reading an a ∈ Σ and we have to compute Safe(ua). Two cases occur : either ua = [t 0 ], or ua = [t 0 ]. Let us study these two cases and show how to manage them from an algorithmic point of view.

If ua = [t 0 ], we can retrieve safe sets configurations from prior computed such sets: Safe(ua) = Safe(u ′ ) where u ′ = ǫ is the unique prefix of u such that u = u ′ a[h], with h ∈ H Σ . Indeed as shown by Lemma 1 below, we have Safe(u ′ a[h]a) = Safe(u ′ ). Hence, from an algorithmic point of view, we just have to use a stack S to store these safe sets of configurations. When opening a, we put Safe(u ′ ) on the stack, and when closing a, we pop it. As h is a hedge, the stack before reading a is exactly the stack after reading a.

Lemma 1. If h ∈ H Σ , then Safe(u[h]) = Safe(u) and LSafe(u[h]) = LSafe(u).
If ua = [t 0 ], the previous argument is no longer correct since u ′ = ǫ and Safe(u ′ ) is not defined for the empty word. Nevertheless, by definition Safe(ua

) = {C ⊆ Q × Γ * | ∃(q, ǫ) ∈ C with q ∈ Q f }.
Therefore we can again use stack S as described before if it is initialized with the set

Init = {C ⊆ Q × Γ * | ∃(q, ǫ) ∈ C with q ∈ Q f }.
(2)

Reading a Letter a ∈ Σ

Let us now consider the much more involved case of sets Safe(ua) with a ∈ Σ.

When reading an a ∈ Σ, two successive steps are performed, with leaf-safe sets of configurations as intermediate object:

Safe(u)

Step 1

----→ LSafe(ua)

Step 2

----→ Safe(ua)

For this purpose, we introduce the notion of predecessor. Let C , C ′ be two sets of configurations, let a ∈ Σ and h ∈ H Σ .

-C is an a-predecessor of C ′ if ∀(q ′ , σ ′ ) ∈ C ′ , ∃(q, σ) ∈ C , (q, σ) a -→ (q ′ , σ ′ ). -C is a h-predecessor of C ′ if ∀(q ′ , σ ′ ) ∈ C ′ , ∃(q, σ) ∈ C , (q, σ) [h] --→ (q ′ , σ ′ ). Let Pred a (C ′ ) = {C | C is an a-predecessor of C ′ } and Pred h (C ′ ) = {C | C is a h-predecessor of C ′ }.
The next proposition can be used to perform Step 1 and Step 2. It states that safe sets of configurations are only among predecessors of prior safe sets of configurations.

Proposition 1. Let ua ∈ Pref (T Σ ). C ∈ LSafe(ua) ⇐⇒ ∃C ′ ∈ Safe(u), C ∈ Pred a (C ′ ) (3) C ∈ Safe(ua) ⇐⇒ ∀h ∈ H Σ , ∃C ′ ∈ LSafe(ua), C ∈ Pred h (C ′ ) (4)
However, to get an algorithm, we face the problem that the number of hedges to consider in Equivalence (4) is infinite. We use relations to overcome this. Also the size of Safe(u) may be huge and not all configurations of Safe(u) are crucial for checking right-universality w.r.t. u. We use antichains to get a compact representation of Safe(u). These two concepts are explained in the following section.

An Antichain-Based Algorithm for Right-Universality

In this section, we give an antichain-based algorithm for incrementally checking right-universality of a VPA, that uses the approach given in Sections 3.2-3.4.

Let us summarize this approach. Let [t 0 ] be the linearization of a given tree t 0 . We initialize a stack S with set Init defined in (2) and we start by computing Safe(u) with u being the first letter of [t 0 ] (see (1)). Suppose that Safe(u) has been computed from the current read prefix u of [t 0 ]. Then, if the next letter read in [t 0 ] is a ∈ Σ, we compute Safe(ua) from Safe(u) by Steps 1 and 2, and we put Safe(u) on the stack S. If the next letter read in [t 0 ] is a ∈ Σ, then we pop the stack S. The element that has been popped is the set Safe(u ′ ) = Safe(ua) where u ′ is the unique prefix of u such that u = u ′ a[h] (except if ua = t 0 in which case the popped set is equal to Init = Safe(ua)), see Section 3.3. At each computation of Safe(u), we check whether Reach(u) ∈ Safe(u) (see Theorem 1).

Finite Number of Hedges

We begin by showing that only a finite number of hedges has to be considered in Equivalence (4). The reason is that a hedge h does not change the stack of a configuration during a run of a VPA, that is (q, σ)

[h] --→ (q ′ , σ). So h can be considered as a function mapping each state q to the set of states obtained when traversing h from q. Formally, for every h ∈ H Σ , rel h is the function from Q to 2 Q such that q ′ ∈ rel h (q) iff (q, σ)

[h] --→ (q ′ , σ) for some σ ∈ Γ * . The number of such functions is finite, and bounded by |Q| • 2 |Q| . These functions naturally define an equivalence relation of finite index over H Σ :

h ∼ h ′ ⇐⇒ rel h = rel h ′ .
Let us note H for a subset containing one hedge per ∼-class. We have |H| ≤ |Q| • 2 |Q| . The next lemma indicates that the computation of h-predecessors can be limited to h ∈ H.

Lemma 2. For every h ∈ H Σ , C is a h-predecessor of C ′ iff there exists h ′ ∈ H with h ∼ h ′ , such that C is a h ′ -predecessor of C ′ .
The set H can be computed by a saturation method based on the VPA rules, as described by Algorithm 3 in Appendix B.2.

Antichains

Let us now introduce antichains. Consider the set 2 Q×Γ * of all sets of configurations, with the ⊆ operator. An antichain is a set of pairwise incomparable sets of configurations with respect to ⊆. Given a set α of sets of configurations, we denote by ⌊α⌋ the ⊆-minimal elements of α. The set α is ⊆-upward closed if for all C ∈ α and C ⊆ C ′ , we have C ′ ∈ α. From their definition, it is immediate that Safe(u), LSafe(u), Pred a (C ) and Pred h (C ) are ⊆-upward closed sets.

The idea is to compute the antichain ⌊Safe(u)⌋ (resp. ⌊LSafe(u)⌋) instead of the whole ⊆-upward closed set Safe(u) (resp. LSafe(u)). The next corollary of Theorem 1 indicates that such a limited computation is enough to check whether a VPA A is right-universal w.r.t. u.

Corollary 1. A is right-universal w.r.t. u iff there exists C ∈⌊Safe(u)⌋ such that C ⊆Reach(u).

Moreover, we show in Appendix B.3 that the antichains ⌊Safe(u)⌋ and ⌊LSafe(u)⌋ are finite and only contain finite sets C of configurations such that C ⊆ Q × Γ k for some k. We now try to use these antichains at the starting point, and in Steps 1 and 2 of our approach.

Starting Point with Antichains

Let us explain how to compute Safe(a). Clearly, by definition of H and using (1) (see Section 3.2), we can compute ⌊Safe(a)⌋ as follows:

⌊Safe(a)⌋ = C | ∀h ∈ H, ∃q f ∈ Q f , ∃(q, σ) ∈ C : (q, σ) ha -→ (q f , ǫ) . (5)
4. 4 Step 1 with Antichains: from ⌊Safe(u)⌋ to ⌊LSafe(ua)⌋ For the two steps, the goal is to adapt Proposition 1 so that it uses ⌊Safe(.)⌋ instead of Safe(.), and ⌊LSafe(.)⌋ instead of LSafe(.). We begin with Step 1. Implication (⇒) of Equivalence (3) can be directly adapted.

C ∈ ⌊LSafe(ua)⌋ =⇒ ∃C ′ ∈ ⌊Safe(u)⌋ , C ∈ Pred a (C ′ ). (6)
Implication (6) gives us a way to compute ⌊LSafe(ua)⌋ from ⌊Safe(u)⌋: it suffices to take all a-predecessors of elements of ⌊Safe(u)⌋ and then limit to those predecessors that are ⊆-minimal. We can even only consider minimal apredecessors of ⌊Safe(u)⌋ in the following sense: C is a minimal a-predecessor of

C ′ if for all C ′′ a-predecessor of C ′ , C ′′ ⊆ C =⇒ C ′′ = C . We finally obtain: ⌊LSafe(ua)⌋ = ⌊{C | C is a minimal a-predecessor of C ′ ∈ ⌊Safe(u)⌋}⌋ . (7)
4. 5 Step 2 with Antichains: from ⌊LSafe(ua)⌋ to ⌊Safe(ua)⌋

The second step for computing ⌊Safe(ua)⌋ from ⌊Safe(u)⌋ relies on the introduction of antichains in Equivalence (4). Implication (⇒) holds with antichains:

C ∈ ⌊Safe(ua)⌋ =⇒ ∀h ∈ H Σ , ∃C ′ ∈ ⌊LSafe(ua)⌋ , C ∈ Pred h (C ′ ). ( 8
)
Similarly to Implication (6), we can restrict h-predecessors to only consider minimal ones:

C is a minimal h-predecessor of C ′ if for all C ′′ h-predecessor of C ′ , C ′′ ⊆ C =⇒ C ′′ = C
. Moreover, by Lemma 2, we can limit the computations to hedges h ∈ H where H is the finite set introduced in Section 4.1. Therefore, we obtain the next equality.

⌊Safe(ua)⌋ = C | C = h∈H C h with C h a minimal h-predecessor of C ′ ∈ ⌊LSafe(ua)⌋ (9)

Algorithm

We are now able to give our antichain-based algorithm (see Algorithm 2). It uses a stack S (initially empty) as recalled at the beginning of this section. The computation of ⌊H⌋ is considered as a preprocessing, as its value only depends on A and not on [t 0 ]. The used results are mentioned inside the algorithm.

Improvements and Implementation

Section 4 resulted in a first algorithm for incrementally testing whether a VPA is right-universal. In this section, we show how this algorithm can be improved by limiting hedges to consider, and optimizing operators and predecessors to be computed. We also give the improved algorithm in a more detail way than in Algorithm 2, as well as the underlying data structures.

Minimal Hedges

A first improvement is obtained by further restricting hedges to consider. Indeed it suffices to consider minimal hedges wrt their function rel h . Formally, let us write h ≤ h ′ whenever rel h (q) ⊆ rel h ′ (q) for every q ∈ Q. We denote by ⌊H⌋ the ≤-minimal elements of H. From the definition of h-predecessor, we have:

C h-predecessor of C ′ and h ≤ h ′ =⇒ C h ′ -predecessor of C ′ (10)
This property can be used to replace h ∈ H in (9) by h ∈ ⌊H⌋:

⌊Safe(ua)⌋ =        C | C = h∈⌊H⌋ C h with C h a minimal h-predecessor of C ′ ∈ ⌊LSafe(ua)⌋        (
⌊Safe(a)⌋ = C | ∀h ∈ ⌊H⌋ , ∃q f ∈ Q f , ∃(q, σ) ∈ C : (q, σ) ha -→ (q f , ǫ) (12)

An Appropriate Operator

Equation (11) expresses that every set of configurations C in ⌊Safe(ua)⌋ is the union of C h with h ∈ ⌊H⌋. We introduce a new operator to improve the readability and find new properties. Let S be a finite set, and A, B ∈ 2 2 S \{∅} . The set A ⊔ B ∈ 2 2 S is defined by

A ⊔ B = {a ∪ b | a ∈ A and b ∈ B}.
Operator ⊔ builds sets obtained by taking one set of each of its operands, and performing their union. It is obviously associative and commutative. Notice that the elements of A, B are supposed to be non empty sets. This is always the case in the algorithms using this operator. When combined with operator ⌊.⌋, operands of the ⊔ operator can be splitted, so that ⊔ is to be computed on smaller sets:

⌊A ⊔ B⌋ = ⌊(A ∩ B) ∪ (A \ B ⊔ B \ A)⌋ (13)
We experimentally observed that a good strategy to evaluate an expression A 1 ⊔ . . . ⊔ A n is to process sets A i with increasing cardinality. Equation ( 11) can now be rewritten in a simpler way as follows.

⌊Safe(ua)⌋ =     h∈⌊H⌋ {C h | C h is a minimal h-predecessor of C ′ ∈ ⌊LSafe(ua)⌋}     (14)
We can go further by reconsidering the notions of minimal a-and h-predecessor with the new operator ⊔. From the definition of minimal predecessor, we immediately get that C is a minimal a-predecessor of C ′ iff C belongs to the set (q ′ ,σ ′ )∈C ′ {(q, σ)} | (q, σ) a -→ (q ′ , σ ′ ) , and similarly for h-minimal predecessors. We provide in Appendix C.3 a similar improvement for ⌊Safe(a)⌋.

Using a SAT Solver to Find Minimal Predecessors

The operator ⊔ allows to compute Step 1 and Step 2. Equation (13) accelerates these computations. In this section, we propose a method to compute

Step 1 based on a SAT solver (a similar approach also works for Step 2, see Appendix C.4).

A SAT solver is an algorithm used to efficiently test the satisfiability of a boolean formula ϕ, that is, to check whether there exists a valuation v of the boolean variables of ϕ that makes ϕ true. In this case we say that v is a model of ϕ, denoted by v |= ϕ.

In Step 1, the computation of set ⌊LSafe(ua)⌋ from ⌊Safe(u)⌋ is given in (7):

⌊LSafe(ua)⌋ = ⌊{C | C is an a-predecessor of C ′ ∈ ⌊Safe(u)⌋}⌋ .
We recall that C is an a-predecessor of C ′ if for all (q ′ , σ ′ ) ∈ C ′ , there exists (q, σ) ∈ C such that (q, σ) a -→ (q ′ , σ ′ ). We also recall that C ∈ ⌊LSafe(ua)⌋ is a finite object such that C ⊆ Q × Γ k for some k. Let us associate a boolean variable x c to each configuration c ∈ Q × Γ k .

We consider the following boolean formula ϕ a :

ϕ a = C ′ ∈⌊Safe(u)⌋ c ′ ∈C ′ c a -→c ′ x c , Let v C be the valuation such that v C (x c ) = 1 iff c ∈ C . We immediately obtain that: v C |= ϕ a iff C ∈ LSafe(ua) ∩ Q × Γ k .
We define an ordering over valuations as follows, in a way to have a notion of minimal models equivalent to ⊆-minimal elements of LSafe(ua).

Let V be a set of boolean variables, let v and v ′ be two valuations over V . We define

v ′ ≤ v iff for all variables x ∈ V , v ′ (x) = 1 =⇒ v(x) = 1. We denote v ′ < v if v ′ ≤ v and v ′ = v. Given ϕ a boolean formula over V , we say that a model v of ϕ is minimal if for all model v ′ of ϕ, we have v ′ ≤ v =⇒ v ′ = v. We get the next characterization. Lemma 3. v C is a minimal model of ϕ a iff C ∈ ⌊LSafe(ua)⌋.
We can now explain how to compute all the minimal models of formula ϕ a . Let ϕ be a boolean formula over V . First, we explain, knowing a model v of ϕ, how to compute a model v ′ of ϕ such that v ′ < v (if it exists). Consider the next formula ϕ ′ :

ϕ ′ = ϕ ∧ ( x∈V0 ¬x) ∧ ( x∈V1 ¬x) where V 0 (respectively V 1 ) is the set of all variables x ∈ V such that v(x) = 0 (resp. v(x) = 1). If ϕ ′ has a model v ′ , it follows from the definition of ϕ ′ that v ′ is a model of ϕ such that v ′ < v. Otherwise, v is a minimal model of ϕ.
So from a model of ϕ we can compute a minimal model of ϕ by repeating the above procedure. Second, let us explain how to compute all the minimal models of ϕ. Suppose that we already know some minimal model v of ϕ, and let V 1 be the set of variables x ∈ V such that v(x) = 1. Consider the formula

ϕ ′ = ϕ ∧ ( x∈V1 ¬x). Then a model v ′ of ϕ ′ , if it exists, is a model of ϕ such that neither v ′ < v (since v is minimal) nor v < v ′ (
by definition of ϕ ′ ). With the previous procedure, we thus get a minimal model of ϕ that is distinct from v. In this way we can compute all minimal models of ϕ.

Improved Algorithm and Data Structures

Let us come back to Algorithm 2 by indicating the underlying data structures and the improvements resulting from the previous three sections.

As explained in Section 5.1, we restrict the computations to the set ⌊H⌋ of minimal hedges. Notice that Algorithm 3 that computes the set {rel h | h ∈ H} (see Appendix) can be easily adapted to compute the set of its ≤-minimal elements. In the main loop of Algorithm 2, Steps 1 and 2 can be computed either with the new operator ⊔ or with a SAT solver (see Sections 5.2 and 5.3 resp.).

Efficient data structures are used both for the relations associated to minimal hedges and for the antichains ⌊H⌋, ⌊Safe(u)⌋ and ⌊LSafe(u)⌋. A relation rel h , with h ∈ ⌊H⌋, is stored as an array of bit-vectors. In this way the composition is computed efficiently using bit-operations, as well as the number of elements of the relation. A hash table is used to store each antichain, such that elements with different weights are stored in different lists. In the case of ⌊H⌋, the weight is the number of elements of rel h ∈ ⌊H⌋. In the case of ⌊Safe(u)⌋ (resp. ⌊LSafe(u)⌋), the weight is the number of elements of C ∈ ⌊Safe(u)⌋ (resp. C ∈ ⌊LSafe(u)⌋). In this way, comparing a new element with the elements of the antichain is made more efficient, by limiting the comparison with elements of the same weight.

Experiments

We have implemented Algorithm 2 in a prototype tool together with the data structures and improvements proposed in Section 5 (following both approaches, using operator ⊔ and a SAT solver). We mainly use Python, with C binding to the Glucose SAT solver (first ranked in recent SAT competitions) [Glucose].

The experimental tests are performed on two different benchmarks, one composed of randomly generated VPAs, and another one based on the translation of XPath expressions to VPAs. The experiments were run on a PC equipped with an Intel i7 2.8GHz processor, 6 GB of RAM and running Linux Ubuntu 3.2. |Q| , and the transition density7 . Our online algorithm for checking rightuniversality needs to compute the set ⌊H⌋ of minimal hedges as a preprocessing. This set can be huge and thus lead to a timeout. In Figure 3a (resp. Figure 3b), we indicate the average size of ⌊H⌋ (resp. the average execution time to compute it) for randomly generated VPAs with variable transition density (from 1 to 19) and variable final state density. In this test, we distinguish universal automata from non-universal ones since a universal VPA is right-universal w.r.t all u ∈ Pref (T Σ ) \ {ǫ}. The two figures show that timeout happens for instances with transition density around 12, and that the density of final states has few influence. In the next experiment, we study the behavior of our algorithm on 90 random instances of size 10 (resp. 20, 30), with fixed transition density 8 (resp. 16) and fixed density 0.5 of final states8 . The considered tree t 0 is a complete binary tree up to height 3 filled with randomly generated letters of Σ. We only comment the experiment using a SAT solver since it outperforms the approach with operator ⊔. We observe several behaviors (see Table 1): many automata are either universal, or right-universal w.r.t. u with |u| = 1 (except 7 cases where |u| = 2), or exhibits a hedge h with rel h being the null relation9 ; the number of timeout increases with |Q|. Table 2 indicates, for some representative VPAs, the execution time and the sizes of ⌊H⌋, Reach(u) and ⌊Safe(u)⌋.

Randomly Generated VPAs

During the random generation of VPAs

A = (Q, Σ, Γ, Q i , Q f , ∆), |Q i | is fixed to 1,

|Q|

When it declares that a given VPA is right-universal w.r.t. u, our algorithm has the nice property that it reproduces the same execution (thus with the same time) for each tree t 0 such that u is prefix of [t 0 ]. This is clearly not the case for the membership algorithm that computes Reach([t 0 ]) and checks if it contains a final configuration. For instance, on a random VPA with size |Q| = 20 and transition density 8, our algorithm consumes less than 5s to declare that the automaton is right-universal w.r.t. a, whereas the membership algorithm takes more than 300s as soon as the height of a binary tree t 0 with an a-root is equal to 8 (see also Appendix D.1).

VPAs resulting from XPath translation

Our second benchmark is based on VPAs obtained from queries over XML documents expressed in the XPath language, and then translated into VPAs. This translation was performed by the QuiXProc tool, as described in [START_REF] Gauwin | Streamable fragments of forward XPath[END_REF]. This family of XPath expressions yields VPAs of linear size increase (VPA with id i has 16 + 11i states), and looks for some complex patterns in the tree. In Figure 4 we report the time used by our algorithm on randomly generated trees, for this family of VPAs. This shows that for real-world VPAs, the size of ⌊H⌋ is outside the hardness threshold exhibited in Figure 3. For instance, for the VPA with id 9 and size |Q| = 115, ⌊H⌋ is computed in about 120s. Moreover, Figure 4b shows the efficiency of our online algorithm (less than 0.8s, see also Appendix D.2).

A Complements to Section 3

A.1 Proof of Theorem 1 (⇒) Assume that A is u-universal. Consider the set C of configurations (q, σ) of A such that there exists v ∈ (Σ ∪ Σ) * , q i ∈ Q i and q f ∈ Q f verifying uv ∈ [T Σ ] and (q i , ǫ) u -→ (q, σ) v -→ (q f , ǫ). We have C ⊆ Reach(u).

Let v be such that uv ∈ [T Σ ]. As A is right-universal w.r.t. u, there exists a configuration (q, σ) ∈ C such that (q, σ) v -→ (q f , ǫ) with q f ∈ Q f . Hence C ∈ Safe(u). As Safe(u) is ⊆-upward closed, we get Reach(u) ∈ Safe(u).

(⇐) Assume now that Reach(u) ∈ Safe(u), and let v be such that uv ∈ [T Σ ]. As Reach(u) ∈ Safe(u), there exists (q, σ) ∈ Reach(u) and p ∈ Q f such that (q, σ) v -→ (p, ǫ). Thus, uv ∈ L(A), and A is right-universal w.r.t. u.

A.2 Proof of Lemma 1 (⊇) Assume C ∈ Safe(u), and let v be such that u

[h]v ∈ [T Σ ]. As h is a hedge, we have uv ∈ [T Σ ]. As C ∈ Safe(u), there exists (q, σ) ∈ C such that (q, σ) v -→ (p, ǫ) with p ∈ Q f . So C ∈ Safe(u[h]). (⊆) Conversely, assume C ∈ Safe(u[h]). Let v be such that uv ∈ [T Σ ]. We also have u[h]v ∈ [T Σ ], so there exists (q, σ) ∈ C such that (q, σ) v -→ (p, ǫ) with p ∈ Q f . Thus C ∈ Safe(u).
The proof is the same for LSafe(u[h]) = LSafe(u), except that we only consider v of the form av ′ .

A.3 Proof of Proposition 1

Before giving the proof of Proposition 1, we introduce the Post operator and Proposition 2. From u ∈ (Σ ∪ Σ) * and a set of configurations C ⊆ Q × Γ * , we define Post u (C ) as the set

Post u (C ) = {(q ′ , σ ′ ) ∈ Q × Γ * | ∃(q, σ) ∈ C , (q, σ) u -→ (q ′ , σ ′ )}. Proposition 2. Let ua ∈ Pref (T Σ ) with a ∈ Σ. C ∈ LSafe(ua) ⇐⇒ Post a (C ) ∈ Safe(u) (15)
C ∈ Safe(ua) ⇐⇒ ∀h ∈ H Σ , Post [h] (C ) ∈ LSafe(ua) (16)
Proof. (15, ⇒) Let C ∈ LSafe(ua) and

C ′ = Post a (C ). Let us show that C ′ ∈ Safe(u). By Lemma 1, it is sufficient to prove that C ′ ∈ Safe(uaa). Let v such that uaav ∈ [T Σ ].
As C ∈ LSafe(ua) and av starts with a ∈ Σ, there exists (q, σ) ∈ C and (q ′ , σ ′ ) such that (q, σ) a -→ (q ′ , σ ′ ) v -→ (p, ǫ) for some p ∈ Q f . By definition of Post a (C ) we have (q ′ , σ ′ ) ∈ C ′ and thus C ′ ∈ Safe(uaa).

(15, ⇐) For the converse, let C ′ = Post a (C ) ∈ Safe(u) = Safe(uaa). Let us show that C ∈ LSafe(ua). Let v be such that uav ∈ [T Σ ] and v = bv ′ . We necessarily have a = b. As C ′ ∈ Safe(uaa), there exists (q ′ , σ ′ ) ∈ C ′ such that (q ′ , σ ′ ) v ′ -→ (p, ǫ) with p ∈ Q f . By definition of Post a (C ), there also exists (q, σ) ∈ C such that (q, σ) a -→ (q ′ , σ ′ ) and thus (q, σ)

v=av ′ ----→ (p, ǫ) with p ∈ Q f . (16, ⇒) Let C ∈ Safe(ua) and h ∈ H Σ . Let us show that C ′ = Post [h] (C )
is in LSafe(ua). Let v such that uav ∈ [T Σ ] and v = bv ′ . We must have a = b. We also have ua[h]av ′ ∈ [T Σ ]. As C ∈ Safe(ua), there exists (q, σ) ∈ C such that (q, σ)

[h] --→ (q ′ , σ ′ ) v=av ′ ----→ (p, ǫ) with p ∈ Q f . By definition of Post [h] (C ), (q ′ , σ ′ ) ∈ C ′ .
(16, ⇐) Let us assume that for every hedge

h ∈ H Σ , Post [h] (C ) ∈ LSafe(ua). Let us show that C ∈ Safe(ua). Let v be such that uav ∈ [T Σ ]. Then we have uav = ua[h]av ′ for some h ∈ H Σ . As C ′ = Post [h] (C ) ∈ LSafe(ua), av ′ starts with a ∈ Σ and uaav ′ ∈ [T Σ ], there exists (q ′ , σ ′ ) ∈ C ′ such that (q ′ , σ ′ ) av ′ --→ (p, ǫ) for some p ∈ Q f . Hence, by definition of Post [h] (C ), there also exists (q, σ) ∈ C such that (q, σ) [h] --→ (q ′ , σ ′ ) av ′ --→ (p, ǫ) with p ∈ Q f . ⊓ ⊔
Predecessors closely relate to the Post operator, in the following sense. Let us recall the definition of h-predecessor:

C is a h-predecessor of C ′ if ∀(q ′ , σ) ∈ C ′ , ∃(q, σ) ∈ C , (q, σ) h -→ (q ′ , σ). Hence if h ∼ h ′ , then C is a h-predecessor of C ′ iff C is a h ′ -predecessor of C ′ .

B.2 Algorithm computing H

We propose an algorithm for computing such a set H from a VPA A. Algorithm 3 is based on the definition of hedges, adapted to their associated functions:

ǫ is the empty hedge, and rel ǫ (q) = {q} for every q ∈ Q. We write this function id Q . -if h 1 , h 2 are two hedges, then h 1 h 2 is a hedge, and rel h1h2 = rel h2 • rel h1 .

B.3 Antichains ⌊Safe(u)⌋ and ⌊LSafe(u)⌋ are Finite Proposition 4. ⌊Safe(u)⌋ and ⌊LSafe(u)⌋ are finite and only contain finite sets of configurations.

Proof. We begin with the following observation. Let v be such that [uv] ∈ T Σ and (q, σ) v -→ (p, ǫ) with p ∈ Q f . Let u ′ (resp. v ′ ) the word obtained from u (resp. v) by removing all factors that are linearizations of hedges. Then

|u ′ | = |v ′ | and |u ′ | = |σ|. Let C ∈ Safe(u). Then by definition ∀v, uv ∈ [T Σ ] =⇒ ∃(q, σ) ∈ C , (q, σ) v -→ (p, ǫ) with p ∈ Q f .
If C is ⊆-minimal, then every (q, σ) ∈ C is used for at least one v in the previous definition. Now by the previous observation, each such (q, σ) belongs to

Q×Γ |u ′ | . Hence C ⊆ Q × Γ |u ′ | ,
Let C ∈ ⌊LSafe(ua)⌋ and let C ′ = Post a (C ). We know from Proposition 2 that C ′ ∈ Safe(u). Let C ′ 0 ⊆ C ′ such that C ′ 0 ∈ ⌊Safe(u)⌋. From the definition of C ′ we get: ∀c ′ ∈ C ′ , ∃c ∈ C , c a -→ c ′ We build C 0 from these c ∈ C but for c ′ ∈ C ′ 0 : C 0 = {c ∈ C | ∃c ′ ∈ C ′ 0 , c a -→ c ′ }

B.5 Proof of Implication (8)

The proof is in the same vein as for Implication (6). Let C ∈ ⌊Safe(ua)⌋, and

h ∈ H Σ . Let C ′ h = Post [h] (C ). By Proposition 2, C ′ h ∈ LSafe(ua). Let C ′′ h ⊆ C ′ h such that C ′′ h ∈ ⌊LSafe(ua)⌋. We know that ∀c ′ ∈ C ′ h , ∃c ∈ C such that c [h] --→ c ′ . We define C h = {c ∈ C | ∃c ′ ∈ C ′′ h , c [h] --→ c ′ }. For every h ∈ H Σ , C h is a h-predecessor of C ′′ h ∈ LSafe(ua). Consider C ∪ = h∈HΣ C h , then C ∪ is also a h-predecessor of C ′′ h . Using Proposition 1, we have C ∪ ∈ Safe(ua). As C ∪ ⊆ C and C ∈ ⌊Safe(ua)⌋, we also have that C ∪ = C . Hence C verifies that ∀h ∈ H Σ , ∃C ′′ ∈ ⌊LSafe(ua)⌋ such that C is a h-predecessor of C ′′ . C Complements to Section 5 C.1 Proof of Equation (11) Let S denote the set C | C = h∈H C h with C h a minimal h-predecessor of C ′ ∈ ⌊LSafe(ua)⌋ Let C ∈ S. We have: C = C h1 ∪ • • • ∪ C h k hi∈⌊H⌋ ∪ C h ′ 1 ∪ • • • ∪ C h ′ n h ′ i ∈H\⌊H⌋ . Let us show that C h1 ∪ • • • ∪ C h k ∪ C h ′ 1 ∪ • • • ∪ C h ′ n-1 ∈ S (C h ′
n has been erased). By induction, this will prove that C h1 ∪ • • • ∪ C h k ∈ S. We have h ′ n ∈ H \ ⌊H⌋, so there exists h i ∈ ⌊H⌋ such that h i ≤ h ′ n . As C hi is a minimal h i -predecessor of an element C ′ in ⌊LSafe(ua)⌋, it follows from (10) that C hi is also a minimal h ′ n -predecessor of The ⊔ operator also simplifies the definition of ⌊Safe(a)⌋.

C ′ . So C h1 ∪ • • • ∪ C h k ∪ C h ′ 1 ∪ • • • ∪ C h ′ n-1 ∪ C hi ∈ S.
Proposition 5. ⌊Safe(a)⌋ = h∈⌊H⌋ A h with A h = {(q, σ)} | ∃q f ∈ Q f : (q, σ) ha -→ (q f , ǫ) .

Proof. We consider ⌊Safe(a)⌋ as defined in Equation ( 12). Let S denote the set C | ∀h ∈ ⌊H⌋ , ∃q f ∈ Q f , ∃(q, σ) ∈ C : (q, σ) ha -→ (q f , ǫ) .

1. Every element of h∈⌊H⌋ A h belongs to S. Thus h∈⌊H⌋ A h ⊆ S. 2. Let us show that for each C in S, there exists C ′ ∈ h∈⌊H⌋ A h such that C ′ ⊆ C . Let C ∈ S. By definition of S, for all h ∈ ⌊H⌋ there exists (q h , σ h ) ∈ C and q f ∈ Q f such that (q h , σ h ) ha -→ (q f , ǫ). Let C ′ = {(q h , σ h ) | h ∈ ⌊H⌋}. Then C ′ ⊆ C and C ′ ∈ h∈⌊H⌋ A h because {(q h , σ h )} ∈ A h , ∀h. The computation of the set ⌊Safe(ua)⌋ from ⌊LSafe(ua)⌋ can be done with a SAT solver as described in Equation (11) :

⌊Safe(ua)⌋ =        C | C = h∈⌊H⌋ C h with C h a h-predecessor of C ′ ∈ ⌊LSafe(ua)⌋        .
The method is the same as for Step 1, with the only difference that we use the next formula instead of formula ϕ a :

h∈⌊H⌋ C ′ ∈⌊LSafe(ua)⌋ c ′ ∈C ′ c h -→c ′ x c ,

D Complements to Section 6

We provide in this section additional experimental results. average tree 0 tree 1 tree 2 tree 3 tree 4 tree 5 tree 6 tree 7 tree 8 tree 9 tree 10 tree 11 tree 12 tree 13 tree 14 Fig. 7: Computation time of the online algorithm for each random tree.

  Time to compute ⌊H⌋.

Fig. 3 :

 3 Fig. 3: Space and time consumption for computing ⌊H⌋ on 50 VPAs of various densities, |Q| = 10, |Σ| = |Γ | = 3, and timeout of 60s.

  and several parameters vary: the sizes |Q|, |Σ| and |Γ |, the density of final states |Q f |

Table 2 :

 2 VPA id Response Time (s.) | ⌊H⌋ | |Reach(u)| | ⌊Safe(u)⌋ | q20-a02-x02-o16-c16-f0.5-00 right-universal w.r.t. a1 0.03 3 4 33 q20-a02-x04-o16-c16-f0.5-02 right-universal w.r.t. a1 0.07 3 8 53 q20-a02-x04-o16-c16-f0.5-06 right-universal w.r.t. a0 0.06 3 5 54 q20-a03-x02-o16-c16-f0.5-06 right-universal w.r.t. a2 0.13 12 4 32 q20-a03-x03-o16-c16-f0.5-06 right-universal w.r.t. a0 0.37 23 4 59 q20-a03-x03-o16-c16-f0.5-09 right-universal w.r.t. a2a0 1.74 13 14 179 q20-a03-x04-o16-c16-f0.5-07 right-universal w.r.t. a2 1.02 44 5 116 q20-a04-x02-o16-c16-f0.5-03 right-universal w.r.t. a3 0-x02-o16-c16-f0.5-07 right-universal w.r.t. a0 1-x03-o16-c16-f0.5-03 right-universal w.r.t. a2 15Time and data structures size on random VPAs, with transition density of 16, |Q| = 20, |Σ| = |Γ | ∈ {2, 3, 4}, and timeout of 300s.

  Reach(u) average time Safe(u) average time LSafe(u) average time ⌊H⌋ average time (a) With the ⌊H⌋ average time curve. Reach(u) average time Safe(u) average time LSafe(u) average time (b) Without the ⌊H⌋ average time curve.

Fig. 4 :

 4 Fig. 4: Average time for computing Safe(u), LSafe(u) and Reach(u) and overall computation for 15 random trees.

Lemma 4 .

 4 C is an a-predecessor of Post a (C ).If C ∈ Pred a (C ′ ), then C ′ ⊆ Post a (C ). Both properties also hold for Post [h] (C ).The proof of Proposition 1 is then the following one.Proof (ofProposition 1). (3, ⇒) Let C ∈ LSafe(ua). Then by Proposition 2, Post a (C ) ∈ Safe(u). Moreover, C is an a-predecessor of Post a (C ) by Lemma 4. (3, ⇐) Let C be an a-predecessor of C ′ , with C ′ ∈ Safe(u). By Lemma 4, C ′ ⊆ Post a (C ). As Safe(u) is ⊆-upward closed, we also have Post a (C ) ∈ Safe(u), so C ∈ LSafe(ua) by Proposition 2. (4) Same proofs, except that a has to be replaced by h, for all h ∈ H Σ . ⊓ ⊔ B Complements to Section 4 B.1 Proof of Lemma 2

Figure 5 Fig. 5 :

 55 Figure5illustrates the construction. The set C 0 is an a-predecessor of C ′ 0 , so us-

C. 2

 2 Proof of Equation (13)(⊇) Let C ∈ ⌊(A ∩ B) ∪ (A \ B ⊔ B \ A)⌋. Then C ∈ A ⊔ B. For contradiction, let us assume that there exists C ′ C such that C ′ ∈ ⌊A ⊔ B⌋. If C ′ ∈ A ∩ B, then C ′ ∈ (A ∩ B) ∪ (A \ B ⊔ B \ A), which contradicts C . So C ′ / ∈ A ∩ B, and assume wlog that C ′ = a ∪ b with a ∈ A \ B and b ∈ B (recall that a, b are non empty sets by definition of ⊔ operator). If b ∈ A, then b ∈ A ∩ B ⊆ A ⊔ B and b C ′ , but this contradicts C ′ . If b / ∈ A, then C ′ ∈ A \ B ⊔ B \ A, so C ′ ∈ A ∩ B ∪ (A \ B ⊔ B \ A), and C ′ C , which contradicts C . (⊆) Let C ∈ ⌊A ⊔ B⌋. Let us first show that C ∈ (A ∩ B) ∪ (A \ B ⊔ B \ A). If C ∈ A ∩ B this is direct. Otherwise C = a ∪ b with a ∈ A \ B and b ∈ B (the other case is symmetric). If b ∈ A then b ∈ A ∩ B ⊆ A ⊔ B and b C , which contradicts the definition of C . So b ∈ B \ A, and C ∈ A \ B ⊔ B \ A.Secondly, assume for contradiction that there existsC ′ C such that C ′ ∈ ⌊(A ∩ B) ∪ (A \ B ⊔ B \ A)⌋.Then, according to (⊇), C ′ ∈ ⌊A ⊔ B⌋, which contradicts the definition of C . We get the next corollary of Equation (13): Corollary 2. If A ⊆ B, then ⌊A ⊔ B⌋ = ⌊A⌋. C.3 Safe(a) and Operator ⊔

  3. Assume that there exists C * ∈h∈⌊H⌋ A h \ ⌊S⌋. By 1., there exists C in ⌊S⌋ such that C C * ; and by 2., there existsC ′ ∈ h∈⌊H⌋ A h such that C ′ ⊆ C C * incontradiction with the definition of C * . Therefore h∈⌊H⌋ A h ⊆ ⌊S⌋. 4. Let C ∈ ⌊S⌋. By 2., there exists C ′ ∈ h∈⌊H⌋ A h such that C ′ ⊆ C . By 3., it follows that C = C ′ and thus ⌊S⌋ ⊆ h∈⌊H⌋ A h . In conclusion, ⌊Safe(a)⌋ = ⌊S⌋ = h∈⌊H⌋ A h ⊓ ⊔ C.4 Step 2 with SAT Solvers

Fig. 6 :

 6 Fig. 6: Execution time of the membership algorithm for a binary tree t 0 of increasing height.

Figure 6

 6 Figure6indicates the execution time of the membership algorithm for a random complete binary tree t 0 of increasing height.

Table 1 :

 1 Number for each type (universal, right-universal, null rel h , timeout) among 90 instances, with a timeout of 300s, and various number of states and transition densities. Average (preprocessing/online) time is given in parentheses (in s).

	universality	right-universality	null rel h	timeout	(preproc.)	timeout	(online)
	tr. density: 8 tr. density: 16	8	16	8 16 8 16 8 16
	10 12 (0.59/0.01) 40 (1.19/0.01) 22 (16.62/9.36) 44 (11.00/1.10) 52 (0.67/0.01) 0 2 2 2 4
	20 13 (9.35/0.01) 29 (0.86/0.01) 14 (20.44/30.85) 41 (5.18/1.07) 46 (9.62/0.01) 0 14 17 3 3
	30 9 (20.22/0.01) 34 (13.39/0.01) 11 (21.23/5.85) 34 (27.31/3.43) 40 (1.23/0.01) 0 30 21 0 1

  and thus both C and ⌊Safe(u)⌋ are finite. The same arguments hold for proving that ⌊LSafe(u)⌋ is finite and contains only finite sets of configurations.

	⊓ ⊔
	B.4 Proof of Implication (6)

VPAs considered in this article are tree acceptors, with acceptance on empty stack.

This notion of universality is different from the one proposed for usual VPAs, where a VPA is universal if it accepts all words of (Σ ∪ Σ) * (and not only linearizations of trees).

[t0] is the trace w of Algorithm 1.

The name "leaf-safe" comes from the fact that we only consider suffixes starting with a Σ symbol, and thus continuations of the tree that do not add children to the current node.

equal to the number of outgoing transitions per state and per symbol.

to deal with managable and not too small sets ⌊H⌋.

This means that the automaton is never right-universal w.r.t. u, for any proper prefix u of [t0]. Therefore, in such cases, our algorithm is slower that the membership algorithm.

Acknowledgements

We thank Grégoire Sutre for useful discussions, and the QuiXProc team for translating XPath expressions of our benchmark to VPAs. We also thank one of the reviewers who helped us to improve the presentation of this article. The second author is supported by a grant from FRIA. This work was also partially supported by CNRS SOSP project.

if h is a hedge and a ∈ Σ, then aha is a hedge, and rel aha (q) is the set of states q ′ such that there exists γ ∈ Γ verifying:

(q, ǫ) a -→ (p, γ) and (p ′ , γ) a -→ (q ′ , ǫ) with p ′ ∈ rel h (p).

Algorithm 3 uses the variables ToProcess and Functions with the following meaning. Functions contains initially the identity relation id Q ; at the end of the computation, it contains all functions rel h , for h ∈ H Σ . ToProcess contains all the newly constructed functions, and these functions are used to create other new functions as described in the previous definition by induction.

Algorithm 3 Computing all functions rel h , for h ∈ H Σ .

function HedgeFunctions(A) Proof. Let Functions be the set computed by Algorithm 3. Clearly, Functions ⊆ {rel h | h ∈ H Σ }. Assume for contradiction that there exists r = rel h with h ∈ H Σ such that r ∈ Functions. Clearly, r = id Q , and we can suppose wlog that either

or there exists r ′ ∈ Functions such that for all q, r(q) is the set of q ′ with q a:γ --→ p ∈ ∆, p ′ a:γ --→ q ′ ∈ ∆ and p ′ ∈ r ′ (p). Consider the first case. When they have been constructed by Algorithm 3, both r ′ 1 and r ′ 2 have been added to ToProcess and to Functions. After the last element (among r ′ 1 and r ′ 2 ) is popped from ToProcess, then r = r ′ 2 • r ′ 1 is built during the loop on f ∈ Functions, which leads to a contradiction. We also have a contradiction in the second case by considering the loop on a ∈ Σ.

⊓ ⊔


Keywords: Event-based control, Nonlinear systems, Time delay, Stabilization

 and previously extended to event-based control of nonlinear undelayed systems. Under the assumption of the existence of a control Lyapunov-Krasovsky functional, it enables smooth (except at the origin) asymptotic stabilization while ensuring that the sampling intervals do not contract to zero. Global asymptotic stability is obtain under the small control property assumption. Moreover, the control can be proved to be smooth anywhere under certain conditions. Some simulation results highlight the ability of the proposals.

INTRODUCTION

The classical (time-triggered) discrete time framework of controlled systems consists in sampling the system uniformly in time with a constant sampling period. This field has been widely investigated for linear systems, see [START_REF] Åström | Computer-Controlled Systems[END_REF] and the references therein. In the case of nonlinear systems, one way to address a discretetime feedback is to implement a continuous time control algorithm with a sufficiently small sampling period (this procedure is denoted as emulation). However, the hardware used to sample and hold the plant measurements or compute the feedback control action may make impossible the reduce of the sampling period to a level that guarantees acceptable closed-loop performance, as demonstrated in [START_REF] Hsu | The effect of discretized feedback in a closed loop system[END_REF]. Furthermore, although periodicity simplifies the design and analysis, it results in a conservative usage of resources since the control law is computed and updated at the same rate regardless it is really required or not. Some works hence recently addressed resource-aware implementations of the control law, where the control law is event-driven.

Other way to tackle the problem of discrete-time control for nonlinear systems is the application of sampled-data control algorithms based on an approximated discrete-time model of the process, like in [START_REF] Nešić | A framework for stabilization of nonlinear sampled-data systems based on their approximate discrete-time models[END_REF], which is not a trivial task. Another proposed approach consists in modifying a continuous time stabilizing control using a general formula to obtain a redesigned control suitable for sampled-data implementation, as done in [START_REF] Nešić | Lyapunov-based continuous-time nonlinear controller redesign for sampled-data implementation[END_REF]. Some event-triggered control approaches have also been suggested as a solution to overcome such drawbacks of emulation, redesigned control and complexity of the underlying nonlinear sampled-data models.

The advantages of an event-based controller over a timebased one are mainly influenced by the way in which the event are generated. Typical event-based detection mechanisms are functions of the state variation (or the output) of the system, like in Årzén (1999); [START_REF] Sandee | Event-driven control as an opportunity in the multidisciplinary development of embedded controllers[END_REF]; [START_REF] Durand | Further results on event-based PID controller[END_REF]; Sánchez et al. (2009b,a). Although the event-triggered control is well-motivated and allows to relax the periodicity of computations, only few works report theoretical results about the stability, convergence and performance. In [START_REF] Åström | Comparison of Riemann and Lebesque sampling for first order stochastic systems[END_REF] in particular, it is proved that such an approach reduces the number of sampling instants for the same final performance. Some stability and robustness proprieties are exploited in [START_REF] Åström | Comparison of Riemann and Lebesque sampling for first order stochastic systems[END_REF]; [START_REF] Heemels | Analysis of event-driven controllers for linear systems[END_REF]; [START_REF] Lunze | A state-feedback approach to event-based control[END_REF]; [START_REF] Donkers | Outputbased event-triggered control with guaranteed l inf -gain and improved event-triggering[END_REF]; [START_REF] Eqtami | Event-triggered control for discrete-time systems[END_REF]. An alternative approach consists in taking events related to the variation of a Lyapunov function -and consequently to the state too -between the current state and its value at the last sampling, like in [START_REF] Velasco | On Lyapunov sampling for event-driven controllers[END_REF], or in taking events related to the time derivative of the Lyapunov function, like in [START_REF] Tabuada | Event-triggered real-time scheduling of stabilizing control tasks[END_REF]; [START_REF] Anta | Self-triggered stabilization of homogeneous control systems[END_REF]; [START_REF] Marchand | A general formula for the stabilization of event-based controlled systems[END_REF][START_REF] Marchand | A general formula for event-based stabilization of nonlinear systems[END_REF]. More particularly, the work in [START_REF] Marchand | A general formula for event-based stabilization of nonlinear systems[END_REF] is based on the universal formula of [START_REF] Sontag | A "universal" construction of Artstein's theorem on nonlinear stabilization[END_REF]. An event-based stabilization of general nonlinear systems affine in the input is proposed. The control updates ensure the strict decrease of a control Lyapunov function (CLF), and so is asymptotically stable the closed-loop system.

Eventually, the event-based control scheme is of growing interest in embedded and networked control systems (where the control loop is closed over a communication link) because it allows to reduce the sending/receiving of information needed for control and, consequently, a strong energy saving. A network has several advantages, like flexibility in the configuration of the communication structure and the number of systems. However, it also has a considerable impact on the performance, notably because of communication delays and packet losses which avoid real-time control constraints to be meet and can even cause the instability of the control loop. This is why it is also important to consider time-delays in the eventbased approaches (note that the packet loss issue is not considered here). Only few works deal with this topic for linear systems, like in Lehmann andLunze (2011, 2012); [START_REF] Guinaldo | Distributed event-triggered control with network delays and packet losses[END_REF][START_REF] Durand | Event-based stabilization of linear system with communication delays in the measurements[END_REF]. Nonetheless, in the best knowledge of the authors, this is the first time an event-based control strategy is proposed for general nonlinear time-delay systems.

The concept of CLF, which is a useful tool for designing robust control laws for nonlinear (undelayed) systems, has been extended to time-delay systems in the form of control Lyapunov-Razumikhin functions (CLRF) and control Lyapunov-Krasovsky functionals (CLKF), see [START_REF] Jankovic | Control Lyapunov-Razumikhin functions to time-delay systems[END_REF][START_REF] Jankovic | Extension of control Lyapunov functions to time-delay systems[END_REF][START_REF] Jankovic | Control of nonlinear systems with time-delay[END_REF]. The latter form is more flexible and easier to construct than CLRFs. Moreover, if a CLKF is known for a nonlinear time-delay system, several stabilizing control laws can be constructed using one of the universal formulas derived for CLFs (such as the Sontag's formula for instance) to achieve global asymptotic stability of the closed loop system. In the present paper, we hence propose to extend the universal event-based formula of [START_REF] Marchand | A general formula for event-based stabilization of nonlinear systems[END_REF] for the stabilization of affine in the control nonlinear time-delay systems. The class of time-delay systems under consideration is restricted here to depend on some discrete delays and a distributed delay. Note also that we only consider state delays and do not consider delays in the control signal (input delays).

The rest of the document is organized as follows. In section 1, some definitions are introduced and the problem is stated. The main contribution is then presented in section 2. The smooth control particular case is also concerned and an example is depicted. An analysis finally concludes the paper.

PRELIMINARIES

Event-triggered stabilization of nonlinear systems

Let consider the general nonlinear dynamical system

ẋ(t) = f x(t), u(t) (1)
with x(0) := x 0 with x(t) ∈ X ⊂ R p , u(t) ∈ U ⊂ R q and f is a Lipschitz function vanishing at the origin. Note that only null stabilization is considered in this paper for the sake of simplicity, and the dependence on t can be omitted in the sequel. Also, let define X * := X \{0} hereafter. Definition 1.1. (Event-based feedback).

By event-based feedback we mean a set of two functions, that are i) an event function ǫ : X × X → R that indicates if one needs (when ǫ ≤ 0) or not (when ǫ > 0) to recompute the control law and ii) a feedback function υ : X → U .

The solution of (1) with event-based feedback (ǫ, υ) starting in x 0 at t = 0 is then defined as the solution of the differential system

ẋ(t) = f x(t), υ(x i ) ∀t ∈ [t i , t i+1 [ (2) with x i := x(t i ) (3)
where the time instants t i , with i ∈ N, are considered as events (they are determined when the event function ǫ vanishes and denote the sampling time instants) and x i is the memory of the state value at the last event. With this formalization, the control value is updated each time ǫ becomes negative. Usually, one tries to design an eventbased feedback so that ǫ cannot remain negative (and so is updated the control only punctually). In addition, one also wants that two events are separated with a non vanishing time interval avoiding the Zeno phenomenon. All these properties are encompassed with the Minimal inter-Sampling Interval (MSI) property introduced in [START_REF] Marchand | A general formula for event-based stabilization of nonlinear systems[END_REF]. In particular: Property 1.2. (Semi-uniformly MSI). An event-triggered feedback is said to be semi-uniformly MSI if and only if the inter-execution times can be below bounded by some non zero minimal sampling interval τ (δ) > 0 for any δ > 0 and any initial condition x 0 in the ball B(δ) centered at the origin and of radius δ. Remark 1.3. A semi-uniformly MSI event-driven control is a piecewise constant control with non zero sampling intervals (useful for implementation purpose).

A particular event-based feedback has been proposed in [START_REF] Marchand | A general formula for event-based stabilization of nonlinear systems[END_REF], based on the universal formula of [START_REF] Sontag | A "universal" construction of Artstein's theorem on nonlinear stabilization[END_REF]. In order to then understand how was built this strategy, we first recall some seminal results for the stabilization of continuous-time systems. Let consider the affine in the control nonlinear dynamical system A smooth and positive definite functional V : X → R is a control Lyapunov function (CLF) for system (4) if for each x = 0 there is some u ∈ U such that

ẋ(t) = f x(t) + g x(t) u(t) (4
α(x) + β(x)u < 0 (5) with α(x) := L f V (x) = ∂V ∂x f (x) β(x) := L g V (x) = ∂V ∂x g(x)
where L f V and L g V are the Lie derivatives of f and g functions respectively.

Property 1.5. (Small control property).

If for any µ > 0, ε > 0 and x in the ball B(µ)\{0}, there is some u with u ≤ ε such that inequality (5) holds, then it is possible to design a feedback control that asymptotically stabilizes the system [START_REF] Sontag | A "universal" construction of Artstein's theorem on nonlinear stabilization[END_REF]). Theorem 1.6. (Sontag's universal formula).

Assume that system (4) admits V as a CLF. For any real analytic function q : R → R such that q(0) = 0 and bq(b) > 0 for b = 0, let φ : R 2 → R be defined by

φ(a, b) := a + a 2 + bq(b) b if b = 0 0 if b = 0 (6)
Then, the feedback υ : X → U , smooth on X * , defined by

υ(x) := -β(x) φ α(x), β(x) 2 (7)
with α(x) and β(x) defined in ( 5), is such that ( 5) is satisfied for all x ∈ X * . Property 1.7. If the CLF V in Theorem 1.6 satisfies the small control property, then taking q(b) = b in φ in ( 6), the control is continuous at the origin and so is globally asymptotically stable the closed-loop system.

The event-based feedback suggested in [START_REF] Marchand | A general formula for event-based stabilization of nonlinear systems[END_REF] is based on such an approach, where the control law υ is similar to the one in (7) (but with a lightly different function φ) and the event function ǫ is related to the time derivative of the CLF in order to ensure a (global) asymptotic stability of the closed-loop system. In this paper, we propose to extend this event-based feedback for the stabilization of nonlinear time-delay systems. Actually, the construction is quite similar, this is why we do not detail the event-based feedback for nonlinear undelayed systems here.

Stabilization of time-delay systems

Hereafter, the state of a time-delay system is described by x d : [-r, 0] → X defined by x d (t)(θ) = x(t + θ). This notation, used in [START_REF] Jankovic | Extension of control Lyapunov functions to time-delay systems[END_REF] in particular, seems more convenient than the more conventional x t (θ). Note that the dependence on t and θ can be omitted in the sequel for the sake of simplicity, writing x d (θ) -or only x d -instead of x d (t)(θ) for instance. Let consider the affine in the control nonlinear dynamical time-delay system

ẋ = f (x d ) + g(x d )u (8) with x d (0)(θ) := χ 0 (θ)
where f , g are smooth functions and χ 0 : [-r, 0] → X is a given initial condition. Note that the class of time-delay system under consideration has been restricted to depend on l discrete delays and a distributed delay in the form

ẋ = Φ(x τ ) + g(x τ )u (9) with Φ(x τ ) := f 0 (x τ ) + 0 -r Γ(θ)F x τ , x(t + θ) dθ and x τ := x, x(t -τ 1 ), . . . , x(t -τ l )
where f 0 , g and F : R (l+2)p → R Γ are smooth functions of their arguments. Without loss of generality, we assume that F (x τ , 0) = 0. The matrix Γ : [-r, 0] → R p×Γ is assumed to be piecewise continuous (hence, integrable) and bounded.

Remark 1.8. The restriction (9) on this class of delay systems is needed to avoid the problems that arise due to non-compactness of closed bounded sets in the space C([-r, 0], X , • ), where C([-r, 0], X ) denotes the space of continuous functions from [-r, 0] into X . This is discussed in [START_REF] Jankovic | Control Lyapunov-Razumikhin functions to time-delay systems[END_REF][START_REF] Jankovic | Extension of control Lyapunov functions to time-delay systems[END_REF]. Remark 1.9. Note that we do not consider input delays of the form u(tτ ) in this paper. However, the control law is computed using the state x d of the time-delay system. Definition 1.10. (Control Lyapunov-Krasovsky functional).

A smooth functional V : X → R of the form

V (x d ) = V 1 (x) + V 2 (x d ) + V 3 (x d ) (10) with V 2 (x d ) = l j=1 0 -τj S j (x(t -ς))dς V 3 (x d ) = 0 -r t t+θ L(θ, x(ς))dςdθ
where V 1 is a smooth, positive definite, radially unbounded function of the current state x, V 2 and V 3 are nonnegative functionals respectively due to the discrete delays and the distributed delay in (9), S j : X → R and L : R + × X → R are nonnegative integrable functions, smooth in the x-argument, is a control Lyapunov-Krasovsky functional (CLKF) for system (9) if there exist a function λ, with λ(s) > 0 for s > 0, and two class K ∞ functions κ 1 and κ 2 such that

κ 1 (|χ 0 |) ≤ V (χ d ) ≤ κ 2 ( χ d ) and β d (χ d ) = 0 ⇒ α d (χ d ) ≤ -λ(|χ 0 |) (11) with α d (x d ) := L * f V (x d ) β d (x d ) := L g V 1 (x d )
for all piecewise continuous functions χ d : [-r, 0] → X , where χ 0 is defined in (8). Remark 1.11. Whereas the classical Lie derivative notation is used in

L g V 1 (x) = ∂V1 ∂x g(x)
for the part function of the current state x, an extended Lie derivative is required for functionals of the form (10). L * f V , initially defined in [START_REF] Jankovic | Extension of control Lyapunov functions to time-delay systems[END_REF], comes from the time derivative of the CLKF V in (10) along trajectories of the system (9), that is

V = ∂V 1 ∂x Φ + ∂V 1 ∂x gu + l j=1 S j (x) -S j (x(t -τ j )) + 0 -r L(θ, x) -L(θ, x(t + θ)) dθ = L * f V (x d ) + L g V 1 (x d )u = α d (x d ) + β d (x d )u
(12) when using the notation in (11), where Φ is defined in (9), which gives

L * f V (x d ) := L Φ V 1 + l j=1 S j (x) -S j (x(t -τ j )) + 0 -r L(θ, x) -L(θ, x(t + θ)) dθ
The Sontag's universal formula (Theorem 1.6) has been extended in [START_REF] Jankovic | Extension of control Lyapunov functions to time-delay systems[END_REF] for the stabilization of nonlinear time-delay systems (9) with a CLKF of the form (10). This can be summarized as follows: Theorem 1.12. (Sontag's universal formula with CLKF).

Assume that system (9) admits a CLKF of the form (10). For any real analytic function q : R → R and φ : R 2 → R, both defined in Theorem 1.6, let the feedback υ : X → U, smooth on X * , defined by

υ(x d ) := -β d (x τ ) φ α d (x d ), β d (x d ) 2 (13)
with x τ and α d , β d defined in ( 9) and ( 11) respectively.

Then υ is such that ( 11) is satisfied for all non zero piecewise continuous functions χ d : [-r, 0] → X . Property 1.13. If the CLKF V in Theorem 1.12 satisfies the small control property, then taking q(b) = b in φ in ( 6), the control is continuous at the origin and so is globally asymptotically stable the closed-loop system.

Contribution of the paper

In the present paper, we propose to extend the event-based approach previously developed in [START_REF] Marchand | A general formula for event-based stabilization of nonlinear systems[END_REF] for nonlinear time-delay systems admitting a CLKF.

In the sequel, let

x di := x d (t i ) (14)
be the memory of the delayed state value at the last event, by analogy with (3).

EVENT-BASED STABILIZATION OF NONLINEAR TIME-DELAY SYSTEMS

It is possible to design an event-based feedback control that asymptotically stabilizes time-delay systems (9) with a CLKF of the form (10): Theorem 2.1. (Event-based universal formula with CLKF).

If there exists a CLKF V of the form (10) for system (9), then the event-based feedback (ǫ, υ) -see Definition 1.1defined by

υ(x d ) = -β d (x τ )∆(x τ )γ(x d ) (15) ǫ(x d , x di ) = -α d (x d ) -β d (x d )υ(x di ) -σ α d (x d ) 2 + θ(x d )β d (x d )∆(x d )β d (x d ) T (16)
with

• α d and β d as defined in (11)

• ∆ : X * → R q×q and θ : X → R are smooth positive definite functions

• γ : X → R is defined by γ(x d ) :=      α d (x d ) + α d (x d ) 2 + θ(x d )β d (x d )∆(x d )β d (x d ) T β d (x d )∆(x d )β d (x d ) T if x d ∈ S d 0 if x d / ∈ S d (17) • S d := {x d ∈ X | β d (x d ) = 0} • σ ∈ [0, 1[ is a tunable parameter
where x di and x τ are defined in ( 14) and ( 9) respectively, is semi-uniformly MSI, smooth on X * and such that the time derivative of V satisfies (11) ∀x ∈ X * . Remark 2.2. The simplification made with respect to the original result in [START_REF] Marchand | A general formula for event-based stabilization of nonlinear systems[END_REF] (for the stabilization of nonlinear undelayed systems) resides in the assumptions made for the functions θ and ∆, that are more restrictive here whereas they are assumed to be definite only on the set S d in the original work.

Remark 2.3. The idea behind the construction of the event-based feedback ( 15)-( 16) is to compare the time derivative of the CLKF V in the event-based case, that is applying υ(x di ), and in the classical case, that is applying υ(x d ) instead of υ(x di ). The event function is the weighted difference between both, where σ is the weighted value. By construction, an event is enforced when the event function ǫ vanishes to zero, that is hence when the stability of the event-based scheme does not behave as the one in the classical case. Also, the convergence will be faster with higher σ but with more frequent events in return. σ = 0 means updating the control when V = 0.

Also, some properties are inherited from [START_REF] Marchand | A general formula for event-based stabilization of nonlinear systems[END_REF] and complete the Theorem 2.1. In particular: Property 2.4. (Global asymptotic stability).

If the CLKF V in Theorem 2.1 satisfies the small control property, then the event-based feedback ( 15)-( 16) is continuous at the origin and so is globally asymptotically stable the closed-loop system. Property 2.5. (Smooth control).

If there exists some smooth function ω :

X → R + such that on S * d := S d \{0} ω(x d )β d (x d )∆(x d )β d (x d ) T -α d (x d ) > 0
then the control is smooth on X as soon as θ(x d ) ∆(x d ) vanishes at the origin with

θ(x d ) := ω(x d ) 2 β d (x d )∆(x d )β d (x d ) T -2α d (x d )ω(x d ) (18)

Proofs

Proof of Theorem 2.1 The proof follows the one developed in [START_REF] Marchand | A general formula for event-based stabilization of nonlinear systems[END_REF] for event-based control of systems without delays (4). First, let define

ψ(x) := α d (x) 2 + θ(x)β d (x)∆(x)β d (x) T (19)
for the lake of simplicity in the sequel.

We begin establishing γ is smooth on X * . For this, consider the algebraic equation

P (x d , ζ) := β d (x d )∆(x d )β d (x d ) T ζ 2 -2α d (x d )ζ -θ(x d ) = 0 (20) Note first that ζ = γ(x) is a solution of (20) for all x d ∈ X .
It is easy to prove that the partial derivative of P with respect to ζ is always strictly positive on 21) by the expression of γ (since ζ = γ(x) is a solution of ( 20)). Therefore ∂P ∂ζ never vanishes at each point of the form {(x d , γ(x d ))|x d ∈ X * }. Furthermore, P is smooth w.r.t. x d and ζ since so are α d , β d , θ and ∆. Hence, using the implicit function theorem, γ is smooth on X * .

X * ∂P ∂ζ := 2β d (x d )∆(x d )β d (x d ) T ζ -2α d (x d ) (21) Indeed, when β d (x d ) = 0, (11) gives ∂P ∂ζ = -2α d (x d ) ≥ 2λ(|χ 0 |) > 0 and when β d (x d ) = 0, (17) gives ∂P ∂ζ = 2 α d (x d ) 2 + θ(x d )β d (x d )∆(x d )β d (x d ) T > 0 replacing ζ in (
The decrease of the CLKF of the form (10) when applying the event-based feedback ( 15)-( 16) is easy to prove. For this, let us consider the time interval [t i , t i+1 ], that is the interval separating two successive events. Recall that x di denotes the value of the state when the i th event occurs and t i the corresponding time instant, as defined in (14). At time t i , when the event occurs, the time derivative of the CLKF, i.e. ( 12), after the update of the control is

dV dt (x di ) = α d (x di ) + β d (x di )υ(x di ) = -ψ(x di ) < 0
when substituting ( 17) in ( 15), where ψ is defined in (19). More precisely, defining a compact set not containing the origin, that is

Ω = {x d ∈ CP ([-r, 0], X ) : d ≤ x d ≤ D},
where CP ([-r, 0], X ) denotes the space of piecewise continuous functions from [-r, 0] into X , d and D are some constant in R + . If V is a CLKF for the system of the form ( 9) then for all 0 < δ < D there exists ε > 0 such that

α d (χ d ) ≥ -1 2 λ(|χ 0 |) ⇒ |β d (χ d )| ≥ ε for χ d ∈ Ω.
As a consequence, one obtains (see Lemma 1 in [START_REF] Jankovic | Extension of control Lyapunov functions to time-delay systems[END_REF], and [START_REF] Jankovic | Control Lyapunov-Razumikhin functions to time-delay systems[END_REF], for further details)

V ≤ -λ(|x|)
With this updated control, the event function ( 16) hence becomes strictly positive

ǫ(x di , x di ) = (1 -σ)ψ(x di ) > 0 since σ ∈ [0, 1[,
where ψ is defined in (19). Furthermore, the event-function necessarily remains positive before the next event by continuity, because an event will occur when ǫ(x d , x di ) = 0 (see Definition 1.1). Therefore, on the interval [t i , t i+1 ], one has

ǫ(x d , x di ) = -α d (x d ) -β d (x d )υ(x di ) -σψ(x d ) = - dV dt (x d ) -σψ(x d ) ≥ 0
which ensures the decrease of the CLKF on the interval since σψ(x d ) ≥ 0, where ψ is defined in (19). Moreover, t i+1 is necessarily bounded since, if not, V should converge to a constant value where dV dt = 0, which is impossible thanks to the inequality above. The event function precisely prevents this phenomena detecting when dV dt is close to vanish and updates the control if it happens, where σ is a tunable parameter fixing how "close to vanish" has to be the time derivative of V .

To prove that the event-based control is MSI, we have to prove that for any initial condition in a priori given set, the sampling intervals are below bounded. First of all, notice that events only occur when ǫ becomes negative (with x d = 0). Therefore, using the fact that when 22) when using the definition of υ(x d ) in ( 15) and ( 17), where ψ is defined in (19). Let us define for x di ∈ S d , the level ϑ i := V (x di ) and the set

β d (x d ) = 0, α d (x d ) < -λ(|χ 0 |) (because V is a CLKF as defined in Definition 1.10), it follows from (16), on {x d ∈ X * | β d (x d ) = 0}, that ǫ(x d , x di ) = -α d (x d ) -σ|α d (x d )| = (1 -σ)λ(|χ 0 |) > 0 because σ ∈ [0,
dV dt (x d ) = α d (x d ) + β d (x d )υ(x di ) = -ψ(x d ) + β d (x d ) υ(x di ) -υ(x d ) (
V ϑi := {x d ∈ X |V (x d ) ≤ ϑ i }.
From the choice of the event function, it follows from ( 22) that x d belongs to V ϑ ⊂ V ϑi . Note that if x di belongs to S d , this is not necessarily the case for x d that can escape from this set. First see that, since i) θ(x d ) is such that

α d (x d ) 2 + θ(x d )β d (x d )∆(x d )β d (x d ) T > 0 for all x d ∈ S *
d , and ii) α d (x d ) is necessarily nonzero on the frontier of S d (except possibly at the origin)

dV dt (x di ) = -ψ(x di ) ≤ - inf x di ∈S d s.t. V (x di )=ϑ i ψ(x di ) =: -ϕ(ϑ i ) < 0 (23)
Considering now the second time derivative of the CLKF

V (x d ) = ∂α d ∂x d (x d ) + υ(x di ) T ∂β T d ∂x d (x d ) Θ(x d , x di ) (24)
with Θ(x d , x di ) := Φ(x τ ) + g(x τ )υ(x di ) where Φ is defined in (9). By continuity of all the involved functions (except for Γ in Φ which is piecewise continuous but bounded by assumption), both terms can be bounded for all x d ∈ V ϑi by the following upper bounds ̺ 1 (ϑ i ) and

̺ 2 (ϑ i ) such that ̺ 1 (ϑ i ) := sup x di ∈S d s.t. V (x di )=ϑi x d ∈V ϑ i ∂α d ∂x d (x d ) +υ(x di ) T ∂β T d ∂x d (x d ) ̺ 2 (ϑ i ) := sup x di ∈S d s.t. V (x di )=ϑi x d ∈V ϑ i Θ(x d , x di )
where Θ is defined in (24). Therefore, V is strictly negative at any event instant t i and cannot vanish until a certain time τ (ϑ i ) is elapsed (because its slope is positive). This minimal sampling interval is only depending on the level ϑ i . A bound on τ (ϑ i ) is given by the inequality

dV dt (x d ) ≤ dV dt (x di ) + ρ 1 ρ 2 (t -t i ) x ∈ V ϑi that yields τ (ϑ i ) ≥ ϕ(ϑ i ) ̺ 1 (ϑ i )̺ 2 (ϑ i ) > 0
where ϕ is defined in (23). As a consequence, the eventbased feedback ( 15)-( 16) is semi-uniformly MSI.

Proof of Property 2.4

To prove the continuity of υ at the origin, one only needs to consider the points in S since we already have υ(x d ) = 0 if β d (x d ) = 0. From (15), we have

υ(x d ) ≤ |α d (x d )| β d (x d )∆(x d )β d (x d ) T ∆(x d )β d (x d ) T + ψ(x d ) β d (x d )∆(x d )β d (x d ) T ∆(x d )β d (x d ) T ≤ 2|α d (x d )| β d (x d )∆(x d )β d (x d ) T ∆(x d )β d (x d ) T + θ(x d ) ∆(x d )
(25) With the small control property (see Property 1.5), for any ε > 0, there is µ > 0 such that for any x d ∈ B(µ)\{0}, there exists some u with u ≤ ε such that L

* f V (x d ) + [L g V 1 (x d )] T u = α d (x d ) + β d (x d )u < 0 and therefore |α d (x d )| < β d (x d ) ε. It follows: υ(x d ) ≤ 2ε β d (x d ) ∆(x d )β d (x d ) T β d (x d )∆(x d )β d (x d ) T + θ(x d ) ∆(x d ) Since the function (v 1 , v 2 ) → v1 v2 v T 1 v2
is continuous with respect to its two variables at the origin where it equals 1, since θ and ∆ are also continuous, since θ(x d ) ∆(x d ) vanishes at the origin, for any ε ′ , there is some µ ′ such that ∀x d ∈ B(µ ′ )\{0}, υ(x d ) ≤ ε ′ which ends the proof of continuity.

Proof of Property 2.5

Finally, with θ as in (18), the control becomes υ(x d ) = -β d (x d )∆(x d )ω(x d ) which is obviously smooth on X .

Example

Consider the nonlinear time-delay system

ẋ1 = u ẋ2 = -x 2 + x 2d + x 3 1 + u (26)
with x 2d := x 2 (tτ ) that admits a CLKF (proposed in [START_REF] Jankovic | Extension of control Lyapunov functions to time-delay systems[END_REF])

V (x) = 1 2 (x 2 1 + x 2 2 ) + 1 2 0 -τ
x 2 2 (θ)dθ ( 27)

with α d = x 2 (-x 2 + x 2d + x 3 1 ) + 1 2 (x 2 2 -x 2 2d ) β d = x 1 + x 2
Indeed, setting, λ(|x|) = 1 4 |x| 4 , one obtains

β d = 0 ⇒ x 1 = -x 2 ⇒ α d = - 1 2 (x 2 -x 2d ) 2 -x 4 2 ≤ -x 4 2 ≤ -λ(|x|)
which proves that ( 27) is a CLKF for (26) using Definition 1.10.

The time evolution of x, υ(x) and the event function ǫ(x, x i ) is depicted in Fig. 1, for ∆ = I p (the identity matrix), θ(x) is as defined in (18) (for smooth control everywhere), with ω = 0.1, σ = 0.1, x 0 = (1 -2) T and a time delay τ = 2 s. One could remark that only 5 events occurs in the 20 s simulation time (including the first event at t = 0) when applying the proposed eventbased approach (15)-( 16).

CONCLUSION

In this paper, we proposed an extension of the Sontag's universal formula for event-based stabilization of nonlinear time-delay systems. Whereas the original work deals with control Lyapunov functions, some control Lyapunov-Krosovsky functionals (CLKF) are now required for a global (except at the origin) asymptotic stabilization of systems with state delays. The sampling intervals do not contract to zero. Moreover, as in the original result, if the CLKF fulfills the small control property then the control is continuous at the origin. With additional assumption, the control can be proved to be smooth everywhere. Some simulation results were provided, they notably highlighted the low frequency of events of the proposal.

Next step is to also consider input delays. Another way of investigation could be to develop event-based strategies for nonlinear systems based on other universal formulas, like the formula of [START_REF] Freeman | Robust Nonlinear Control Design: State-Space and Lyapunov Techniques[END_REF] or the domination redesign formula of [START_REF] Sepulchre | Constructive Nonlinear Control[END_REF], using CLRF and CLKF in the spirit of [START_REF] Jankovic | Extension of control Lyapunov functions to time-delay systems[END_REF] (for the time-triggered case).

  ) with x(0) := x 0 where f and g are smooth functions with f vanishing at the origin. Definition 1.4. (Control Lyapunov function).

  1[ and λ(s) > 0 for s > 0. Therefore, there is no event on the set{x d ∈ X | β d (x d ) = 0} ∪ {0}.We then restrict the study to the setS * d = {x d ∈ X * | β d (x d ) = 0}, where θ and ∆ are strictly positive by assumption. Let us rewrite the time derivative of the CLKF along the trajectories, that is

Fig. 1 .

 1 Fig. 1. Sumulation results of system (26) with CLKF as in (27) and event-based feedback (15)-(16).

ACKNOWLEDGMENT

This work has been partially supported by the LabEx PERSYVAL-Lab (ANR-11-LABX-0025).


whether they are published or not. The documents may come