Paul Rousse
email: rousse@kth.se.

Pierre-Jean Meyer
email: pjmeyer@kth.se.

Dimos V Dimarogonas

Using progress sets on non-deterministic transition systems for multiple UAV motion planning

Keywords: Guidance, navigation and control of vehicles, Multi-vehicle systems, Formal control synthesis, Temporal logic specifications, Non-deterministic transition system

This paper presents a new approach for control synthesis of non-deterministic transition systems under Linear Temporal Logic (LTL) specifications with applications to multiple Unmanned Aerial Vehicles (UAV) motion planning problems. The consideration of such systems is motivated by the non-determinism possibly introduced while abstracting dynamical systems into finite transition systems. More precisely, we consider transition systems enhanced with a progress set describing the fact that the system cannot stay indefinitely in some subset of states. The control synthesis problem is firstly translated into a terminating planning problem. Then, a backward reachability strategy searches for a path from the initial set to the goal set. At each iteration, subsets of states contained in the progress set are added to the path, thus ensuring the reachability to the goal set in finite time. If a solution to the terminating problem is found, the obtained controller is translated back to the initial problem formulation. This approach is validated through an experiment involving two UAVs with a surveillance specification.

INTRODUCTION

Robot motion planning with temporal logic specifications has received a lot of attention in the control community. More recently, the expressiveness of temporal specifications coupled with automated control synthesis methods brought powerful tools. Such tools can be used for provably correct control and planning design of robotic systems under high-level specifications in the form of temporal logic formulas [START_REF] Belta | Symbolic planning and control of robot motion [grand challenges of robotics[END_REF].

The Linear Temporal Logic (LTL) specification language provides an expressive framework where safety, reachability and reactive properties are suitably formulated [START_REF] Baier | Principles of Model Checking[END_REF]. More importantly, they can be translated to finite automata [START_REF] Clarke | Model checking[END_REF][START_REF] Babiak | LTL to büchi automata translation: Fast and more deterministic[END_REF] which makes relevant the use of computer science tools (e.g., graph search and fix point algorithms). In this work, we use LTL formulas that can be expressed as deterministic automata. Even if the expressiveness power is weaker than the whole LTL language, it still encapsulates a wide variety of specifications and is often used in control synthesis [START_REF] Alur | Deterministic generators and games for LTL fragments[END_REF][START_REF] Fainekos | Translating temporal logic to controller specifications[END_REF].

Common approaches for control synthesis under high-level specifications involve the construction of an abstraction of the system. This abstraction is supposed to be used in place of a dynamical system and aims at reducing the overall complexity of the initial synthesis problem. If the system and the abstraction verify some behavioural relationship (see e.g., [START_REF] Tabuada | Verification and control of hybrid systems: a symbolic approach[END_REF], then the controller synthesized on the abstraction under the LTL specification can be refined into a controller such that the original system satisfies the same specification. Although some methods result in deterministic abstractions [START_REF] Kloetzer | A fully automated framework for control of linear systems from temporal logic specifications[END_REF][START_REF] Boskos | Decentralized abstractions for feedback interconnected multi-agent systems[END_REF], other abstraction approaches induce some non-determinism (i.e., a control input can induce several successors from the same initial state, see e.g., [START_REF] Moor | Abstraction based supervisory controller synthesis for high order monotone continuous systems[END_REF][START_REF] Nilsson | Incremental synthesis of switching protocols via abstraction refinement[END_REF]. Non-deterministic transitions in the abstraction can arise due to the state space partitioning or because of initial disturbances of the continuous system. Methods to lower these effects exist, such as partitioning the state space according to the system flow (see e.g., [START_REF] Lafferriere | Ominimal hybrid systems[END_REF][START_REF] Tabuada | Verification and control of hybrid systems: a symbolic approach[END_REF] or designing local controllers that confine disturbances in each cell of the partition (see e.g., [START_REF] Kloetzer | A fully automated framework for control of linear systems from temporal logic specifications[END_REF]. However, none of them can guaranty to get ride of the non-determinism (see e.g., [START_REF] Habets | Reachability and control synthesis for piecewise-affine hybrid systems on simplices[END_REF], and, in such cases, the nondeterministic nature of the system needs to be taken into account.

While control synthesis problems with deterministic models can easily be solved through a reformulation into a model checking problem [START_REF] Clarke | Model checking[END_REF], the same approach cannot be applied with non-deterministic models (Kloetzer and Belta, 2008a). Fixed points methods have been widely used in correct-by-design control synthesis for non-deterministic models (see e.g., [START_REF] Cimatti | Weak, strong, and strong cyclic planning via symbolic model checking[END_REF]Kloetzer and Belta, 2008a). They determine the set of valid controllers by trying to maximize some winning region which corresponds to the subspace of states where there exists a control strategy solving the synthesis problem.

As it has been highlighted in [START_REF] Cimatti | Weak, strong, and strong cyclic planning via symbolic model checking[END_REF], such planner prevents any cycle (path of state-transition that starts and ends at the same state) from being part of a solution as they might keep the state away from the goal set forever. Other approaches use a fairness assumption: for any infinite run, every transition will be taken an infinite number of times [START_REF] Cimatti | Weak, strong, and strong cyclic planning via symbolic model checking[END_REF][START_REF] Fu | Simple and fast strong cyclic planning for fullyobservable nondeterministic planning problems[END_REF]. A direct consequence of this assumption is that every trajectory cannot stay indefinitely in a cyclic path, and thus, these cycles can be part of the solution plan. This fairness assumption is justified in probabilistic models where the probability of any transition is not zero. For this reason, it has been used in action planning where any action can be assigned to a success probability, and an infinite number of attempts will almost surely result in a success. Such probabilistic approaches cannot always hold in the case of control synthesis of a dynamical system: any transition from one state of the abstraction to itself might correspond to an equilibrium point in the original continuous system, and any cycle in the abstraction might correspond to a stable orbit of the system. Therefore the global fairness property is not granted. [START_REF] De Giacomo | Generalized planning with loops under strong fairness constraints[END_REF] where the fairness assumption is modelled as an LTL formula 3ϕ ⇒ 3ψ which stands for: "by trying ϕ infinitely often, ψ will happen infinitely often". This formulation can then be integrated in a general reactivity framework. In this approach, and contrary to fixed point techniques where cycles are all eliminated, or all accepted (when fairness property stands), only nonblocking cycles identified by the model can be part of the solution plan. Other common approaches in control synthesis have been using the quotient transition system in order to deal with cycles in motion planning: this abstraction suppresses any self-transition of the model and only considers a fragment of the LTL formulas [START_REF] Tůmová | A symbolic approach to controlling piecewise affine systems[END_REF][START_REF] Pappas | Bisimilar linear systems[END_REF].

Models with local fairness property have been investigated in De

In this paper we propose a new method for control synthesis of non-deterministic transition systems under LTL specifications. We consider a non-deterministic augmented Finite Transition System (FTS) (firstly introduced for switching systems by [START_REF] Nilsson | Incremental synthesis of switching protocols via abstraction refinement[END_REF]. This model extends the standard FTS structure with the knowledge of a progress set that identifies local control strategies that are terminating (trajectories cannot stay indefinitely in the subset of states using the associated control inputs). We use this model as an abstraction for a dynamical system where the size of the progress set was large, and for this reason, the approach of De [START_REF] De Giacomo | Generalized planning with loops under strong fairness constraints[END_REF], that efficiently deals with small progress sets, was not appropriate. We first introduce the model and the problem to be solved (Section 2). Then the product automaton of the model and the Büchi Automaton is defined and translated to a terminating planning problem (Section 3.1). A backward reachability algorithm is used (Section 3.3) to find a path through a terminating control strategy (Section 3.2) bringing the initial state deterministically in finite time to the goal set. Correctness and termination of the solutions are investigated. This approach is then validated in an experiment (Section 4) involving multiple Unmanned Aerial Vehicles (UAV).

PRELIMINARIES

Definitions

We denote by N the set of natural numbers and by R the set of real numbers. For the sets X, Y , we denote by |X| ∈ N the cardinality of X, 2 X its power set and X ω the set of infinite words with elements chosen in X. For a word w of X ω , Inf (w) ⊆ X denotes the set of elements appearing infinitely often in w. For Z ⊆ X × Y , Z| X ⊆ X denotes the projection of the set Z on the set X. Let X \Y be the set of elements of X not in

Y . If K is R or N, let a, b ∈ K, [a, b] K be the set {x ∈ K | a ≤ x ≤ b} ⊂ K.
In this work, we use a Finite Transition System (FTS) enhanced with a progress set adapted from [START_REF] Nilsson | Incremental synthesis of switching protocols via abstraction refinement[END_REF]: Definition 1. An Augmented Finite Transition System (AFTS) is a tuple defined by T = S, S 0 , U T , δ T , P T where:

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

• U T is the input alphabet; • δ T : S × U T → 2 S is the transition function; • P T ⊆ 2 S×U T is the progress set. An execution of the AFTS T is an infinite sequence r ∈ (S × U T ) ω of state-control input pairs r = {(s k , u k )} k∈N such that: • s 0 ∈ S 0 ; • ∀k ∈ N, s k+1 ∈ δ T (s k , u k ); • ∀m ∈ P T , Inf (r) ⊆ m.
The progress set P T identifies local control strategies that are terminating, i.e., any execution reaching an element m ∈ P T is guaranteed to exit m in finite time. Note that the condition ∀m ∈ P T , Inf (r) ⊆ m does not forbid any execution r to visit infinitely often an element m ∈ P T as long as the execution also leaves m infinitely often (i.e., if

Inf (r) ∩ m = ∅ and Inf (r) \ m = ∅ then Inf (r) ⊆ m).
In the case of switching systems, [START_REF] Nilsson | Incremental synthesis of switching protocols via abstraction refinement[END_REF] introduced the progress set where each element is chosen in 2 S × U T . An element identifies a set of states p g ⊆ S (a progress group) and a control mode u g ∈ U T , and any trajectory starting in the progress group p g using the control mode u g leaves p g in finite time. In this paper, we do not consider control modes that are related to switching systems (control policy valid for a group of states) but a control strategy (state-control action pairs).

We say that ρ ∈ S ω is a run of T if there exists an execution r of T such that ρ = r| S ω . In the present work, we assume that the AFTS T is well-formed meaning that we have: S 0 = ∅; for every reachable state s ∈ S there exists at least one control action leading to another state, i.e., ∃u ∈ U T , |δ T (s, u)| ≥ 1; and all elements of P T have an outgoing transition, i.e., ∀m ∈ P T , ∃(s, u) ∈ m, δ T (s, u) ⊆ m| S .

The reader is referred to the dedicated literature about formal methods (such as [START_REF] Baier | Principles of Model Checking[END_REF] for a formal definition of the LTL language. In summary, an LTL formula over a set S is defined inductively by: ϕ

::= | a | ¬ϕ | ϕ 1 ∧ ϕ 2 | ϕ | ϕ 1
Uϕ 2 where the logical operators (true), ¬ (negation), ∧ (conjunction), the temporal operators (next) and U (until) are combined with elements a ∈ S and LTL formulas ϕ 1 and ϕ 2 . The useful operators ∨ (disjunction), ⇒ (implication), (always) and 3 (eventually) can be derived from the previous ones. These LTL formulas provide a userfriendly language to express specifications, for example "avoid area d, visit area c, and avoid area a until you reach area b" can be expressed by the following formula: ϕ = ( ¬d) ∧ (3c) ∧ ((¬a)Ub). Every LTL formula over an input alphabet S can be translated into a Büchi Automaton (BA) [START_REF] Clarke | Model checking[END_REF]:

Definition 2. A Büchi Automaton is a tuple A ϕ = Q ϕ , Q ϕ 0 , S, δ ϕ , F ϕ where: • Q ϕ is the finite set of states; • Q ϕ 0 ⊆ Q ϕ is the set of initial states; • S is the input alphabet; • δ ϕ : Q ϕ × S → 2 Qϕ is the transition function; • F ϕ is the set of accepting states. If Q ϕ 0 is a singleton and |δ ϕ (q, a)| ∈ {0, 1} for all a ∈ S and all q ∈ Q ϕ , then A ϕ is called Deterministic Büchi Automaton (DBA). It is called a Non-deterministic Büchi Automaton (NBA) otherwise.
In this paper, we use LTL specifications that can be represented with DBA. Such DBA can be generated using a NBA of a given LTL formula and applying determinization processes [START_REF] Alur | Deterministic generators and games for LTL fragments[END_REF][START_REF] Babiak | LTL to büchi automata translation: Fast and more deterministic[END_REF]. However, this is not always achievable, and only a fragment of LTL formulas are translatable into DBA (see Theorem 4.50 in Baier and Katoen, 2008, pp. 190). Nonetheless, this fragment allows to express a wide range of specifications [START_REF] Fainekos | Translating temporal logic to controller specifications[END_REF]. For an infinite input word w = w 1 w 2 w 3 ... ∈ S ω , there exists a set of infinite state trajectories in A ϕ produced by w that we denote as R ϕ (w) ⊆ Q ϕ ω .

Definition 3. The input word w ∈ S ω is said to be accepted by A ϕ if there exists r ∈ R ϕ (w) such that Inf (r)∩F ϕ = ∅.

Note that the input alphabet S of A ϕ is chosen as the set of states of T so that a run of T produces an input word for the BA A ϕ . A run r of T can then be accepted or not by A ϕ .

Problem statement

The problem considered in this paper is formulated as follows:

Problem 4. Given a non-deterministic and well-formed AFTS T = S, S 0 , U T , δ T , P T and a DBA A ϕ = Q ϕ , Q ϕ 0 , S, δ ϕ , F ϕ , find a control strategy such that all runs of the controlled system are accepted by A ϕ .

To satisfy the acceptance condition of A ϕ (see Definition 3), the control strategy of the system T should produce trajectories in A ϕ that reach the acceptance set F ϕ in finite time. Therefore, in the case of an FTS (AFTS with no progress set, i.e., P T = ∅), every control strategy creating cyclic trajectories in A ϕ outside of the acceptance set F ϕ cannot be a solution of the problem. For the AFTS T , if these corresponding cyclic executions are in one element of the progress set P T , then these cycles are escaped in finite time, and the controller might be a solution of Problem 4.

SOLUTION

Problem 4 is solved in several steps. First, we create the product automaton of T and A ϕ , and translate it into an equivalent formulation as a terminating planning problem (Section 3.1). Then, we identify control strategies on subsets of the state space which can reach, deterministically and in finite time, given sets of states (Section 3.2). Finally, we use these local terminating controllers to find a nonblocking control strategy starting the search from the goal set until the initial set is found (Section 3.3).

Terminating formulation

We first define the product automaton of a DBA and an AFTS: Definition 5. The product automaton A p of the DBA A ϕ and of the AFTS T is defined by

A p = T ⊗ A ϕ = Q p , Q p 0 , U p , δ p , F p , P p where: • Q p = S × Q ϕ is the set of states; • Q p 0 = S 0 × Q ϕ 0 is the set of initial states; • U p = U T is the input set; • δ p : Q p × U p → 2 Qp is the transition function defined by (s , q ) ∈ δ p ((s, q), u) iff s ∈ δ T (s, u), q ∈ δ ϕ (q, s); • F p = S × F ϕ is the acceptance set; • P p ⊆ 2 Qp×Up is the progress set defined for m ∈ 2 Qp×Up by m ∈ P p ⇔ m| S×U T ∈ P T .
Note that the product automaton A p is a Büchi Automaton augmented with the progress set of the AFTS T . We say that an execution r ∈ (Q p × U p ) ω of the product automaton is valid if ∀m ∈ P p , Inf (r) ⊆ m (this condition is inherited from Definition 1 of the AFTS). A valid execution r of the product automaton is said to be accepted if the corresponding state trajectory ρ = r| Qp ω satisfies Inf (ρ) ∩ F p = ∅. An accepted execution of A p thus corresponds to a valid execution of T that is accepted by

A ϕ . A controller of A p is a map π : Q p → U p that associates to each state p ∈ Q p an available control action u ∈ U p (p) where U p (p) = {u ∈ U p | |δ p (p, u)| ≥ 1}.
• Q t = Q p ∪ G 0 t is the set of states; • Q t0 = Q p 0 ∪ G 0 t is the set of initial states; • U t = U p is an input alphabet; • δ t : Q t × U t → 2 Qt is the transition function defined by p ∈ δ p (p, u) ⇔ p ∈ δ t (σ(p), u); • G t = F p is the goal set; • P t = P p is the progress set. where σ : Q p → Q t is a function mapping Q p \ F p to Q t \ (G t ∪ G 0 t ) and F p to G 0 t , namely: σ(p) = p if p ∈ Q p \ F p σ(g j ) = g 0 j for j ∈ [1, n] N A t is said to be well-formed if A p is well-formed. A controller π t : Q t → U t of A t is said to be closed (resp. terminating) if the associated controller π p = π t • σ of A p is closed (resp. terminating).
The terminating formulation A t of A p is built by mapping all transitions from F p to transitions from a duplicate set G 0 t of F p and by adding G 0 t to the initial set Q t0 . Figure 1 illustrates the construction of the transition function δ t and of the set of states Q t of A t . A p is supposed to be well-formed (see Problem 4), thus A t is also wellformed which means that for every state q ∈ Q t \ G t there exists an available control action u ∈ U t (q) where U t (q) = {u ∈ U t | |δ t (q, u)| ≥ 1}. Let an execution of A t be a finite or infinite sequence r = {(q k , u k )} k<I of length I ∈ N ∪ {∞} with elements chosen in Q t × U t such that:

• q 0 ∈ Q t0 ; • ∀k < I, q k+1 ∈ δ t (q k , u k ); • ∀m ∈ P t , Inf (r) ⊆ m.
For a closed controller π t , a π t -execution corresponds to a sequence of A t such that r = {(q k , π t (q k ))} k≤I with I ∈ N∪{∞}. From Proposition 6, we can now equivalently solve Problem 4 by trying to find a closed and terminating controller π t for the system A t such that all the π texecutions of A t reach the goal set G t in finite time.

Terminating modules search

Any control strategy in A t creating cyclic execution might produce runs that loop ad infinitum, hence keeping the state away from G t forever. If, however, each of these potential cycles is included into elements of the progress set P t , then none of them can block the system indefinitely. Thus, a control strategy π t in A t can ensure the termination property if the following statement is true: π t bring the state from terminating modules (defined in the sequel) to other terminating modules strictly closer to the goal set G t . This section details the search of a terminating module that reaches, deterministically and in finite time, a given set of states. We first introduce some definitions. Let a module m ⊆ Q t × U t of A t be a set of state-control input pairs such that ∀(q, u) ∈ m, u ∈ U t (q) and every state is associated to a unique control action (∀q ∈ m| Qt , |m ∩ ({q} × U t )| = 1). We call M the set of modules of A t . Then, let P ost : M → 2 Qt be the function that associates to a module its successor states, i.e., for m ∈ M , P ost(m) = (q,u)∈m δ t (q, u), let P ost : M → 2 Qt be defined as the set of the outgoing successor states of a given module, i.e., for m ∈ M , P ost(m) = P ost(m) \ m| Qt . Definition 7. m ∈ M is a terminating module of A t if all executions of A t = Q t , m| Qt , U t , δ t , G t , P t exit m in finite time, i.e., for every execution r = {(q k , u k )} k<I , I ∈ N ∪ {∞} of A t , there exists i < I such that q i / ∈ m| Qt , and ∀k < i, (q k , u k ) ∈ m.

Note that each module m ∈ M in the progress set P t or such that P ost(m) ∩ m| Qt = ∅ (i.e., without selftransitions) is terminating.

For a goal set g ⊆ Q t , let PrecedingSingletonModules(g) ⊆ M be defined as the set of singleton modules with states chosen in Q t \ g that have one or more successors in g, namely:

{(q, u)} ∈PrecedingSingletonModules(g)

⇔ q ∈ Q t \ g δ t (q, u) ∩ g = ∅
and, for a module m ∈ M , let ExpandModule(g, m) ⊆ M be defined by:

m ∈ExpandModule(g, m) ⇔ m | Qt = m| Qt ∪ (P ost(m) \ g) m ⊂ m ExpandModule(g, m)
is the set of possible expansions of m with states chosen in Q t \ g. Algorithm 1 details the search of terminating modules that go, deterministically and in finite time, to a given subset g of Q t . The search is implemented as a Breadth-First Search (BFS) over the set of possible terminating modules. For a set of winning regions W ⊆ 2 Qt , w ∈ W corresponds to a set of states where a winning control strategy (i.e., terminating and reaching the goal set G t ) has already been found (the next section will more specifically state the definition of W ). The set M of modules to visit is initialized (line 1) with the preceding singleton modules of g (PrecedingSingletonModules(g)). At each iteration, one of the smallest modules m of M (smallest in terms of cardinality; lines 4, 5 and 6) is removed from M and added to the set of visited modules M v . All possible successor modules of m are obtained with ExpandModule(g, m), and those that have not been visited added to the set M of modules to visit (line 10). Finally, the module m is returned if it verifies the following properties (line 7):

L v ← L v ∪ {K} ; // Add K to L v 21 W ← { l| Qt | l ∈ L ∪ L v } ; // set
• P ost(m) ⊆ g: all the successor states of m are either going to the set of states m| Qt or to the set g, • m ∈ P t or P ost(m) ⊆ g: m is a terminating module,

• g ∪ m| Q /
∈ W : no control strategy has been found yet.

The first property ensures that any trajectory beginning from module m either stays in m or reaches g in finite time.

The second one ensures that the trajectory actually leaves m| Qt . The first two properties combined together show that modules returned by Algorithm 1 deterministically reach the set of states g and are terminating. The last property ensures that the new set of reachable states has not been considered yet. If there is no module found, ∅ is returned (line 13).

Backward Reachability Algorithm

We are now able to find terminating modules that bring any execution of A t deterministically and in finite time to a given set of states through Algorithm 1. The same algorithm can then be used to iteratively expand a winning region where a terminating and closed control strategy exists. Algorithm 2 implements this as a Depth-First Search (DFS) using a backward reachability strategy: preceding terminating modules are searched and added to a terminating controller starting from the goal set G t until all initial states in Q t0 are found.

Let a plan K ⊆ M ∪{m 0 } be a set of terminating modules of A t (see Definition 7) and of:

m 0 = {(g, ∅) | g ∈ G t }
(1) a fake module comprised of each goal state associated to none of the control actions. Let K = k∈K k be the corresponding set of state-control action pairs. L corresponds to the set of plans to visit and is initialized (line 14) with K G = {m 0 }. At each step, the highest cardinality plan K is selected from L (line 17). If the initial set belongs to K| Qt (the set of states of plan K), then plan K is returned (line 19). Otherwise, a terminating module m preceding K| Qt (line 22) is returned by Algorithm 1, and the new plan K ∪ {m} is added to the list L of plans to visit (line 24). Note that the module m is chosen to produce a plan with a set of reachable states that have not been created yet (m| Qt ∪ K| Qt / ∈ W ; line 7 of Algorithm 1). If there is no valid module found (lines 22 and 23), then plan K is removed from L (line 26). When the set L of plans to visit is empty (line 28), that means that among all the possible configurations of reachable states comprised of terminating modules, none of them could find a solution and a F ail flag is returned (line 29). Theorem 8. Let K be a valid plan returned by Algorithm 2 (K = F ail) and π K be the controller associated with K defined by π K (q) = u for all (q, u) ∈ K = k∈K k. The controller π K is closed and terminating.

Proof. Let K be a plan found from Algorithm 2, let m 0 , m 1 , ... be the modules that compose the plan K indexed from the first one added (m 0 , defined in (1)) to the last one (m |K|-1 ), K = {m 0 , m 1 , ...} with m 0 | Qt = G t . By construction of K (see Algorithm 1 line 7, and Algorithm 2 lines 21 and 22), for all i ∈ [1, |K| -1] N :

P ost(m i ) ∈ 0≤j<i m j | Qt (2) m i | Qt ∩ 0≤j<i m j | Qt = ∅ (3) Using (3) recursively, for all i, i ∈ [0, |K| -1] N s.t. i = i , we have: m i | Qt ∩ m i | Qt = ∅. (4) As each module m i ∈ M , for i ∈ [1, |K| -1] N ,
associates to each state of m i | Qt a unique control action (see the definition of M in Section 3.2), and thanks to (4), every state in ( K \ m 0 )| Qt is associated to one and only one control input. Thus, the controller π K is correctly defined in Theorem 8.

As for all (q, u) ∈ K \ m 0 , δ t (q, u) ⊆ K| Qt from (2) and as Q t0 ⊆ K| Qt (Algorithm 2, line 18), the controller π K is closed. As π K is closed, there exists a π K -execution r = {(q k , u k )} k<I with I ∈ N ∪ {∞} such that (q i , u i ) ∈ K for every i < I. From (4), for every q ∈ K| Qt there exists a unique

j ∈ [0, |K| -1] N such that q ∈ m j | Qt . We define the b 0 b 1 G ¬G G Fig. 2. Deterministic Büchi Automaton that represents the formula ϕ = (¬G)U( G). The acceptance set is F ϕ = {b 1 } and the initial set is Q ϕ 0 = {b 0 }.
unique sequence of indexes J = j 0 j 1 ... such that q i ∈ m ji for every i < I. As A t is well-formed (Problem 4 and Property 6), there is always an available transition as long as m 0 is not reached. Therefore, we choose r to be infinite (I = ∞) iff m 0 is not reached. By definition of r and as (q 0 , u 0 ) ∈ m j0 , we have q 1 ∈ δ t (q 0 , u 0 ) ⊆ P ost(m j0 ).

Then from (2), all the successors of m j0 are in the modules of smaller indexes, consequently j 1 ≤ j 0 . This argument can be used for all i < I, meaning that J is a decreasing sequence. Moreover J is lower bounded by 0, therefore it is converging to a value j * such that 0 ≤ j * < |K|.

Assuming j * > 0 implies that Inf (r) ⊆ m j * . However, this invalidates the fact that m j * is a terminating module (line 7 of Algorithm 1). The only solution is j * = 0 and m j * | Qt = m 0 | Qt = G t , which means that there exists i ∈ N such that q i ∈ G t , i.e., the goal set is reached in finite time, and therefore, the controller π K is terminating. 2

As the controller π K is closed and terminating, the controller (after mapping with σ -previously defined by ∀p ∈ Q p \ F p , σ(q) = q and ∀j ∈ [1, n] N , σ(g j ) = g 0 j ) is a valid solution of Problem 4. Corollary 9. Let K be a valid plan returned by Algorithm 2 (i.e., K = F ail) and π K be the controller associated to K defined by π K (q) = u for all (q, u) ∈ K. The controller π p = π K • σ is a solution of Problem 4. Remark 10. The termination of Algorithm 1 and 2 is ensured by two facts: the browsed state space is finite and the use of a visited set (M v and L v in Algorithm 1 and 2) avoids any element to be visited twice.

Illustration

Figure 3 illustrates how Algorithm 2 finds a solution plan. An agent starting in Q 0 needs to verify ϕ = (¬G)U( G), namely "reach and stay in G", using four given control actions ( , , and ). Note that ϕ can be represented by a DBA (e.g., see ltl3ba, Babiak et al., 2012, Figure 2 shows a DBA representing ϕ). The progress set P T is partially described by {a, b, c, d} ⊂ P T . The transition system T is not explicitly defined and the reader is instead referred to Figure 3.

Due to the special form of the LTL formula ϕ, the terminating formulation A t can be defined equivalently Four control actions are available ( , , and ) and each of them points in the direction of the 3 successors of the considered state (square cell). Each red box corresponds to a terminating module and the green box corresponds to the goal set G t of A t .

than in Section 3.1 by: the goal set G t = G, the set G 0 t = {g 0 1 , ..., g 0 4 } duplicate of G = {g 1 , ..., g 4 }, the set of states Q t = S ∪ G 0 t , the initial set Q t0 = Q 0 ∪ G 0 t , the progress set P t = P T , and the transition function defined by: s ∈ δ T (s, u) ⇔ s ∈ δ t (σ(s), u) (where σ : S → Q t is the mapping function similarly defined as in Proposition 6, i.e., σ(s) = s iff s ∈ S \ G t and σ(g i ) = g 0 i for i ∈ [1, 4] N ). Note that in Figure 3, G t and G 0 t are superimposed however, we remind that G t ∩ G 0 t = ∅. Algorithm 2 is initialized with a plan K 0 = {m 0 } where m 0 is the fake goal module introduced in Section 3.3 (i.e, m 0 | Qt = G t , green box in Figure 3). At the first iteration, the plan K 0 is selected from the set L = {K 0 } of plans to visit. Algorithm 1 searches for a terminating module preceding the set of states G t = K0 | Qt : e.g., m 1 = g 0 1 = {(g 0 1 , )} is returned as all successors P ost(m 1 ) of m 1 are in K0 | Qt . The new plan K 1 = K 0 ∪{m 1 } is added to L. At the next iteration of Algorithm 2 (and at each iteration in this example), the highest cardinality plan of L is the last one added to L. For the same reasons than for module m 1 with plan K 0 , modules m 2 = g 0 2 , m 3 = g 0 3 and m 4 = g 0 4 are successively added to plans K 2 = K 1 ∪ {m 2 }, K 3 = K 2 ∪{m 3 } and K 4 = K 3 ∪{m 4 }. At the 5 th iteration of Algorithm 2, K 4 is the biggest plan of L = {K 0 , ..., K 4 } and Algorithm 1 searches for a terminating module going to K4 | Qt = G t ∪ G 0 t deterministically and in finite time; there is no singleton terminating module, the smallest valid ones are composed of at least 2 elements, e.g., a is returned as it belongs to P t and goes to G t ⊂ K4 | Qt . m 5 = a is added to K 5 = K 4 ∪ {m 5 }.

In the next iteration, the terminating module b is returned as it goes to a| Qt ⊂ K6 | Qt and as b ∈ P t , then m 6 = b is added to the plan K 6 = K 5 ∪ {m 6 }. m 7 = c is added to K 7 = K 6 ∪{m 7 } as it goes deterministically to a| Qt ∪b| Qt ⊂ K6 | Qt and as c ∈ P T . Note that the transition between the modules is not deterministic (P ost(c) ⊆ (a| Qt ∪ b| Qt )). Finally, m 8 = d is added to K 8 = K 7 ∪ {m 8 }, and as d| Qt ∪ c| Qt = Q t0 ⊂ K8 | Qt , K 8 is a plan that brings all the trajectories starting in Q t0 to the goal set in finite time. Algorithm 2 returns the solution plan K = K 8 . Every trajectory of the system T controlled by π p = π K • σ (Theorem 8 and Corollary 9) verifies the specification ϕ.

EXPERIMENT

The experiment detailed below shows that the approach presented in this paper is appropriate for UAV motion planning scenarios. Multiple quadricopters (Iris Plus, 3DRobotics) are tracked with a motion capture system (Qualisys) and controlled from an offboard computer (using the Robot Operating System -ROS-framework). Algorithms are implemented in python, and the LTL translation to DBA is done using ltl3ba [START_REF] Babiak | LTL to büchi automata translation: Fast and more deterministic[END_REF].

Each quadricopter is modelled as a 2D first integrator system with additive disturbances. The multi-agent model is built as the concatenation of each single agent linear model, namely S is defined by: ẋ = u + w where x ∈ R 2n , n ∈ N is the number of agents (n = 2 in our case), u ∈ U is the control input with U = {-0.2, 0.2} 2n , and w ∈ W is a disturbance with W = [-0.1, 0.1] 2n R . Such a system verifies a monotonicity property [START_REF] Angeli | Monotone control systems[END_REF] which can be described in the following way: let φ(t, x, u, w) the state reached at time t from x under input u and disturbance w, if x ≤ x , u(t) ≤ u (t) and w(t) ≤ w (t) for all t ≥ 0, then φ(t, x, u, w) ≤ φ (t, x , u , w ) where ≤ is the component-wise inequality. For x, y ∈ R 2n , we define the closed interval

[x, y] = {z ∈ R 2n | x ≤ z ∧ z ≤ y} ⊂ R 2n .
Let the following intervals of R 2n be defined by:

X=[    -1 -1 -1 -1   ,    1 1 1 1   ], X a =[    -1 -1 0.2 0.2   ,    -0.2 -0.2 1 1   ], X b =[    0.2 0.2 -1 -1   ,    1 1 -0.2 -0.2   ].
A discrete time system S d is obtained by sampling the continuous system S at a sampling time ∆ T = 1.0s. In order to build the FTS structure of T , the state space of S d is partitioned, let Ξ : X → S be the partitioning function which associates to each continuous state of S d a symbol of T . The set X is uniformly partitioned (with a step x d = 0.4 for every dimension of R 4 ) and R 4 \ X is mapped to a single symbol. As in [START_REF] Meyer | Invariance and symbolic control of cooperative systems for temperature regulation in intelligent buildings[END_REF], a nondeterministic abstraction is created after the computation of reachable set over-approximations of S d (using the monotonicity property). The set P T is defined by: m ∈ P T ⇔ X m is bounded and min dx∈Cm dx > 0 where C m is the convex hull of the set m| U T + W (with + the Minkowski sum) and X m ⊆ X is the set of continuous states covering the symbols of m| Qt (i.e., X m = {x ∈ X | Ξ(x) ∈ m| S }). For m ∈ P T , as X m is bounded and as the time average of the state displacement has a strictly positive norm, every trajectory of S d starting in X m will escape the set X m in finite time (details are omitted due to space limitation). This guaranties the existence of some behavioural relationship (see [START_REF] Nilsson | Incremental synthesis of switching protocols via abstraction refinement[END_REF] between the abstraction and the system S d . Hence, the control synthesis for the abstraction will be valid as well for the original continuous system.

For x = [x 1 , x 2 , x 3 , x 4 ] the continuous state of the system, where [x 1 , x 2 ] is the position of agent 1, and [x 3 , x 4 ] the position of agent 2, we define the following atomic propositions: out ⇔ x / ∈ X, a ⇔ x ∈ X a , b ⇔ x ∈ X b , collide ⇔ max i∈{1,2} |x i -x i+2 | < 0.4. In other words, the label a (resp. b) corresponds to agent 1 in region blue (resp. in region red) and agent 2 in region red (resp. in region blue; see Figure 4), collide corresponds to a situation where the quadricopters are too close and can collide, and the label out corresponds to one or more agents leaving the environment X| R 2 .

The system must verify the following specification: ϕ = ( ¬out) ∧ ( ¬collide) ∧ ( 3a) ∧ ( 3b).

Note that there exists a DBA translation of ϕ (e.g., see ltl3ba in [START_REF] Babiak | LTL to büchi automata translation: Fast and more deterministic[END_REF]. The specification ϕ can be expressed in plain words as: "always stay inside the environment, always avoid collision, infinitely often go to a, infinitely often go to b".

We ran the experiment with real quadricopters using the controller π p solution of Problem 4 found with Algorithm 2 and Corrolary 9. Figure 4 shows a few steps of the experiment and a video is available at 1 . All states of T have non-deterministic transitions with 16 possible successors (for each control input). Modules of the solution plan K, obtained with Algorithm 2, have a cardinality of 4 when the module must be terminating for both agents and of 8 when the module is terminating for only one of the agents (e.g., if one of the agents has already reached its region and must wait for the other one to reach its own region). Agent 1 and agent 2 start in b. The discrete state of the system p ∈ A p is initialized with the measurement of the continuous state x 0 : p = (Ξ(x 0 ), p 0 ) ∈ Q p 0 . At each step, the continuous state x of the system is measured and mapped to a symbol s = Ξ(x) of S, then the current discrete state p ∈ Q p of A p is updated with the new state p = (t, b), unique element of δ p (p, π p (p)) such that t = s.

Steps at T = 13, 14 and 15 highlight the cyclic transitions of the AFTS in one of the terminating module of the plan K.

Step T = 40 shows the end of the experiment where the agents reached a.

CONCLUSION

We proposed a solution to the control synthesis problem of a non-deterministic transition system under Linear Temporal Logic specifications that can be represented by Deterministic Büchi Automata. The considered system is modelled as a finite transition system enhanced with a progress set. Elements of the progress set identify local control strategies that are terminating (the state will escape a given set of states in finite time). Experiments with multiple UAVs show that this approach is relevant for world applications where the non-determinism of the system cannot be narrowed after the abstraction of it.

Only a fragment of LTL formulas are translatable into DBA, and if there is no deterministic translation possible, then the product automaton of the FTS and the NBA representing the formula is not fully observable (2 successors of the same state and input control might produce the same observation), and our approach is not valid anymore. How to handle such situations will be the topic of future works.

Fig. 3 .

 3 Fig. 3. Illustration of Algorithm 1 and 2. The agent goes from set Q 0 (in red) to reach and stay in set G (in blue) following the control actions (black arrows).Four control actions are available ( , , and ) and each of them points in the direction of the 3 successors of the considered state (square cell). Each red box corresponds to a terminating module and the green box corresponds to the goal set G t of A t .

Fig. 4 .

 4 Fig. 4. Agent 1 (in blue) and agent 2 (in red) need to exchange position infinitely often. At timestep T, the current state of the agents (cell in plain color) is associated to a control input (thick blue arrows) and have multiple successors (thin black arrows and cells in light color).

  The controller is said to be closed if every state reachable from the initial set Q p 0 using the controller π is associated with a control action, and it is terminating if all the reachable states can reach the acceptance set F p in finite time. Construction of A t from A p . Similar node shape represents equivalent state sets. Similar line style represents equivalent transition function between sets. formulation of A p is denoted as A t = Q t , Q t0 , U t , δ t , G t , P t such that:

	Qp \ Fp	Fp	≡	G 0 t	Qt \ (G 0 t ∪ Gt)	Gt
	Fig. 1.
						Finding
						a controller for Problem 4 consists in finding a closed
						and terminating controller over A p . In what follows, this
						control problem is translated into a terminating formula-
						tion.

Proposition 6. (Theorem 4 in

[START_REF] Patrizi | Fair LTL synthesis for non-deterministic systems using strong cyclic planners[END_REF]

. Let a non-deterministic product automaton

A p = Q p , Q p 0 , U p , δ p , F p , P p , where F p = {g 1 , ..., g n }, |F p | = n, and Q p = {p 1 , ..., p m , g 1 , ..., g n }, |Q p | = n + m. Let G 0 t = {g 0 1 , .

., g 0 n } be a duplicate definition of F p (with different names for the corresponding states so that G 0 t ∩F p = ∅). The terminating

  Function PrecedingModuleBFS(A t , g, W ) Data:A t : the terminating problem formulation, g ⊆ Q t : a set of states to be reached, W ⊆ 2 Qt : a set of already visited sets of states. Result: m if a valid module is found, ∅ otherwise

	1 M ← {PrecedingSingletonModules(g)} ;	// modules
		to visit
	2 M v ← ∅ ;	// visited modules
	3 repeat
	4	m ← arg min x∈M (|x|) ;		// smallest
		cardinality module
	5	M ← M \ {m} ;	// Remove m from M
	6	M v ← M v ∪ {m} ;	// mark m as visited
	7	if P ost(m) ⊆ g and (m ∈ P t or P ost(m) ⊆ g) and
		g ∪ m| Q / ∈ W then
	8	return m ; // terminating module found
	9	else
	10	M ← M ∪ (ExpandModule(g, m) \ M v ) ;	// Add
		the new modules to the set of modules
		to visit
	11	end
	12 until |M| = 0;
	13 return ∅ ;	// no module found

Algorithm 1. Breadth-First Search (BFS) of the terminating modules

This work was supported by the H2020 ERC Starting Grant BUCOPHSYS, the EU H2020 AEROWORKS project, the EU H2020 Co4Robots project, the Swedish Foundation for Strategic Research, the Swedish Research Council and the KAW Foundation.


Ingrid Falk

Fabienne Martin

Towards a lexicon of event-selecting predicates for a French FactBank

.

Introduction

Texts not only describe events, but also encode information conveying whether the events described correspond to real situations in the world, or to uncertain, (im)probable or (im)possible situations. This level of information concerns event factuality. This study reports ongoing work on the annotation of French TimeBank events with event factuality information, whose main goal is the elaboration of a French FactBank. We plan to achieve this as follows. [START_REF] Saurí | Are you sure that this happened? assessing the factuality degree of events in text[END_REF] developed an elaborate model of event factuality that allows for its automatic detection. We aim to capitalise on this work by applying [START_REF] Saurí | Are you sure that this happened? assessing the factuality degree of events in text[END_REF]'s algorithm to the events in the French TimeBank (FTiB henceforth) and assign to these a factuality profile. Given that the FTiB has only about 1/4 of the size of the English Time-Bank, we will manually review the automatically obtained factuality profiles in a second step. [START_REF] Saurí | Are you sure that this happened? assessing the factuality degree of events in text[END_REF]'s algorithm relies on two crucial prerequisites. The first is the identification of the sources at play, i.e. the cognitive agents endorsing a specific epistemic stance on the events described. The text author is the default source, but some linguistic constructions -and a subclass of verbs in particular, see e.g. affirm -present one or more sources that are also committed to the factuality of the reported event. Secondly, the algorithm makes use of three languagespecific and manually developed lexical resources, capturing the way polarity particles, particles of epistemic modality and so-called event-selecting predicates (e.g. manage to, suspect that) influence event factuality. In this study, we show how existing lexical semantic resources can be used and modified in order to build the French-specific lexical resources needed to apply Saurí and Pustejosvki's algorithm to the French TimeBank.

The English FactBank

As described in [START_REF] Saurí | FactBank: a corpus annotated with event factuality[END_REF], FactBank is an English corpus annotated with information concerning the factuality of events. It is built on top of the English TimeBank by adding a level of semantic information. TimeBank is a corpus annotated with TimeML [START_REF] Pustejovsky | Temporal and event information in natural language text[END_REF], a specification language representing temporal and event information in discourse. The factuality information encoded in TimeBank and relevant for our work are the event-selecting predicates (cf. Section 3) which project a factual value to the embedded event by means of subordination links (or SLINKs).

In TimeBank, a total of 9 488 events across 208 newspaper texts have been manually identified and annotated. FactBank assigns additional factuality information to these events. More specifically, it is annotated for each event (i) whether its factuality is assessed by a source different from the text author and (ii) the degree of factuality the new source and the text author attribute to the event (for in-stance, Peter affirmed P presents P as certain for Peter, but does not commit the text author to P in a specific way). Saurí and Pustejovsky (2009) distinguish six 'committed' factuality values (i.e. values to which a source is committed) and one 'uncommitted' value, which are shown in Table 1. [START_REF] Saurí | Are you sure that this happened? assessing the factuality degree of events in text[END_REF] present an algorithm which assigns to each TimeBank event a factuality profile consisting of (i) its factuality value, (ii) the source(s) assigning the factuality value to that event and (iii) the time at which the factuality value assignment takes place. The algorithm assumes that events and relevant sources are already identified and computes the factuality profile of events by modelling the effect of factuality relations across levels of syntactic embedding. It crucially relies on three lexical resources which the authors developed manually for English. Since to apply this algorithm to the French data we need to create similar resources for French, we describe them in more detail in the following section.

Lexical Resources for the Automatic Detection of Factuality Profiles

The first lexical resource is a list of 11 negation particles (adverbs, determiners and pronouns) which determine the polarity of the context, together with a language independent table showing how these polarity markers influence the polarity of the event. The corresponding list of negation particles needed for French can be set up easily.

The second resource aims to capture the influence of epistemic modality on the event. It gives a list of 31 adjectives, adverbs and verbs of epistemic modality together with the factuality value they express. Most of their French counterparts influence the context the same way as in English, except for modal verbs, that are well-known to give rise to an 'actuality entailment' under their root/non-epistemic readings (i.e. to present the embedded event as a fact in the real world) when combined with a perfective tense, see [START_REF] Hacquard | On the Interaction of Aspect and Modal Auxiliaries[END_REF], an issue briefly addressed in Section 4.

The third resource is the most complex one and accounts for the influence on the event factuality value in cases where the event is embedded by so-called event-selecting predicates (ESPs), of which suspect that/manage to are examples. ESPs are predicates with an event-denoting argument, which lexically specify the factuality of the event. Saurí and Pustejovsky distinguish two kinds of ESPs: Source Introducing Predicates (SIPs) introduce a new source in discourse (e.g. suspect/believe); Non Source Introducing Predicates (NSIPs) do not (e.g. manage/fail). As part of their lexical semantics, SIPs determine (i) the factuality value the new source (the 'cogniser') assigns to the event described by the complement, and (ii) the factuality value assigned by the text author (i.e. the 'anchor') to the same event. NSIPs, on the other hand, determine event factuality wrt. a unique source, the anchor. In addition, the assessment of event factuality wrt. the relevant source(s) varies with the polarity and modality present in the context of the ESP. Table 1 illustrates the lexicon layout through sample entries for the NSIPs manage and fail. 1 The ESP lexicon built by [START_REF] Saurí | Are you sure that this happened? assessing the factuality degree of events in text[END_REF] consists of 646 entries in total (393 verbs, 165 nouns and 88 adjectives). In order to apply [START_REF] Saurí | Are you sure that this happened? assessing the factuality degree of events in text[END_REF]'s algorithm to the French TimeBank, we need to build a similar ESP lexicon for French. To speed up this process, we plan to use a large body of research about English predicates with sentential complements (Karttunen, 1971b;Karttunen, 1971a;[START_REF] Nairn | Computing relative polarity for textual inference[END_REF][START_REF] Karttunen | Simple and phrasal implicatives[END_REF] 2 , which we briefly introduce in the following.

Factive and implicative verbs. [START_REF] Nairn | Computing relative polarity for textual inference[END_REF] develop a semantic classification of complement-taking verbs according to their effect on the polarity of their complement clauses. This classification is shown in Table 2. We illustrate how the table works in the following examples. In example (1), the ESP fail to has positive polarity. We obtain the factuality of the embedded event (reschedule) by retrieving from the polarity + column in Table 2 the polarity value in the fail to row, which is '-', i.e. the meeting is not rescheduled (has factuality CT-). For (2), the factuality must be retrieved from the polaritycolumn resulting in '+', i.e. a factuality of CT+ (the meeting is rescheduled).

(1) Kim failed to reschedule the meeting.

(2) Kim did not fail to reschedule the meeting.

The effect of a predicate on the polarity of its embedded complement is represented more concisely through a "signature". For instance, the signature of factive verbs as forget that is '+ + | -+' (Read: 'if positive polarity, event happens; if negative polarity, event happens'). Thus, based on the signature of a predicate and its polarity in a given sentence, we can determine the factuality of the embedded event in that sentence. It should now be obvious how the classification in Table 2 can be "plugged" into the ESP lexical resources illustrated in Table 1:3 For a given ESP for which a lexical entry has to be set up (eg. fail), the factuality value conveyed on the embedded event can be retrieved from Table 2 whenever the corresponding table entry is not n. In case it is, the polarity value must be set to u (unspecified). [START_REF] Nairn | Computing relative polarity for textual inference[END_REF] compiled a list of roughly 250 English verbs found to carry some kind of implication: a positive or negative entailment, a factive or a counterfactive presupposition4 . To test how this approach can help us build the French ESP lexical resource required for a French factuality profiler, we translated these English verbs into their French counterparts, and looked at the sentences in the French TimeBank using these French counterparts as ESPs. We first briefly introduce the French TimeBank before describing our data, experiments and findings.

Experiments on the French TimeBank

The French TimeBank [START_REF] Bittar | Building a TimeBank for French: a reference corpus annotated according to the ISO-TimeML standard[END_REF][START_REF] Bittar | French TimeBank: an ISO-TimeML annotated reference corpus[END_REF] is built on the same principles as the English TimeBank, but introduces additional markup language to deal with linguistic phenomena not yet covered and specific to French. Most relevant to this study are the following. FTiB uses ALINK elements to encode aspectual subordination relations, holding between events realised by an aspectual verb (e.g. commencer 'begin') and a subordinated event complement. The subordinating events in ALINKs, as those in SLINKS, are ESPs and are therefore also relevant for this study. Also, since French modal auxiliaries can be fully inflected and fall within the scope of aspectual operators, they are also marked up as events. Lastly, the TimeML schema was adapted to represent the grammatical tense/aspect system of French, and to account eg. for the imparfait (IMPERFECT), not grammaticalised in English.

FTiB is made up of 108 newspaper texts for a total of 16 208 tokens. 2 098 of these represent events. Since in our experiments, we are interested in assessing factuality at the sentence level, we segmented FTiB into (814) sentences, and extracted from them the subordination links (SLINKs and ALINKs). Overall, FTiB contains 485 subordination links. Luckily, the subordinating events in 444 of these links are ESPs. From these links, we selected those where the subordinating event was a translation of an English verb for which we have a signature (179, instantiating 49 different verbs). We first checked for the 49 types whether the French predicate has the same signature as the English verb it translates. We found that this was very roughly the case for most of these verbs (but see below). For example, the factive signature '+ + | -+' of learn that is inherited by its translation apprendre que. Similarly, the implicative signature '+ -|n' of help also characterises its French translation aider à. Our translation approach raised several interesting issues, however. A first one concerns verbs with a syntax-dependent factuality profile. In English, learn that/forget that for instance have the (factive) signature + + | -+, whereas learn to is less biased wrt. the factuality of the embedded event, and forget to has the (implicative) signature + -| -+. French translations of these verbs also quite systematically see their signatures varying with the syntactic structure, or have an argument structure that its English counterpart cannot instantiate; see e.g. the factive VP apprendre sa mort (lit. '*learn his death'). For these cases, we paired the relevant reading with the appropriate signature manually. A second issue is raised by verbs with an aspect-dependent factuality profile. It is well-known that in Romance, modal verbs trigger an actuality entailment under some of their readings, but with a perfective only. For instance, the example (3), where the modal verb permettre has an enable reading and is combined with a perfective (PFV), triggers an actuality entailment (the embedded event has to happen). With an imperfective (IMP), however, the actuality entailment vanishes, cf. (4). Also, when the same verb permettre has a deontic ('grant permission') reading, no actuality entailment is triggered, even with a perfective, see (5) (Hacquard 2006:41) Our translations of the English verbs analysed by [START_REF] Nairn | Computing relative polarity for textual inference[END_REF] revealed that several other French verbs show the same lability, see Table 3. That is, the entailment triggered with the perfective is lost with an imperfective, or at least replaced by a defeasible inference, see e.g. the examples ( 6)-( 7). NEG escape-PFV 'At that moment, she 'was managing' to escape. But finally, she didn't escape.' Interestingly, most of these predicates with an aspect-dependent inferential profile (12 out of 13 in the current stage of annotation) are implicative verbs. On the other hand, verbs whose inferential profile is independent from aspect are mostly factive (+ + | -+) verbs (17 out of 23). The verb savoir illustrates well the point. Used as a translation of the English factive verb know, savoir is factive both with PFV and IMP. However, savoir is also used in the FTiB as a two-way implicative verb (+ + | --), see ( 8)-( 9). In the latter use, savoir has an abilitative reading and like être capable de 'be able to', triggers an actuality entailment with PFV, see ( 8), but has a neutral inferential profile with IMP (+n|n), see ( 9). Why do implicative verbs (contrary to factive verbs) lose their entailment when combined with IMP? Recent analyses of implicative verbs by [START_REF] Baglini | The Implications of Managing[END_REF] and [START_REF] Nadathur | Causal necessity and sufficiency in implicativity[END_REF] can help to explain this observation. According to Baglini & Francez' analysis, a manage p statement presupposes familiarity with a causally necessary but insufficient condition A for the truth of p, and asserts that A actually caused the truth of p. Nadathur extends a modified version of this analysis to the whole class of implicative verbs. The important point for us is that under these analyses, implicative verbs have an at-issue component: they assert an 'event', namely the obtaining/actualisation of the causal factor A for the truth of p. Given the 'imperfective paradox', the imperfective form of such verbs unsurprisingly suspends the actualisation event, as what happens with the imperfective form of overtly causative verbs (e.g. Trump was causing a new catastrophe when Pence stopped him does not entail the occurrence of a new catastrophe). On the other hand, factive verbs like savoir que p 'know that p' do not assert the obtaining of a causal factor for the truth of p, but rather a mental state having p as its object. We therefore do not expect aspect to interfere with their inferential profile. For these verbs with an aspect-dependent aspectual profile (including plainly modal ones)5 , we manually annotated the reading instantiated and the corresponding signature in the FTiB. The third interesting point raised by our translation is illustrated by French verbs having a different factuality profile than their English counterparts. For instance, although pousser à is used to translate the implicative verb provoke to, it is not implicative with an agent subject, even with a perfective (contrary to its near synonym conduire à).

Ongoing research

These experiments showed that verbs whose factuality profile varies with the reading selected and/or its argument structure are very pervasive among French ESPs. A lexicon of ESPs should therefore carefully distinguish between the different readings/argument structures an ESP may instantiate. Also, they suggest that interesting new correlations can be found between event factuality profiles on one hand, and particular sets of syntactic/semantic properties on the other. For instance, verbs like refuser 'refuse/fail' are two way implicative verbs with an inanimate subject or with an animate subject controlling the complement, cf. ( 10)-( 11), but only trigger a strong (but nevertheless defeasible) inference with a matrix subject distinct from the infinitival subject, see ( 12). ( 10 To find these correlations, we are building a French lexicon of ESPs on top of a rich lexicon encoding morphological, syntactic and semantic properties of French verbs for each of their readings, "Les verbes français" [START_REF] Dubois | Les Verbes français[END_REF][START_REF] François | Présentation de la classification des Verbes Français de Jean Dubois et Françoise Dubois-Charlier[END_REF]. In the first step, we use the French verbs analysed in our experiments as seeds, link them with each of their readings in Les verbes français, and provide a manual signature for all of their other ESP readings. This will hopefully give an idea of the semantic and syntactic properties characterising each factuality profile. In the second step, we will enrich the different subclasses of ESPs (distinguished by their signature) with similar candidates by using (semi-)automatic methods along the lines of those described in [START_REF] Richardson | Light textual inference for semantic parsing[END_REF][START_REF] De | Sensespecific implicative commitments[END_REF][START_REF] Steven | A computational model of s-selection[END_REF][START_REF] Eckle-Kohler | Verbs Taking Clausal and Non-Finite Arguments as Signals of Modality -Revisiting the Issue of Meaning Grounded in Syntax[END_REF], and then review them manually.

Table 1 :

 1 CT+ CT-CTu PR+ PR-PRu PS+ PS-PSu Uu Uu Uu fail (a) CT-CT+ CTu PR-PR+ PRu PS-PS+ PSu Uu Uu Uu Sample lexical entries for NSIPs. CT, PR and PS signify certain, probable and possible respectively, U (and/or u) unspecified (unknown or uncommitted), (a) refers to the anchor.

					Contextual factuality
			CT			PR			PS			U
	polarity	+	-	u	+	-	u	+	-	u	+	-	u
	manage (a) Polarity of ESP		Sample
		+	-		predicate
	2-way	+	-		manage to
	implicatives	-	+		fail to
	1-way	+	n		force to
	+implicatives -	n		refuse to
	1-way	n	-		attempt to
	-implicatives	n	+		hesitate to
	factives	+	+		forget that
	counterfactives -	-	pretend that
	Neutral	n	n		want to

Table 2 :

 2 Semantic classification of complement taking verbs wrt. the effect of the polarity of the main clause (ESP, head row) on the factuality of the complement clause (embedded event, subsequent rows). n stands for none.

  .

	(3) Cette	carte	m'a permis	d'entrer.
	This	card	me permit-PFV	to enter
	→ I entered.
	(4) Cette	carte	me permettait	d'entrer.
	This	card	me permit-IMP	to enter
	→ I entered.
	(5) Le	doyen	m'a permis	d'entrer.
	The	dean	me permit-PFV	to enter
	→ I entered.

Table 3 :

 3 Examples of verbs whose inferential profile varies with the aspect used. Certain events are labelled '+', very likely but not certain events, '+ * ', counterfactual events, -, very unlikely events '- * '.

	(6) A	ce	moment-là,	elle	a réussi	à
	at	that	moment		she	manage-PFV	to
	s'enfuir.	#Mais	finalement,	elle
	escape	but	finally	she
	ne s'est pas enfuie.
	NEG escape-PFV
	'At that moment, she managed to escape.
	But finally, she didn't escape.'
	(7) A	ce	moment-là,	elle	réussissait
	at	that	moment		she	manage-IMP
	(encore)	à	s'enfuir.	OK Mais
	(still)	to	escape		but
	finalement,	elle	ne s'est pas enfuie.
	finally		she

)

  Le tiroir a refusé de s'ouvrir, #mais il s'est ouvert quand même. 'The drawer failed to open, but it opened nevertheless.' (11) Marie a refusé d'entrer, #mais elle est entrée quand même. 'Marie refused to enter, but she entered nevertheless.' (12) Le garde a refusé que Marie entre, OK mais elle est entrée quand même. 'The guard refused to allow Marie to enter, but she entered nevertheless.'

The lexicon layout for SIPs, less relevant for our study, is very similar except that an SIP lexicon entry must also provide factuality values for the cogniser source in addition to the anchor.

 2 The ESP lexicons created in[START_REF] Saurí | Are you sure that this happened? assessing the factuality degree of events in text[END_REF] are not freely available.

Factive and implicative verbs are typically non-source introducing predicates (NSIPs).

These resources are available at https://web. stanford.edu/group/csli_lnr/Lexical_ Resources/.

FTiB has only 32 instances of devoir, 8 of falloir and 21 of pouvoir.


Antoine Criniere
email: antoine.crinière@ifsttar.fr

Jean Dumoulin

Laetitia Perez

Fréderic Bourquin

Thermographie infrarouge synchronisée avec la mesure de paramètres météorologiques : Application à l'auscultation du tablier d'un pont ouvert au trafic

Résumé -Cet article présente un monitoring thermique conduit pendant plusieurs jours sur le tablier du pont de « Musmeci » à Potenza (Italie). L'analyse des données est conduite en exploitant la mesure de paramètres météorologiques synchronisée avec l'acquisition d'images thermiques. Une analyse par FFT, permet de détecter sur les séquences de cartes d'amplitude et de phase la structure interne du tablier. Un modèle thermique exprimé dans le domaine fréquentiel a été développé et couplé à une procédure d'estimation de paramètres. Une cartographie de la distribution spatiale de la conductivité thermique apparente est ainsi calculée puis comparée avec l'analyse d'images par approche fréquentielle.

Introduction

Parmi les axes de recherche conduit au sein de l'IFSTTAR la maîtrise du vieillissement, des risques et les nuisances est un thème qui englobe la résistance au temps et aux agressions du milieu naturel. Au sein de cet axe, la durabilité des ouvrages est un enjeu primordial d'ordre économique mais aussi de sécurité pour l'usager. Le diagnostic de l'état des ouvrages fait donc l'objet de nombreux travaux de recherche que ce soit au niveau de l'instrumentation ou des outils d'analyse de données acquises sur ouvrages avec de nouveaux dispositifs d'auscultation. Parmi les différentes techniques non destructives étudiées, la surveillance des structures par thermographie infrarouge, couplée aux avancées des technologies de l'information et de la communication [START_REF] Argenti | ISTIMES: Integrated System for Transport Infrastructures Surveillance and Monitoring by Electromagnetic Sensing[END_REF], apparait comme une voie de recherche à explorer. Un système de mesure par thermographie infrarouge, adapté à un tel contexte de mise en oeuvre et d'exploitation, a été étudié et développé [START_REF] Dumoulin | Developement of an infrared system coupled with a weather station for real time atmospheric correction using GPU computing: Application to bridge monitoring[END_REF]. Ce système de mesure a été déployé sur différentes structures de Génie Civil dans le cadre du projet européen ISTIMES [START_REF] Proto | Transport Infrastructure Surveillance and Monitoring by Electromagnetic Sensing: The ISTIMES Project[END_REF]. Les résultats que nous présentons dans cet article s'appuient sur des données acquises, pendant plusieurs jours sur le tablier du pont de « Musmeci » à Potenza (Italie).

Une présentation de l'ouvrage, du système de mesure déployé sans interrompre la circulation et des mesures obtenues est faite. Par la suite deux méthodes d'analyse sont présentées. La première couramment utilisée en contrôle non destructif par thermographie infrarouge active s'appuie sur l'utilisation de la FFT. La deuxième s'appuie sur une modélisation thermique par la méthode des quadripôles thermiques dont la résolution se fait dans le domaine fréquentiel. Les conditions aux limites (flux solaire, flux convectif) sont calculées à l'aide de modèles disponibles dans la littérature et des données mesurées sur site. Une procédure d'estimation de paramètres adaptée à de telles données est proposée. Au final une cartographie de la conduction thermique apparente en surface du tablier du pont est calculée. Les résultats obtenus par ces deux approches sont analysés et des perspectives sont proposées.

Dispositif expérimental et mesures réalisées sur ouvrage

Le pont de Musmeci (Viadotto dell'Industria), situé sur la commune de Potenza en Italie a été conçu par l'architecte Sergio Musmeci . Sa construction a été achevée en 1975. La figure 1 présente une vue de cet ouvrage en béton. Dans le cadre du projet européen ISTIMES [START_REF] Proto | Transport Infrastructure Surveillance and Monitoring by Electromagnetic Sensing: The ISTIMES Project[END_REF], différentes techniques de mesure en vue d'ausculter cet ouvrage ont été testées pendant une semaine l'approche par thermographie infrarouge en surveillance continue pendant 3 jours.

Le système de mesure déployé

Ce système s'articule autour d'un mini-PC® Zotac. Il intègre le système d'information développé pour l'architecture web du projet ISTIMES, mais permet également la synchronisation et le stockage des différentes données acquises. Un schéma de principe est présenté sur la figure 2. Un GPS (positionnement + datation des données), une camera infrarouge FLIR® A320 et une station météo VAISALA® WXT520 sont connectées au système conçu pour fonctionner de manière autonome. Le système assure la mise à disposition des données sur un réseau wifi privé. Un PC de contrôle peut être utilisé localement afin de paramétrer le système. Il autorise également la récupération asynchrone des données. Lors des essais, le mini-PC a été placé dans un boitier étanche sous le pont. La caméra infrarouge et la station météo ont été fixées sur un mât de 6m (figure 3). Le mât était positionné au niveau du garde corps du pont. La figure 4 présente de manière schématique le champ de vue de la caméra infrarouge reportée sur une photographie de la surface du tablier de ce pont.

Les données mesurées

Durant cette expérimentation, le suivi du champ de température de surface a été réalisé par thermographie infrarouge avec une fréquence d'échantillonnage d'environ 0.083 Hz obtenu par moyenne d'images en cours d'acquisition. L'évolution de la température de l'air et de la vitesse du vent faisait l'objet de mesures en parallèle avec une fréquence d'échantillonnage de 0.0167 Hz. Le suivi de l'évolution de l'humidité relative constituait un des paramètres d'entrée pour corriger en temps réel les mesures infrarouges [START_REF] Dumoulin | Developement of an infrared system coupled with a weather station for real time atmospheric correction using GPU computing: Application to bridge monitoring[END_REF] avant stockage. La figure 5 présente l'évolution de la température de surface en un point du tablier extraite de la séquence d'images infrarouges, mais aussi l'évolution de la vitesse du vent et de la température de l'air durant l'essai sur site.

Figure 5 Evolution des Températures de surface et d'air et de la vitesse du vent

On constate sur cette figure que, pendant les deux premiers jours, les vitesses du vent entre le jour et la nuit varient périodiquement. Puis le dernier jour un épisode de vent intense dans la journée se traduit par une chute de la température de surface de l'ouvrage.

Structure du tablier

Une coupe transversale du tablier et une vue 3D de la structure interne des dalles utilisées pour le tablier du pont sont reportées sur la figure 6.

Modélisation thermique

Dans ce paragraphe nous décrivons le modèle thermique étudié et la procédure d'estimation utilisée pour construire une cartographie des conductivités thermiques apparentes à partir des données mesurées.

Modélisation du tablier du pont

Les mesures acquises présentent un comportement périodique quasi établi si l'on focalise notre analyse sur les deux premières journées de mesure. Le système à résoudre peut donc être exprimé en utilisant la notion d'amplitude complexe [START_REF] Crinière | On the feasibility of defect detection in composite material based on thermal periodic excitation[END_REF] [START_REF] Autrique | On the use of periodic photothermal methods for materials diagnosis[END_REF]. Son expression est reportée dans l'équation 1. De plus, compte-tenu de l'épaisseur totale du tablier du pont, de sa nature et de la période des sollicitations thermiques naturelles observées sur quelques cycles journuit, une condition de flux nul peut être appliquée sur le dessous du tablier.

2 2 0 () () () () () 0 a n n a n a n a x n a a xe T j T x T k x T k x                                     (1)
Enfin le tablier est assimilé à un milieu monocouche en considérant des propriétés thermiques apparentes. Cette simplification permet de s'affranchir en première approche de la géométrie 3D du tablier. Les différentes variables temporelles du système sont exprimées dans le domaine fréquentiel à l'aide de la transformée de Fourier, équation 2.

  0 1 ( ) ( ) exp 2 p n t jt n T T t dt        (2)
Le gradient thermique présent initialement dans la structure est inconnu. L'obtention du gradient de température au sein du milieu est approchée par répétition sur 10 périodes l'intervalle temporel pris en considération lors du calcul. La procédure d'identification est effectuée sur la septième période. La résolution du système est effectuée à l'aide des quadripôles thermiques [START_REF] Maillet | Thermal Quadrupoles Solving the Heat Equation through Integral Transforms[END_REF], exprimé dans l'équation 3 en considérant un matériau constitué d'une couche.

        0 0 1 cosh sinh ( ) ( ) ( ) ( ) 0 0
                                                                                                              (3)
Le retour dans le domaine temporel s'effectue alors à l'aide de la transformée de Fourier inverse, équation 4.

  0 () 1 ( 0, ) ( ) exp ) 2 fin n j n m n n n A T x t T d C               (4)

Réduction du volume de données et prise en compte des flux convectif et solaire

Afin de réduire le volume de données à traiter et d'optimiser le processus de calcul utilisé, la période journalière présentant le moins de perturbations a été utilisée et sous-échantillonnée à 0.0083Hz. Les données sous-échantillonnées sont présentées sur la figure 7.

La détermination du flux global en surface du tablier s'appuie sur l'identification du flux convectif et du flux solaire en surface du tablier.

Le transfert de chaleur convectif dû au vent en surface de l'ouvrage doit être pris en considération. Le coefficient de transfert de chaleur par convection est donc calculé pour chaque mesure de vitesse du vent en utilisant les corrélations de McAdams [START_REF] Mcadams | Heat Transmission[END_REF]. La figure 7 présente son évolution au cours du temps.

Procédure d'identification de paramètres thermiques apparents

La procédure d'identification étudiée requiert la mise en oeuvre d'un filtrage sur les différentes données de mesure brutes en entrée du calcul. Ce filtrage permet de réduire l'influence des événements trop rapides qui perturbent le modèle vis-à-vis du signal moyen étudié sur 24 h. Ainsi un filtre passe bas de Butterworth [START_REF] Butterworth | On the Theory of Filter Amplifiers[END_REF] a été appliqué à chaque donnée en entrée. Les fréquences de coupure et l'ordre des filtres sont reportés dans le tableau 2.

  _0 ( ) ( ) ( ) filtré éxterieure filtrée filtrée t h t T Mesure t     (5)
La figure 9 présente l'évolution des différents flux calculés en surface du tablier. L'algorithme de minimisation choisi est l'algorithme de Levenberg-Marquardt [START_REF] Marquardt | An Algorithm for Least-Squares Estimation of Nonlinear Parameters[END_REF].

Analyse des résultats

Application du modèle thermique en deux points du tablier

Avant d'appliquer la procédure d'estimation à une séquence d'images thermiques complète, nous présentons les résultats obtenus en deux points de la surface du tablier. L'un au droit d'une paroi en béton d'un caisson interne et l'autre au dessus de la partie évidée d'un caisson. Les conductivités thermiques apparentes estimées sont de 1.75 W/m.°C au droit d'une paroi et 1.8 W/m.°C au dessus de la parie évidée. La conductivité apparente calculée au niveau d'une paroi du caisson est de l'ordre de grandeur de la conductivité équivalente estimée dans le cas d'une connaissance a priori de paramètres [START_REF] Maillet | Thermal Quadrupoles Solving the Heat Equation through Integral Transforms[END_REF]. La conductivité apparente calculée au dessus d'une partie vide d'un caisson est éloignée de la valeur de la conductivité équivalente calculée en considérant de l'air en troisième couche. Cet écart pourrait être dû à un coffrage perdu en bois utilisé lors de la fabrication sur site des dalles avec caisson. La figure 11 présente une comparaison entre la température mesurée et la température reconstruite après la procédure d'estimation sur une période.

Application du modèle thermique à la séquence d'images infrarouge et comparaison avec une analyse par FFT

La caméra infrarouge utilisée a une résolution spatiale 320x240 pixels. Au sein de l'image, une zone de 240x200 pixels a été extraite au centre de la scène. Par la suite afin de réduire les temps de calcul, une moyenne spatiale sur quatre pixels a été appliquée. Ainsi la séquence d'images thermiques traitée a une résolution spatiale de 120x100 pixels. La figure 12 présente une image thermique sous échantillonnée spatialement et acquise le premier jour de la campagne d'essai à 12h30 GMT. En parallèle une analyse fréquentielle a été appliquée à cette même séquence d'images. Une FFT [START_REF] Cooley | An algorithm for the machine calculation of complex Fourier series[END_REF] est appliquée sur l'évolution temporelle de chaque pixel. L'analyse des cartes de phase et d'amplitude calculées permet de détecter à certaines fréquences la structure interne du tablier. La figure 14 présente la valeur en amplitude de la deuxième harmonique du signal et la figure 15 la valeur en phase de la cinquième harmonique. La cartographie de conductivité apparente montre que le modèle étudié permet de détecter et caractériser les changements de propriétés dans l'épaisseur du tablier. Le premier caisson de béton est notamment bien visible. En revanche, l'état de surface de la structure, les ombres portées et la distorsion spatiale due au champ de vision de la caméra influent sur la sortie du modèle. Pour l'analyse fréquentielle les zones situées en haut à gauche et en bas à droite présentent une dégradation de la qualité de la détection sur la carte d'amplitude pour l'une et celle de phase pour l'autre. Ces mêmes zones influences la procédure d'estimation.

Conclusion

Le travail conduit dans cette étude s'est appuyé sur des données acquises pendant plusieurs jours sur un pont ouvert au trafic. Le système de mesure utilisé sur site mettait en oeuvre une caméra infrarouge à matrice de microbolomètres et une station météorologique connecté à un système d'information adapté. L'analyse des séquences d'images infrarouges a été conduite par FFT puis à l'aide d'un modèle thermique et d'un protocole d'identification de la conductivité thermique apparente développé et étudié dans le cadre de ce travail. Un avantage de l'approche thermique est de conduire à une cartographie unique alors que l'approche par FFT requiert d'analyser les séquences de cartes de phase et d'amplitude. A contrario le temps de calcul est loin d'être aussi performant que l'approche par FFT, toutefois la parallélisation des calculs sur GPU devrait permettre un gain en temps de calcul très significatif. La cartographie des cartes de conductivité thermique apparente ouvre aussi la voie au suivi sur le long terme d'un possible indicateur d'état de la structure en lien avec le vieillissement des matériaux constitutifs d'une structure soumise aux aléas climatique et au trafic.

2

 2

Figure 1

 1 Figure 1 Pont de Musmeci Figure 2 Système d'information utilisé

Figure 3 Figure 4

 34 Figure 3 Schéma de montage de la camera

Figure 6

 6 Figure 6 Schéma du pont

Figure 7 Figure 8

 78 Figure 7 Mesures sous-échantillonnées à 0.0083Hz

Tableau 2

 2 Paramètres des filtres de Butterworth Les données filtrées (figure 9) sont utilisées pour le calcul du flux solaire 0 () t  et le calcul du flux convectif en s'appuyant sur le calcul du coefficient de transfert de chaleur convectif h(t). La connaissance de ces deux flux permet alors d'en déduire le flux global () t  en surface du tablier, équation 5.

Figure 9

 9 Figure 9 Calcul du flux de surface La répétition de la période d'étude conduit également à rendre le coefficient d'échange convectif périodique. La procédure d'estimation étudiée et mise en oeuvre vise à déterminer des paramètres apparents du système. La figure 10 présente un schéma d'ensemble de la procédure d'estimation proposée.

Figure 10

 10 Figure 10 Procédure d'estimation Figure 11 comparaison mesureestimation

FigureFigure 14

 14 Figure 12 Température de surface Figure 13 Cartographie de conductivité apparente