Denis Poitrenaud

Etienne Renault

Combining Parallel Emptiness Checks with Partial Order Reductions

 shown that the best performance is currently obtained using their multi-core SCC-based emptiness check. However, combining the latest SCC-based algorithm with POR is not trivial since a condition on cycles, the proviso, must be enforced on an algorithm which processes collaboratively cycles. In this paper, we suggest a pessimistic approach to tackle this problem for liveness properties. For safety ones, we propose an algorithm which takes benefit from the information computed by the SCC-based algorithm. We also present new parallel provisos for both safety and liveness properties that relies on other multi-core emptiness checks. We observe that all presented algorithms maintain good reductions and scalability.

Introduction and Related Work

The automata-theoretic approach to explicit Linear-time Temporal Logic (LTL) model checking explores finite Labeled Transition Systems (LTS). Unfortunately, LTS are often too large to be fully explored in reasonable time and applying sequential algorithms becomes impractical. To tackle this well-known state explosion problem, various techniques have been suggested. In this paper we focus on the combination of two of them: Partial Order Reduction (POR) and multi-core emptiness checks.

POR exploits the interleaving semantics of concurrent systems by only considering representative executions [START_REF] Valmari | Stubborn sets for reduced state space generation[END_REF][START_REF] Peled | Combining partial order reductions with on-the-fly model-checking[END_REF][START_REF] Laarman | Guard-based partial-order reduction[END_REF] rather than all possible permutations of the execution of n independent actions (i.e. n! possible interleavings). The selection of the representative executions is performed on-the-fly while exploring the LTS: for each state, the exploration algorithm only considers a nonempty (reduced) subset of all enabled actions, such that all omitted actions are "independent" from those in the reduced set. The execution of omitted actions is then postponed to a future state. The reduced LTS is sufficient to check reachability problems (e.g. existence of a global deadlock). However, for LTL model checking, 1 only stuttering-invariant formula (e.g. not using the Next operator) can be verified. In addition to this restriction on formulas that can be checked, a complementary condition, called a proviso, must be enforced. If the same actions are consistently ignored along a cycle, the reduction may miss some undesirable behavior. When checking liveness properties, a sufficient condition is to force every cycle of the reduced LTS to contain at least one fully expanded state i.e. a state for which all actions are considered. When checking safety properties, forcing every (non-deadlock) state to have at least one fully expanded successor (direct or indirect) is sufficient.

An emptiness check for LTL model checking is an algorithm looking for a counterexample in the state space of the system. A counterexample is simply a lasso-shaped execution, i.e. a particular cycle reachable from the initial state.

The best multi-core emptiness checks are based on a Depth-First Search (DFS) exploration [START_REF] Bloemen | Multi-core scc-based ltl model checking[END_REF] and can be classified into two categories: those based on a Nested Depth First Search (NDFS) [START_REF] Evangelista | Improved multi-core nested depth-first search[END_REF], and those based on an enumeration of Strongly Connected Components (SCC) [START_REF] Renault | Variations on parallel explicit model checking for generalized Büchi automata[END_REF][START_REF] Bloemen | Multi-core scc-based ltl model checking[END_REF]. While the algorithm of Renault et al. [START_REF] Renault | Variations on parallel explicit model checking for generalized Büchi automata[END_REF] performs a state-based DFS exploration, one can note that the one suggested by Bloemen and van de Pol [START_REF] Bloemen | Multi-core scc-based ltl model checking[END_REF] performs a DFS over SCCs rather than states which makes the detection of individual cycles more difficult. All these concurrent algorithms are based on the swarming technique [START_REF] Holzmann | Swarm verification techniques[END_REF]: multiple threads, with their own exploration order, are spawned from the initial state. Additionnaly, in best concurrent emptiness checks [START_REF] Evangelista | Improved multi-core nested depth-first search[END_REF][START_REF] Renault | Variations on parallel explicit model checking for generalized Büchi automata[END_REF][START_REF] Bloemen | Multi-core scc-based ltl model checking[END_REF], each thread shares information to prune the exploration of the others. Bloemen and van de Pol [START_REF] Bloemen | Multi-core scc-based ltl model checking[END_REF] have shown recently that their SCC-based algorithm provide actually the best results. This algorithm uses a (lock-free) concurrent union-find data structure that centralizes all the shared information. This structure is adapted with a work stealing mechanism.

In a sequential setting, provisos for emptiness checks have been well studied these last years [START_REF] Nalumasu | An efficient partial order reduction algorithm with an alternative proviso implementation[END_REF][START_REF] Evangelista | Solving the ignoring problem for partial order reduction[END_REF][START_REF] Duret-Lutz | Heuristics for checking liveness properties with partial order reductions[END_REF][START_REF] Hansen | Safety property-driven stubborn sets[END_REF][START_REF] Valmari | More stubborn set methods for process algebras[END_REF]. The in-stack proviso introduced by Peled [START_REF] Peled | Combining partial order reductions with on-the-fly model-checking[END_REF] and implemented in Spin has been improved by Evangelista and Pajault [START_REF] Evangelista | Solving the ignoring problem for partial order reduction[END_REF] with several mechanisms to reduce the number of expansions during a DFS exploration. Some of these mechanisms have then been deconstructed by Duret-Lutz et al. [START_REF] Duret-Lutz | Heuristics for checking liveness properties with partial order reductions[END_REF] to build new provisos (for liveness properties) that outperform the previous ones. These authors also proposed original provisos that can exploit the SCC information when the underlying emptiness check computes it. Other provisos have also been suggested (but not evaluated) in the more complex context of process algebra to consider τ -transitions [START_REF] Hansen | Safety property-driven stubborn sets[END_REF][START_REF] Valmari | More stubborn set methods for process algebras[END_REF]. Some works also focus on non-DFS based emptiness checks [START_REF] Bosnacki | Partial-order reduction for general state exploring algorithms[END_REF][START_REF] Bošnaȃźki | Partial-order reduction for general state exploring algorithms[END_REF] thus defining new ways to detect potential ignoring cycles based on quadratic algorithms.

In a multi-core setting, POR has been less studied. Barnat et al. [START_REF] Barnat | Parallel partial order reduction with topological sort proviso[END_REF] suggested an approach based on a topological sort which sounds hard to combine efficiently with state-of-the-art parallel emptiness checks (see Laarman and Faragó [14]). Lerda and Sisto [START_REF] Lerda | Distributed-memory model checking with spin[END_REF] proposed an adaptation of the in-stack proviso without knowing the entire DFS stack. More recently, Laarman and Wijs [START_REF] Laarman | Partial-order reduction for multi-core ltl model checking[END_REF] worked on the adaption of the in-stack proviso with the best multi-core NDFS-based emptiness check [START_REF] Evangelista | Improved multi-core nested depth-first search[END_REF] and achieved good reductions and good scalability.

Even if it has been shown that the best current performance is obtained using multi-core SCC-based emptiness checks, these algorithms have not yet be combined with POR due to several problems. For liveness properties, multi-core lw14 Laarman and Wijs [START_REF] Laarman | Partial-order reduction for multi-core ltl model checking[END_REF] dfs-pr19-safe dfs-pr19-live scc-pr19-safe elpp12 Evangelista et al. [START_REF] Evangelista | Improved multi-core nested depth-first search[END_REF] rdkp16 Renault et al. [START_REF] Renault | Variations on parallel explicit model checking for generalized Büchi automata[END_REF] ep10 Evangelista and Pajault [START_REF] Evangelista | Solving the ignoring problem for partial order reduction[END_REF] dkpr16-live

Duret-Lutz et al. [START_REF] Duret-Lutz | Heuristics for checking liveness properties with partial order reductions[END_REF] hpy96 Holzmann et al. [START_REF] Holzmann | On nested depth first search[END_REF] c99

Couvreur SCC-based emptiness checks compute SCCs rather than particular cycles while the proviso relies on detecting cycles. For safety properties, the expansion of a single state in each SCC without successor is enough but has never been realized in a multi-threaded context.

Figure 1 summarizes the contributions of this paper (in green). First, we aim at experimentally demonstrating that the improvements suggested in dkpr16 in a sequential setting can be shifted to multi-core one. dfs-pr19-live and dfs-pr19-safe correspond to this adaptation. We can notice that both are compatible with the emptiness checks elpp12 and rdkp16. After recalling necessary definitions in Section 2, we introduce in Section 3 these two new provisos and suggest a new one for safety properties scc-pr19-safe. This last proviso exploits the underlying SCC computation of rdkp16. Section 4 introduces two last provisos ws-pr19-live and ws-pr19-safe. These algorithms are the first provisos compatible with the bp16 emptiness check. Section 5 evaluates the performances of our provisos and shows that all of them achieve a reduction comparable to the state-of-the-art while maintaining a good scalability.

Preliminaries

A Labeled Transition System (LTS) is a tuple L = V, v 0 , Act, δ where V is a finite set of states, v 0 ∈ V is a designated initial state, Act is a set of actions and δ ⊆ V × Act × V is a (deterministic) transition relation where each transition is labeled by an action. If (s, α, d) ∈ δ, we say that d is a successor of s. We denote by post(v) the set of all successors of v ∈ V .

A path between two states v, v ∈ V is a finite and non-empty sequence of adjacent transitions ρ

= (v 1 , α 1 , v 2 )(v 2 , α 2 , v 3 ) . . . (v n , α n , v n+1 ) ∈ δ + with (a) (b) (c) (d)
Fig. 2. Black nodes and plain edges represent the DFS stack, dashed edges represent

(not yet visited) back edges, and starred states corresponds to already expanded states. In (a) and (b) conditional provisos do not require an expansion. In (c) and (d), the source or the dest of the back edge should be preventively expanded. The liveness proviso of Evangelista and Pajault [START_REF] Evangelista | Solving the ignoring problem for partial order reduction[END_REF] will avoid the expansion in (d) since it is useless. For the purpose of partial-order reductions, an LTS is equipped with a function reduced : V → 2 V that returns a subset of successors reachable via a reduced set of actions. For any state v ∈ V , we have reduced (v) ⊆ post(v) and reduced (v) = ∅ =⇒ post(v) = ∅. The reduced function must satisfy other conditions depending on whether we use ample set, stubborn set or persistent set [see 15, for a survey]. The algorithms we present do not depend on the actual technique used to compute reduced .

v 1 = v and v n+1 = v . When v = v
The function reduced preserves only two properties on the corresponding reduced LTS: the presence of deadlocks, i.e. states without successors, and the presence of an infinite sequence, i.e. a cycle. When checking more complex properties, i.e. LTL formulae (safety or liveness), some additional conditions must be enforced. The reduced function must be restricted to reflect the variations of the Boolean values of the atomic propositions (appearing in the property). These extra conditions can easily be integrated in the computation of reduced .

However, the previous conditions do not prevent from continuously ignoring the same actions (in a cycle of the reduced LTS). This is the so-called ignoring problem. This problem can be solved using different provisos depending on the nature of the property, i.e. safety or liveness. These provisos rely on the presence of a (fully) expanded states in some cycles. A (fully) expanded state v is simply a state for which all the successors post(v) are considered in the reduced LTS even if reduced (v) is strictly included in post(v).

Provisos for emptiness checks applying a state-based DFS

Liveness properties. When checking liveness properties with POR and to ensure that no action will be ignored for ever, emptiness checks must ensure Algorithm 1: State-based DFS equipped (highlighted in yellow) for checking liveness properties with POR

1 ∀v ∈ V : v.status ← unknown 2 visited ← ∅ 3 ∀p ∈ [1 . . . n] : dfsp ← ∅ 4 dfs-pr19-live1(v0)|| . . . || dfs-pr19-liven(v0) 5 Procedure dfs-pr19-livep(v ∈ V ) 6 dfsp ← dfsp ∪ {v} 7 next ← reduced(v) 8 if next = post(v) then cas(v.status, unknown, expanded) 9 for v ∈ mixp(next) do 10 if v ∈ dfsp ∪ visited then dfs-pr19-livep(v ) 11 else if v ∈ dfsp ∧ v.status = unknown ∧ v .status = unknown then 12 cas(v .status, unknown, expanded)
13 cas(v.status, unknown, not expanded)

14 if v.status = expanded then 15 next ← post(v) \ reduced(v) 16 for v ∈ mixp(next) do 17 if v ∈ dfsp ∪ visited then dfs-pr19-livep(v ) 18 visited ← visited ∪ {v} 19 dfsp ← dfsp \ {v}
that every cycle contains at least one expanded state (i.e. a state for which all actions are considered). Notice that this property is an over-approximation but ensures that the ignoring problem is tackled correctly. Thus it could lead to useless expansions while all actions have been seen during a particular cycle but not containing any fully expanded state. Before diving into a multi-core setting, let us recall how this proviso property can be enforced for sequential DFS algorithms. Duret-Lutz et al. [START_REF] Duret-Lutz | Heuristics for checking liveness properties with partial order reductions[END_REF] suggested simple sequential provisos that are competitive with the state-of-the-art. During the DFS exploration of state v, the algorithm detects back edges, i.e. transitions (v, , v ) where v is already in the DFS stack. When detecting such transitions, a cycle has been detected. Then, the algorithm (1) checks if v or v is already expanded and if not (2) chooses to expand the source v, (exclusive) or the destination v . In both cases, the expansion of v or v ensures that the cycle closed by (v, , v ) contains at least one expanded state. Since all back edges discovered by the DFS cover all the elementary cycles, the property is respected. Figure 2 (a andb) describes cases where no expansion is required, while (c) describes a situation where an expansion is required (source or destination) and (d) a situation where a useless expansion is performed.

The aforementioned algorithms can be combined with a parallel swarmed exploration. Algorithm 1 (without highlighted lines) presents a swarmed exploration where all threads perform a state-based DFS exploration of the reduced state space. 2The n threads share a visited set (declared line 2) and each thread p maintains its own DFS set dfs p (line 3). The threads are spawned line 4. When a new state v is visited by a thread p, it is first added in the local set dfs p (line 6) and then a reduced set of successors is computed (line 7). These selected successors are explored in a randomized order (line 9). Each time a new state is discovered line 10, a recursive call is realized. After all the successors (not in dfs p ) has been inserted in visited, v can be itself added into visited and removed from dfs p (lines 18 and 19).

Highlighted lines implement a new parallel proviso for liveness properties. It is based on the combination of two ideas: (1) the conditional destination expansion as suggested by Duret-Lutz et al. [START_REF] Duret-Lutz | Heuristics for checking liveness properties with partial order reductions[END_REF] since it achieves good results in sequential settings and, (2) the sharing of the state status (unknown, expanded, not expanded) as presented by Laarman and Wijs [START_REF] Laarman | Partial-order reduction for multi-core ltl model checking[END_REF].

Initially, all states are tagged unknown (line 1). When an unknown state yielding no reduction is encountered line 8, its status is fixed to expanded by a compare-and-swap instruction. When a back-edge is detected between two unknown states (line 11), the destination is selected for expansion (line 12). Such an expansion is realized line 14 to 17 by considering the previously ignored successors. Before this expansion, the status of the state is checked. If this status is still unknown, no expansion is required for this state and its status can be fixed to not expanded (line 13).

Safety properties. When checking safety properties with POR and to ensure that no action will be ignored at all, emptiness checks must ensure that at least one expanded state is reachable from any visited state. Here again, this property is an over-approximation. Thus it could lead to useless expansions while all actions have been seen during a bottom SCC not containing an expanded state.

As for Algorithm 1, the highlighted lines in Algorithm 2 correspond to a proviso equipping a state-based DFS. This new proviso implements a conditional destination expansion mixed with a sharing of the state status. During the DFS exploration, the proviso of Laarman and Wijs [START_REF] Laarman | Partial-order reduction for multi-core ltl model checking[END_REF] systematically expands states having all its successors on the DFS stack. Here, we expand one of its destinations and only if the other destination are not already expanded. This is the first time that a safety proviso based on the expansion of a destination is proposed.

When visiting a state, the algorithm decides to expand it if its direct successors (in the reduced set) are all in its local DFS stack. The local variable allin (declared line 9) tracks if this condition holds. Initially, allin is true and set to false when the algorithm detects a direct successor not belonging to the DFS stack (lines 12 & 15). Line 14 implements the conditional expansion: allin stays true if all the direct successors are on the DFS stack but have an unknown status.

When a status has been fixed (different from unknown) for a state v, either v is itself expanded or an expanded state is reachable from it. In both cases, it is not necessary to expand its predecessor. Then, lines 17 and 18 are executed only if an expansion is required: a destination is chosen randomly and marked as to be expanded (just before the DFS will backtrack this state -line 20).

In the previous algorithm, multiple expansions can occur for a given SCC (see Figure 3). The next algorithm avoids expansion in non bottom SCC and try to limit the expansions only to the entry point of each bottom SCC. In a sequential settings, this leads to have at most one expansion per bottom SCC. Recently, a state-based parallel swarmed DFS computing SCC has been proposed [START_REF] Renault | Variations on parallel explicit model checking for generalized Büchi automata[END_REF]. Here, we adapt this algorithm to implement the aforementioned idea while exploiting the status sharing as in the previous algorithm. The unhighlighted lines of Algorithm 3 correspond to the one of Renault et al. [START_REF] Renault | Variations on parallel explicit model checking for generalized Büchi automata[END_REF]. The shared variable S maps to each state v, the set of states S(v) belonging to the same (partial) SCC. The shared set dead contains all states belonging to fully visited SCCs. Initially, for any state v, the set S(v) = {v}. Each thread p maintains two local variables, a stack roots p which contains the entry point of each traversed (partial) SCC and a set visited p holding each state visited by thread p. A local unique number v.num p (called the live number in the SCC computation proposed by Tarjan [START_REF] Tarjan | Depth-first search and linear graph algorithms[END_REF]) is associated to each state v (line 8). Each newly discovered state is considered as the root of an SCC and then inserted in the stack roots p line 9. This stack as well as the mapping S are updated each time a closing edge, i.e. a transition (v, , v ) such that v belongs t a partial SCC containing a state of the DFS stack, is detected (lines 21 to 23). The local unique number of states help to determine the effective root of the partial SCC: the stack is popped until this entry point becomes the top of the stack. The mapping S is updated to aggregate all the sets associated to popped states (line 23). Notice that the instruction line 23 must be atomic. When discovering the effective root v of a (complete) SCC (line 28), all states belonging (i.e. S(v)) to it are marked as dead atomically (line 35), thus restricting the visit by the other threads (line 15). The mapping S (and the set Algorithm 3: State-based DFS equipped (highlighted in yellow) for checking safety properties with POR -unhighlighted lines correspond to the SCC computation algorithm as presented in Renault et al. [START_REF] Renault | Variations on parallel explicit model checking for generalized Büchi automata[END_REF] dead) can be efficiently implemented using a lock-free version of an union-find data structure.

1 ∀v ∈ V : S(v) ← {v} 2 dead ← expanded ← ∅ 3 ∀p ∈ [1 . . . n] : visitedp ← ∅ 4 ∀p ∈ [1 . . . n] : rootsp ← ∅ 5 scc-pr19-safe1(v0)|| . . . || scc-pr19-safen(v0) 6 Function scc-pr19-safe(v ∈ V ) : Boolean 7 visitedp ← visitedp ∪ {v} 8 v.nump ← |visitedp| 9 rootsp.push(v) 10 next ← reduced(v) 11 isTerm ← reduced(v) = post(v) // S(
S(r) ← S(v ) ← S(r) ∪ S(v ) 24 if isTerm ∧ v ∈ expanded then 25 isTerm ← ⊥ 26 next ← post(v) \ reduced(v)
To limit the number of expansions, the algorithm expands only the root of each bottom SCC not already containing an expanded state. The local variable isTerm tracks such an SCC (line 11, 16 and 19). When popping the root of a bottom SCC (line 28) for which no expanded state has been already discovered, an expansion is realized (lines 30-33). However, a same bottom SCC may have different entry points for different threads. To limit the number of expansions, the algorithm detects some of these situations line 24.

Notice that the two first provisos presented in this section are compatible with most of the optimizations presented by Evangelista and Pajault [START_REF] Evangelista | Solving the ignoring problem for partial order reduction[END_REF] as well as the one suggested by Duret-Lutz et al. [START_REF] Duret-Lutz | Heuristics for checking liveness properties with partial order reductions[END_REF]. Moreover, these provisos can be integrated in any emptiness checks based on a state-based DFS swarm exploration for instance CNDFS [START_REF] Evangelista | Improved multi-core nested depth-first search[END_REF] or Renault et al. [START_REF] Renault | Variations on parallel explicit model checking for generalized Büchi automata[END_REF] algorithm. The latest presented proviso is only compatible with Renault et al. [START_REF] Renault | Variations on parallel explicit model checking for generalized Büchi automata[END_REF].

Provisos for SCC-based DFS emptiness checks

Provisos presented in the previous section are not compatible with the best currently known parallel emptiness check [START_REF] Bloemen | Multi-core scc-based ltl model checking[END_REF]. Until now, there is no proviso, neither for safety nor for liveness properties, for this model-checking algorithm. This algorithm differs from the previous ones since it does not perform a DFS in terms of states but only in terms of SCCs: in particular, the states of a same SCC may be visited (and processed) in any order. One can note that SCCs are still marked dead in a DFS post-order (see Algorithm 4 without highlighted lines). We denote this kind of algorithms as SCC-based DFS emptiness-checks.

The algorithm of Bloemen and van de Pol [START_REF] Bloemen | Multi-core scc-based ltl model checking[END_REF] has been introduced to tackle the main drawback of the algorithm suggested by Renault et al. [START_REF] Renault | Variations on parallel explicit model checking for generalized Büchi automata[END_REF]. Indeed, in this last algorithm, each SCC must be completely processed by the same thread before it can be marked dead. To improve this, Bloemen and van de Pol [START_REF] Bloemen | Multi-core scc-based ltl model checking[END_REF] introduced a work-stealing mechanism to allow SCCs to be cooperatively treated (see the outer loop line 9 of Algorithm 4). Notice that this mechanism induces a more complex shared union-find data-structure (see [START_REF] Bloemen | Multi-core scc-based ltl model checking[END_REF]).

In this approach, all threads start a DFS until they reach a (partial) SCC which is currently processed by one (or more) other thread(s). The states belonging to this SCC (aggregated by the DFS) are then distributed among the various threads (line 10) and marked done (line 27) when all their successors are dead or detected to belong to the current SCC. When the last state of an SCC is marked done, the SCC itself is marked dead (line 29). Liveness properties. Implementing a proviso for liveness properties in this algorithm is complex since the work stealing mechanism removes all possible knowledge about cycles in this SCC. When checking liveness properties, the proviso must ensure that each elementary cycle contains (at least) one expanded state. In sequential and for such a cycle, the states can be marked done by the algorithm in any order. Our proviso consists to expand any state with at least one successor marked done. In a sequential setting, this approach ensures that all cycles or size n > 1 contains at least one expanded state (n -1 for the worst case, n/2 in average).

However, in a parallel setting, this approach is not sufficient. Let us consider the example of Figure 4 with two threads, one visiting state a, the second state b, and with a and b known to belong to the same SCC. Thread t 1 selects a line 9, while thread t 2 selects b and both a and b are not already done. The test line 15 prevents from a recursive call (for both t 1 and t 2 ). Since a and b will only be marked done line 27, t 1 as well as t 2 will not detect that an expansion is required. Indeed, the only successor of a (resp. b) is not done.

To solve this problem, we introduce the shared sets wip p that represent states currently processed by a thread p. Highlighted lines of Algorithm 4 detail this new proviso for liveness properties. A state is inserted into wip p when first discovered by a thread p (line 10) and removed either line 28 when the state Algorithm 4: SCC-based DFS equipped (highlighted in yellow) for checking liveness properties with POR -unhighlighted lines correspond to the SCC computation algorithm as presented in Bloemen and van de Pol [START_REF] Bloemen | Multi-core scc-based ltl model checking[END_REF]

1 ∀v ∈ V : S(v) ← {v} 2 dead ← done ← expanded ← ∅ 3 ∀p ∈ [1 . . . n] : Rp ← wipp ← ∅ 4 ws-pr19-live1(v0)|| . . . || ws-pr19-liven(v0) 5 Procedure ws-pr19-livep(v ∈ V ) 6 Rp.push(v) 7 if v ∈ expanded ∧ post(v) = reduced(v) then 8 expanded ← expanded ∪ {v}
if v ∈ expanded ∧ w ∈ (done ∪ ( i∈[1...n] wipi)) \ expanded then 21 expanded ← expanded ∪ {w} 22 next ← next ∪ (post(v ) \ reduced(v )) 23 while w ∈ S(v) do 24 r ← Rp.pop() 25 t ← Rp.top() 26 S(r) ← S(t) ← S(r) ∪ S(t) 27 done ← done ∪ {v } 28 wipp ← wipp \ {v } 29 if S(v) ⊆ dead then dead ← dead ∪ S(v) 30 if v = Rp.top() then Rp.pop()
has been marked done or line 16 before performing a recursive call. Doing a recursive call ensures that state v will not be marked by the current while loop line 12. Indeed, when backtracking from the recursive call, line 18 the thread will realize a jump to the outer loop. This jump implies that all the successors of a state must be seen without performing a recursive call before this state is marked done. This is the main difference between our algorithm and the one of Bloemen and van de Pol [START_REF] Bloemen | Multi-core scc-based ltl model checking[END_REF]. Line 20 checks when an expansion is required. A state is expanded if one of its successors is done or belong to a wip p sets and neither the source nor the destination is expanded.

Notice that the introduction of the wip p sets also solves the expansion of the elementary cycles of size 1. As for the previous algorithms, the expanded set allows to share expansions between threads. Safety properties. As for liveness properties, a proviso for safety properties has never been proposed for the algorithm of Bloemen and van de Pol [START_REF] Bloemen | Multi-core scc-based ltl model checking[END_REF]. The goal, like in Algorithm 3, is to limit expansions only to bottom SCCs and to minimize the number of expansions in such SCCs. Detecting that the SCC is a bottom one can be done as easily as for Algorithm 3. A Boolean isT erm is associated to each SCC and updated consequently (lines 1, 8, 15, 18 and 29 of algorithm 5). Notice that this Boolean is associated to an SCC rather than a state in order to propagate the information inside of the work stealing mechanism.

Algorithm 5: SCC-based DFS equipped (highlighted in yellow) for checking safety properties with POR -unhighlighted lines correspond to the SCC computation algorithm as presented in Bloemen et al. [START_REF] Bloemen | Multi-core on-the-fly scc decomposition[END_REF]

1 ∀v ∈ V : S(v) ← {v}, S(v).isTerm ← 2 dead ← done ← expanded ← ∅ 3 ∀p ∈ [1 . . . n] : Rp ← ∅ 4 ws-pr19-safe1(v0)|| . . . || ws-pr19-safen(v0) 5 Procedure ws-pr19-safep(v ∈ V ) 6 if v ∈ expanded ∧ post(v) = reduced(v) then 7 expanded ← expanded ∪ {v} 8 S(v).isTerm ← ⊥ 9 Rp.push(v) 10 while pick v from (S(v) \ done) do 11 isExpanded ← v ∈ expanded 12 next ← isExpanded ? post(v ) : reduced(v ) 13 foreach w ∈ mixp(next) do 14 if w ∈ dead then 15 S(v ).isTerm ← ⊥ 16 else if ∃w ∈ Rp : w ∈ S(w ) then 17 ws-pr19-safep(w) 18 if w ∈ S(v ) then S(v ).isTerm ← ⊥ 19 else 20 while w ∈ S(v) do 21 r ← Rp.pop() 22 t ← Rp.top() 23 S(r) ← S(t) ← S(r) ∪ S(t)
if nb = S(v ) ∩ done then done ← done ∪ {v } 39 if S(v) ⊆ dead then dead ← dead ∪ S(v) 40 if v = Rp.top() then Rp.pop()
To implement the proviso, we can exploit a property of the original algorithm: when the last state of an SCC is marked done, the SCC is then marked dead. Capturing this instant could be useful to trigger an expansion in each bottom SCC. This approach, even if satisfying, does not work in the algorithm. Indeed, the algorithm is not aware that the state is the last one to be marked done.

To solve this problem, we propose a pessimistic approach (as previously). When a state is about to be marked done (lines 24 to 38), three situations may occur. First of all (line 27), the current state v is the last one of the bottom (partial) SCC: in this case, the state is expanded line 28 and the SCC does not require any more expansion, i.e. isT erm is set to false. Second of all (line 34-35), the state is about to be marked done while another thread required the expansion of this state. In this case, new successors must be explored for this state, and the break line 35 will force this exploration. Finally, two (or more) states may be concurrently candidate for being done. Line 25 and 38 prevent concurrent multiple insertions in the set done (and thus potentially missing a required expansion). Each thread captures line 25 the current number of done states in the (partial) SCC while line 38 checks that this number has not changed in between. This leads to sequentialize the insertions in done. Notice that line 38 must be performed atomically even if it contains a conditional statement.

Evaluation

Benchmark Description. To evaluate the performance of the new provisos, we selected 21 models from the BEEM benchmark [START_REF] Pelánek | BEEM: benchmarks for explicit model checkers[END_REF] that cover all types of models described by the classification of Pelánek [START_REF] Pelánek | Properties of state spaces and their applications[END_REF]. All the models were selected such that Algorithm 1 with one thread and without applying POR would take at most 20 minutes on Intel(R) Xeon(R) @ 2.00GHz with 250GB of RAM. We fix the maximum running time to 40 minutes. 3 Here we compute only a reduced LTS explored by the algorithms presented in the previous sections. When applied in the context of a model checker, the visited reduced LTS will be larger due to the observation of visible transitions [START_REF] Peled | Relaxed visibility enhances partial order reduction[END_REF]. Experiments were run three times and only the median of the three values were kept.

According to Bloemen et al. [START_REF] Bloemen | Multi-core on-the-fly scc decomposition[END_REF], the performances of parallel emptiness checks may rely on the underlying graph structure. To evaluate this, the 21 models selected are divided into two categories: M 1 (models with short cycles and many small SCCs) and M 2 (models with long cycles and a small number of large SCCs). Bloemen et al. [START_REF] Bloemen | Multi-core on-the-fly scc decomposition[END_REF] observe that the performances for the algorithm suggested by Renault et al. [START_REF] Renault | Variations on parallel explicit model checking for generalized Büchi automata[END_REF] are degraded for M 2 which is the motivation of the introduction of their new algorithm.

In this benchmark, we compared all the new algorithms presented in this paper with the only parallel provisos of the state-of-the-art, i.e lw14-live (see Algo. 1 in Laarman and Wijs [START_REF] Laarman | Partial-order reduction for multi-core ltl model checking[END_REF]),4 lw14-safe (see Algo. 2 in Laarman and Wijs [START_REF] Laarman | Partial-order reduction for multi-core ltl model checking[END_REF]). All the presented results have been computed using the same canvas and are then comparable. See Figure 1 for an overview of our contributions and the compatibility with existing emptiness checks.

Implementation Details. Since all the presented algorithms rely on hashtables and linked lists, they can be implemented lock-free. The reduced function implements the stubborn set method from Valmari [START_REF] Valmari | Stubborn sets for reduced state space generation[END_REF] as described by Pater [START_REF] Pater | Partial order reduction for pins[END_REF] but in a deterministic way, i.e. for any state s, reduced (s) always returns the same set. However, because the computation of a reduced set5 of enabled transitions can be costly, we opted for its memoization using mutexes. This is an implementation choice but a pure lock-free version remains possible. All the approaches proposed here have been implemented in Spot [START_REF] Duret-Lutz | Spot 2.0 -a framework for LTL and ω-automata manipulation[END_REF]. For a given model the corresponding Kripke structure is generated on-the-fly using DiVinE 2.4 patched by the LTSmin team. 6Reduction rates. Figure 5 gives the mean of the reduction rates for the benchmark. It appears that the reduction rate of each algorithm is insensitive to the thread number. For M 1 , all algorithms tend to have a similar reduction rate even if laarman (live and safe) is slightly worse than the others (both for liveness and safety cases). For liveness and models M 2 , it appears that ws-pr19-live significantly degrades the reduction rate. This is due to the pessimistic approach imposed by the lack of information from the DFS stack. This effect is minored for the safety case because expansions are limited to the bottom SCCs and by our strategy that minimizes the number of expansions in such SCCs. Time analysis. Tables 1 and2 describe the measure for the two categories of model and all the algorithms running with 1 to 12 threads. For safety, lw14-safe and ws-pr19-safe have comparable running times. Since ws-pr19-safe has a smaller reduction rate than lw14-safe, the work-stealing mechanism implemented in ws-pr19-safe shows its efficiency. Nonetheless, scc-pr19-safe and dfs-pr19-safe perform better. However, the complex data structure of scc-pr19-safe impacts negatively its running time. For liveness, lw14-live performs better than ws-pr19-live. dfs-pr19-live performs better than the two others regardless the category of models. Finally, we can notice that the work-stealing mechanism of ws-pr19-live particularly improves the speedup for models M 2 . The Figure 6 displays the speedup curves for both liveness and safety and M 2 . For models M 1 , the speedup of all algorithms are comparable.

Conclusion

To our knowledge, only the work of Laarman and al. proposes provisos designed for parallel model checking. Nonetheless, in sequential settings and for liveness properties, Duret-Lutz et al. [START_REF] Duret-Lutz | Heuristics for checking liveness properties with partial order reductions[END_REF] empirically shown that variations on the traditional proviso could improve performances. In this paper, we demonstrate that the application of the suggested provisos (in particular dfs-pr19-live and dfs-pr19-safe) can also benefit to the parallel emptiness check based on a state-based DFS. During this investigation, we also proposed a new proviso also based on destination expansion but dedicated to safety properties.

However, the best existing parallel emptiness checks are based on an SCC computation. For the best of them (bp16 [START_REF] Bloemen | Multi-core scc-based ltl model checking[END_REF]), no existing provisos can be directly applied since it is based on a work-stealing mechanism breaking the DFS postorder. In this paper, we proposed new provisos for this parallel emptiness check (for both liveness and safety properties). Moreover, we also presented a dedicated proviso for safety properties for Renault et al. [START_REF] Renault | Variations on parallel explicit model checking for generalized Büchi automata[END_REF]. Figure 1 summarizes the compatibility of the different provisos with respect to existing emptiness checks.

One of the challenging problems in parallelizing explicit state model checking is the model checking of stutter-free LTL properties on distributed systems. In this paper we propose, for the first time, several algorithms (that can be directly integrated into the best known emptiness checks) to tackle this problem. All provisos presented and evaluated in this paper achieve comparable speedups. However, the reduction rate of ws-pr19-live for models with long cycles and a small number of large SCCs is significantly degraded compared to the other proposed algorithms. An open question remains: can we develop a liveness proviso for bp16 that preserves a good reduction rate for any category of models?

Fig. 1 .

 1 Fig. 1. Contributions of this paper are detailed in green. Red plain boxes correspond to sequential emptiness checks and blue plain boxes represent parallel emptiness checks. Dashed boxes are provisos. A proviso box is covered by a emptiness check box if the two are compatible. An edge links one box to another if the second one reuses ideas from the first one. Bullets tagged l represent liveness provisos and s the safety ones.

Algorithm 2 :5 6 dfsp ← dfsp ∪ {v} 7 nextFig

 267 Fig. 3.Example where a useless expansion occurs in bottom-SCC for Algorithm 2. The two starred nodes will be expanded.

  Fig. 4. Two threads cooperatively discovering a cycle. Dashed edges represent paths from the initial state while plain edges represent currently processed edges.

9 12 while next = ∅ do 13 w

 1213 while v ∈ (S(v) \ done) do 10 wipp ← wipp ∪ {v } 11 next ← v ∈ expanded ? post(v ) : reduced(v ) ← randomlyPick(next)14 if w ∈ dead then continue 15 else if ∃w ∈ Rp : w ∈ S(w ) then 16 wipp ← wipp \ {v } 17 ws-pr19-livep(w)

Fig. 5 .

 5 Fig.5. Mean Reduction rates (in percent) on the whole benchmark, depicted for liveness and safety and for the two categories M1 and M2. The x-axis represents the number of threads when the y-axis the mean of the reduction rates.

Fig. 6 .

 6 Fig. 6. Speedup on models M2

  the path is a cycle. Moreover, when all the states v 1 , . . . v n are distinct states, then the cycle is said elementary.A non-empty set C ⊆ V is a Strongly Connected Component (SCC) iff any two different states v, v ∈ C are connected by a path, and C is maximal w.r.t. inclusion. If C is not maximal we call it a partial SCC.

  v) is a TSCC without exp. st.

	12	if ¬isTerm then
	13	expanded ← expanded ∪ {v}
	14	for v ∈ mixp(next) do

15 if v ∈ dead then 16 isTerm ← ⊥ 17 else if v ∈ visitedp then 18 t ← scc-pr19-safe(v ) 19 isTerm ← isTerm ∧ t 20 else 21 while v .nump < rootsp.top().nump do 22 r ← rootsp.pop()

Table 1 .

 1 States in 10 6 , times in seconds and speedup for liveness provisos

				lw14-live			dfs-pr19-live	ws-pr19-live
				States Time Sp.	States Time Sp. States Time(s)	Sp.
			1 th.	412.3 3 755	-	410.1 3 732	-	411.5	4 651	-
		M1	2 th. 4 th. 8 th.	413.9 1 983 1.89 415.2 1 136 3.30 414.6 805 4.66	410.1 1 960 1.90 411.5 410.1 1 124 3.32 411.5 410.1 773 4.83 411.5	2 505 1 429 1 021	1.86 3.25 4.55
			12 th. 414.6		691 5.43	410.1	678 5.50 411.5	829	5.60
			1 th.	202.0 1 372	-	181.5 1 218	-	256.3	2 761	-
		M2	2 th. 4 th. 8 th.	199.3 197.3 195.1		718 1.91 391 3.50 246 5.56	182.2 182.2 182.3	632 1.93 256.2 343 3.55 256.0 222 5.49 255.9	1 392 721 466	1.98 3.83 5.93
			12 th. 193.9		186 7.34	182.2	165 7.36 255.7	359	7.69
			lw14-safe			dfs-pr19-safe	scc-pr19-safe	ws-pr19-safe
		State Time	Sp. State Time	Sp. State Time	Sp. State Time	Sp.
		1 th. 412.3 5 124	-	410.1 3 734	-	410.1 4 179	-	410.1 5 041	-
	M1	2 th. 413.9 2 709 4 th. 414.6 1 527 8 th. 414.5 1 067	1.84 410.1 1 961 3.38 410.1 1 124 4.87 410.1 803	1.90 410.4 2 235 3.32 410.3 1 372 4.65 410.7 870	1.87 410.1 2 744 3.04 410.1 1 493 4.80 410.1 1 034	1.84 3.38 4.87
		12 th. 414.7	809	6.23 410.1	641	5.82 410.5	784	5.33 410.1	809	6.23
		1 th. 202.0 1 372	-	180.2 1 214	-	179.1 1 380	-	179.1 1 935	-
	M2	2 th. 199.6 4 th. 197.2 8 th. 195.1	724 391 263	1.90 180.5 3.50 180.7 5.21 180.8	633 339 214	1.92 179.2 3.58 179.2 5.67 179.5	713 336 257	1.93 179.1 4.10 179.1 5.37 179.2	997 543 362	1.94 3.56 5.35
		12 th. 194.0	187	7.32 180.7	165	7.32 179.5	205	6.72 179.2	296	6.52

Table 2 .

 2 States in 10 6 , times in seconds and speedup for safety provisos

See Peled[START_REF] Peled | Combining partial order reductions with on-the-fly model-checking[END_REF] for a survey of POR reductions with LTL.

All instructions (excepted recursive calls) are considered to be atomic.

For a description of our setup, including selected models, detailed results and code, see http://www.lrde.epita.fr/ ~renault/benchs/ICFEM-2019/results.html

Notice that we only consider the blue DFS (without lines 33-37). When implementing an emptiness check the ignored lines could trigger complementary expansions. Thus the reported values here can be interpreted as the optimal bound (time, reduction, ...) for this

algorithm.[START_REF] Bošnaȃźki | Partial-order reduction for general state exploring algorithms[END_REF] Our implementation uses persistent sets since a special attention must be paid when combining ample sets with on-the-fly exploration[START_REF] Stephen | What's wrong with on-the-fly partial order reduction[END_REF].

See http://fmt.cs.utwente.nl/tools/ltsmin/#divine for more details.


Ying Siu Liang

Damien Pellier

Humbert Fiorino

Sylvie Pesty

End-User Programming of Low-and High-Level Actions for Robotic Task Planning

Programming robots for general purpose applications is extremely challenging due to the great diversity of end-user tasks ranging from manufacturing environments to personal homes. Recent work has focused on enabling endusers to program robots using Programming by Demonstration. However, teaching robots new actions from scratch that can be reused for unseen tasks remains a difficult challenge and is generally left up to robotic experts. We propose iRoPro, an interactive Robot Programming framework that allows endusers to teach robots new actions from scratch and reuse them with a task planner. In this work we provide a system implementation on a two-armed Baxter robot that (i) allows simultaneous teaching of low-and high-level actions by demonstration, (ii) includes a user interface for action creation with condition inference and modification, and (iii) allows creating and solving previously unseen problems using a task planner for the robot to execute in real-time. We evaluate the generalisation power of the system on six benchmark tasks and show how taught actions can be easily reused for complex tasks. We further demonstrate its usability with a user study (N=21), where users completed eight tasks to teach the robot new actions that are reused with a task planner. The study demonstrates that users with any programming level and educational background can easily learn and use the system.

I. INTRODUCTION

Despite the ongoing advances in Robotics and A.I., it is extremely challenging to pre-program robots for specific enduser applications. Instead of developing robots for domainspecific tasks, a more flexible solution is to have robots learn new actions directly from end-users and let them customise the robot for their specific application. Programming by Demonstration (PbD) [START_REF] Billard | Robot programming by demonstration[END_REF] has been used to allow endusers to teach robots actions in an intuitive way by taking demonstrations as input and inferring a policy for the task. However, PbD solutions usually require users to teach robots an action sequence to achieve a certain goal. If the goal changes, the user has to teach the robot a new sequence.

Consider the Tower of Hanoi, a puzzle consisting of three pegs and a number of differently-sized disks, stacked on one peg in descending order, with the largest peg at the bottom. The goal is to move the entire stack from one peg to another, by moving one disk at a time, and only to a larger disk or an empty peg. The solution is different depending on the given number of disks. If we want to teach a robot to solve this problem, it would be infeasible to demonstrate the solution each time. A more efficient approach would be to teach the robot the primitive action of moving a disk, associate rules or conditions to this action (e.g., smaller disks can only be Y.S. Liang, D. Pellier, H. Fiorino, and S. Pesty are with the Univ. Grenoble Alpes, LIG, F-38000 Grenoble, France {liangyi, pellierd, fiorinoh, pestys}@univ-grenoble-alpes.fr placed on top of larger ones), and have the robot generate an optimal solution using a task planner [START_REF] Ghallab | Automated planning: Theory & Practice[END_REF].

Our research argues for teaching robots primitive actions, instead of entire action sequences, and delegating the logical reasoning process of finding a solution to task planners. Even though task planners are generally used by domainexperts, we have previously shown that users with little to no programming experience can easily learn and use symbolic planning languages [START_REF] Liang | Evaluation of a Robot Programming Framework for Non-Experts using Symbolic Planning Representations[END_REF]. Based on the obtained results, this work presents iRoPro, an interactive Robot Programming system (Sec. III). It is a working end-to-end system that allows efficient programming of both how an action is performed (low-level) and when it can be applied (highlevel), while generalising both aspects to previously unseen scenarios. We implement the system on a Baxter robot and developed a graphical interface that allows users to teach new actions by kinesthetic demonstration, modify their conditions and define previously unseen problems to solve with a task planner (Sec. IV). We demonstrate our system's capability to generalise primitive actions on six benchmark tasks that are programmed and executed on the robot (Sec. V). We empirically investigate the system's usability and validate its intuitiveness through a study with users of different educational backgrounds and programming levels (Sec. VI). To better understand user teaching strategies, we split participants into two control groups, with and without automatic condition inference, and showed that users in both groups can easily learn and use the system. Finally, we discuss limitations and possible extensions to further increase the system's generalisability (Sec. VII).

II. RELATED WORK

Our work relates to several topics explored in previous research. End-user robot programming has been addressed previously for industrial robots to be programmed by nonrobotics domain experts, where users specify and modify existing plans for robots to adapt to new scenarios [START_REF] Stenmark | Simplified programming of re-usable skills on a safe industrial robot: Prototype and evaluation[END_REF]. In our work we argue for the use of task planners to automatically generate plans for new scenarios.

Previous work has addressed knowledge engineering tools for constructing planning domains but usually require PDDL experts or common knowledge in software engineering (e.g., itSIMPLE [START_REF] Vaquero | itSIMPLE: towards an integrated design system for real planning applications[END_REF]). There has been previous work on integrating task planning with robotic systems [START_REF] Cashmore | ROSPlan: Planning in the Robot Operating System[END_REF] and learning preconditions and effects of actions to be used in planning [START_REF] Konidaris | From skills to symbols: Learning symbolic representations for abstract high-level planning[END_REF]. However, the robot is usually provided with a fixed set of low-level motor skills. We do not provide the robot with any predefined actions but allow users to teach both low-and high-level actions from scratch.

Programming by demonstration [START_REF] Billard | Robot programming by demonstration[END_REF] has been commonly applied to allow end-users to teach robots new actions by demonstration. Recent work has focused on mobile and industrial manipulators [START_REF] Stenmark | Simplified programming of re-usable skills on a safe industrial robot: Prototype and evaluation[END_REF] and learning from single demonstrations [START_REF] Alexandrova | Robot programming by demonstration with interactive action visualizations[END_REF]. Alexandrova et al. created an end-user programming framework with an interactive action visualisation allowing the user to teach new actions from single demonstrations but do not reuse them with a task planner.

Most closely related to our approach is the work by Abdo et al. [START_REF] Abdo | Learning manipulation actions from a few demonstrations[END_REF] where manipulation actions are learned from kinesthetic demonstrations and reused with task planners. However, the approach requires 5-10 demonstrations to learn action conditions which becomes tedious and impractical if several actions need to be taught. Our work argues for having the user act as the expert by letting them correct inferred action conditions, thus allowing a new action to be learned from a single demonstration. We further provide a graphical interface that allows users to create new actions and previously unseen problems that can be solved with task planners.

III. APPROACH

Our approach aims at providing end-users with an intuitive way of teaching robots new actions that can be reused with a task planner to solve more complex tasks. Given a single demonstration, the robot should learn both how (Sec. III-A) and when (Sec. III-B) an action should be applied. To accelerate the programming process, action conditions are directly inferred from a single demonstration (Sec. III-C). The action generalisation is performed on both low-and high-level representations (Sec. III-D), allowing it to be reused with a task planner (Sec. III-E). We will describe our approach in the following sections.

A. Low-level Action Representation

We represent low-level actions as proposed in previous work using keyframe-based PbD [START_REF] Alexandrova | Robot programming by demonstration with interactive action visualizations[END_REF], where the action is represented as a sparse sequence of gripper states (open/close) and end-effector poses relative to perceived objects or to the robot's coordinate frame. During the demonstration phase the user guides the robot arm using kinesthetic manipulation and saves poses that they find relevant for the action. For example, the pick-and-place action of an object to a marked position could be represented as poses relative to the object (for the pick action), poses relative to the target position (for the place action), and corresponding open/close gripper states. Action executions are performed by first detecting the landmarks in the environment, calculating the end-effector poses relative to the observed landmarks, and interpolating between the poses.

While these actions can be learned from multiple demonstrations [START_REF] Niekum | Learning and generalization of complex tasks from unstructured demonstrations[END_REF], we take the approach that only requires a single demonstration by heuristically assigning poses and letting the user correct them if needed [START_REF] Alexandrova | Robot programming by demonstration with interactive action visualizations[END_REF]. Thus, the first demonstrated action is already an executable action. The user can teach multiple manipulation actions and discriminate between them by associating different conditions that specify when the robot should use them (e.g., actions using claw or suction grippers). These conditions are discussed next in Sec. III-B.

B. High-level Action Representation

We represent high-level actions similar to previous work on task planning [START_REF] Ghallab | Automated planning: Theory & Practice[END_REF], where an action is represented as a tuple a = (param(a), pre(a), eff(a)), whose elements are:

• param(a): set of parameters that a applies to • pre(a): set of predicates that must be true to apply a • eff(a) : set of predicates that are false after applying a • eff(a) + : set of predicates that are true after applying a where eff(a) = eff(a) [ eff(a) + . Action parameters are world instances that the robot interacts with and are associated with a type. For example, in iRoPro, we implemented a type hierarchy, consisting of a general type ELEMENT, divided into POSITION and OBJECT, which further divides into BASE, CUBE, and ROOF (Fig. 1).

Predicates are used to describe object states and relations between them and are defined in first-order logic. In our graphical interface, predicates are translated from first-order logic ('on(obj, A)') to English statements ('obj is on A').

In iRoPro, we implemented predicates that are commonly used in task planning domains as well as two additional ones to describe object properties:

• ELEMENT is clear: an element has nothing on top of it • OBJECT is on ELEMENT: an object is on an element • OBJECT is stackable on ELEMENT: an object can be placed on an element • OBJECT is flat: an object has a flat top • OBJECT is thin: an object is thin We assume that CUBE and BASE objects are flat, while CUBE and ROOF objects are thin enough for the robot to grasp. The set of inferred types and predicates could be extended for more complex tasks (e.g., object colour or orientation [START_REF] Li | Learning object orientation constraints and guiding constraints for narrow passages from one demonstration[END_REF]).

C. Action Inference from Demonstration

Instead of manually defining action parameters, preconditions, and effects, we accelerate the programming process by inferring them from the observed sensor data during the teaching phase. Object types are inferred based on their detected bounding boxes (see Sec. IV-A). Object positions are determined by the proximity of the object to given positions. If the nearest position p to the object o is within a certain threshold d, then the predicates 'o is on p' and 'p is not clear' are added to the detected world state.

To infer action conditions, the robot perceives the initial world state before and after the kinesthetic action demonstration as seen in similar work for learning object manipulation tasks [START_REF] Ahmadzadeh | Learning symbolic representations of actions from human demonstrations[END_REF]. Let O 1 = { 1 , 2 , ...} be the set of predicates observed before the action demonstration and

O 2 = { 1 , 2 , .
..} after. The action inference is the heuristic deduction of predicates that have changed between O 1 and

O 2 , i.e., pre(a) = (O 1 O 1 \ O 2 ) = { i | i 2 O 1 ^ i / 2 O 2 }, eff(a) = (O 2 O 1 \ O 2 ) = { i | i / 2 O 1 ^ i 2 O 2 },
where eff(a) includes positive and negative effects (Fig. 3).

A predicate has variables var( ) = {v 1 , v 2 , . . . }, where each v i has a type. Therefore, action parameters are the set of variables that appear in either preconditions or effects, i.e.,

param(a) = {v i | 9 2 pre(a) s.t. v i 2 var( ) _ 9 2 eff(a) s.t. v i 2 var( )}.
Note that conditions could be learned from multiple demonstrations [START_REF] Abdo | Learning manipulation actions from a few demonstrations[END_REF], [START_REF] Konidaris | From skills to symbols: Learning symbolic representations for abstract high-level planning[END_REF]. Our work argues for accelerating the teaching phase by learning from a single demonstration and letting the user act as the expert to correct wrongly inferred conditions.

D. Action Generalisation

The low-level representation (Sec. III-A) generalises motion trajectories by re-calculating poses based on detected landmarks from the demonstrated to the new environment. The high-level representation (Sec. III-B) specifies when an action can be applied, therefore allows taught low-level motion trajectories to be reused for other objects (e.g., use suction grip for all objects, regardless of their dimension) or to be restricted for certain types (e.g., only BASE objects). By combining these two representation levels, taught actions can be generalised for more complex environments and the user can customise them for their specific use case.

Before (O1) obj is on A

A is not clear obj is not on B B is clear C is clear obj is clear obj is flat ____ ____ ____ A B C After (O2) obj is on B B is not clear obj is not on A A is clear C is clear obj is clear obj is flat ____ ____ ____ A B C _______________ A B Goal Preconditions obj is on A A is not clear obj is not on B B is clear Effects obj is on B B is not clear obj is not on A A is

E. Task Planning

Task planners are used to generate solutions, or action sequences, to solve complex problems. Given a description of a planning domain, i.e., object types, actions with preconditions and effects, we can define a planning problem with an initial state and a desired goal state. The planner generates an optimal action sequence, or plan, which guarantees the transition from initial state to the goal state. PDDL [START_REF] Mcdermott | PDDL-the planning domain definition language[END_REF] is often used as a standard encoding language for planning problems. A move action as shown in Fig. 3 is defined as follows:

(:action move :parameters (?obj -object ?A -position ?B -position) :precondition (and (on ?obj ?A)(clear ?B) not(on ?obj ?B) not(clear ?A)) :effect (and (on ?obj ?B) (clear ?A) not(on ?obj ?A) not(clear ?B))

A planning problem consists of an initial state and a goal state and can be solved using existing actions in the domain. For example, the problem of swapping two objects obj1, obj2 on A and B respectively with C unoccupied, can be defined as:

(:objects obj1 obj2 -object A B C -position) (:init (and (on obj1 A) (on obj2 B) (clear C)) (:goal (and (on obj1 B) (on obj2 A)))

The planner would generate the following action sequence:

1. move(obj1, A, C) 2. move(obj2, B, A) 3. move(obj1, C, B)

IV. SYSTEM

A. Platform & Implementation Details

We implemented our system on a Baxter robot with two arms (one claw and one suction gripper), both with 7-DoF and a load capacity of 2.2kg. For the object perception we mounted a Kinect Xbox 360 depth camera on the robot. We developed a user interface as a web application that can be accessed via a browser on a PC, tablet or smartphone. The source code for iRoPro is developed in ROS [START_REF] Quigley | ROS: an open-source Robot Operating System[END_REF] and available online 1 . The low-level action is learned using the open-source system Rapid PbD 2 . The integration of the task planner is implemented using the ROS package PDDL planner 3 .

In our implementation, landmarks are either predefined table positions or objects that are detected from Kinect point cloud clusters using an open-source tabletop segmentation library 4 . An object obj = (x, y, z, width, length, height) is represented by its detected location and bounding box, which are used to infer its type and related predicates (Sec. III-C) The user creates a complete PDDL domain via the GUI by teaching new actions and problems that can be solved with the integrated task planner. 5

B. Interactive Robot Programming

The user interacts with the GUI (Fig. 4) to visualise the robot and the detected objects, create new actions, run the kinesthetic teaching by demonstration, modify inferred types or predicates, create and solve new problems with the task planner. The interactive robot programming cycle consists of creating and modifying actions and problems. a) Actions: New actions are taught by kinesthetically moving the robot's arms, where both low-level and high-level actions are learned and generalised. The low-level action is learned by keyframe-based demonstration (Sec. III-A). To verify the taught action, the user can have the robot re-execute it immediately. The high-level action is inferred automatically by capturing the world state before and after the action demonstration (as described in Sec. III-C). The user can modify the action properties if the inference was not correct. To teach more actions, the user can either create a new one or copy a previously taught action and modify it.

b) Problems: New planning problems can be created if at least one action exists. To create a problem, the robot first detects the existing landmarks and infers their types and initial states. The user can modify them if the inference was not correct. Then, the user enters predicates that describe 1 https://github.com/ysl208/iRoPro/tree/cond 2 https://github.com/jstnhuang/rapid_pbd 3 http://docs.ros.org/indigo/api/pddl_planner 4 https://github.com/jstnhuang/surface_perception 5 Video can be viewed at https://youtu.be/YCDrC0UFX38 the goal states to achieve. The complete planning domain and problem are translated into PDDL and sent to the Fast-Forward planner [START_REF] Hoffmann | The FF planning system: Fast plan generation through heuristic search[END_REF]. If a solution is found that reaches the goal, it is displayed on the GUI for the user to verify and execute on the robot. If no solution is found or if the generated plan is wrong, the user can open a debug menu which summarises the entire planning domain with hints described in natural language to the problem (e.g., 'make sure the action effects can achieve the goal states'). In our user study (Sec. VI) we found that this helped users understand how the system worked and why the generated plan was wrong. Once the user modified actions, initial or goal states, they can relaunch the planner to see if a correct plan is generated. To solve new tasks, the user can create a new problem or modify existing ones by redetecting the objects.

C. Plan Execution

The generated plan is a sequence of actions with parameters that correspond to detected objects. For each action, the sequence of end-effector poses are calculated relative to the landmarks that the action is being applied to (Sec. III-A). To accelerate the execution, we only detect the landmarks once at the start and save their new positions in a mental model. After each action execution, the user can confirm that it executed correctly and the mental model is updated with the latest positions of the changed landmarks. The mental model is also used as a workaround for our limited perception system for problems with stacked objects in their initial states (Sec. VII).

V. SYSTEM EVALUATION

We evaluate our system's generalisability on six benchmark tasks (Table I) and show how taught primitive actions can be reused for complex tasks. The tasks involved manipulating different object types on four marked positions with both claw and suction grippers. We take the Blocksworld domain [START_REF] Slaney | Blocks world revisited[END_REF] for building and rebuilding stacked objects (Tasks 1-4) and an elaborate version of the Tower of Hanoi problem with different object types to build a 'house' (Tasks 5&6). Instead of disks, we decided to use different object types (ROOF, CUBE, BASE), where BASE corresponds to the largest disk, followed by CUBE and ROOF. The rules for stacking different objects still apply (e.g., BASE cannot be stacked on top of ROOF or CUBE). However, to demonstrate the generalisation of actions to diverse tasks, additional constraints are added as objects cannot be all manipulated in the same way. The order of the tasks was given with increasing complexity, requiring the user to modify existing actions or teach new actions from scratch.

A. Protocol

The tasks were programmed by one of the authors, with the most efficient teaching strategy of minimising the number of actions created and generalising them by changing the action properties (as described in Sec. III-D). Depending on the given task and involved objects, the experimenter decided what manipulation action needed to be taught. Only one planning problem was created and reused for all tasks by redetecting the objects in the initial state and changing the goal state. When the generated plan was incorrect, the debug menu on the GUI was used to determine the changes to be made to generalise the actions. A task was considered completed when the generated plan was correct and the robot successfully executed it. As the mental model saved the latest object positions after an action execution, Tasks 3 and 6 were continued from the preceding tasks and did not require redetecting the initial states.

B. Results

We programmed three manipulation actions for the six benchmark tasks, which involved demonstrating pick-andplace actions with claw and suction grippers from the top and from the side. Actions were generalised by changing parameter types (e.g., from CUBE or POSITION to ELE-MENT) or adding preconditions or effects which were not inferred automatically. For pick-and-place actions from the top, 'obj is clear' was added as a precondition (Task 1-3), while it was not included when picking an object from the TABLE I: Benchmark tasks for the system evaluation. Three different pick-and-place actions were programmed. side to allow moving a pile of objects (Task 4). For actions involving the claw gripper, the precondition 'obj is thin' was added so that the robot would only use it on ROOF and CUBE objects, similarly 'is flat' for the suction gripper (Task 5&6). The 'is stackable' condition was used for the Tower of Hanoi as an equivalent to the rule 'larger objects cannot be placed on top of smaller ones'. Due to the noisy sensing and control of the Baxter robot, action executions failed occasionally, even though the generated plan was correct. Overall, the robot was able to generate plans for all tasks and executed them at least twice (Fig. 5). While the experimental scope was limited and set in a controlled environment, it still demonstrates iRoPro's expressivity. With minimal end-user programming effort, manipulation actions can be taught from scratch and reused for a diverse range of tasks, even beyond the six benchmark tasks.

VI. USER EVALUATION

The second part of the evaluation was conducted using THEDRE [START_REF] Mandran | THEDRE: a Traceable Process for High Quality in Human Centred Computer Science Research[END_REF], a human experiment design method that combines qualitative and quantitative approaches to continuously improve and evaluate the developed system from the experimental ground. The aim was to evaluate our approach with real end-users and we were also interested in the user's programming strategy for using the system. We split participants into two control groups, with and without condition inference (Sec. III-C) and evaluated user performance in terms of programming times for completing a set of benchmark tasks. We set the following hypotheses for our experiments:

H1 Action creation: users can teach new low-and highlevel actions by demonstration H2 Problem solving: users can solve new problems by defining the goal states and executing the plan on Baxter H3 Autonomous system navigation: users understand the system and can navigate and troubleshoot on their own H4 Condition inference (CI) -Group 1 vs 2: users without CI will understand the system better H5 Pre-study test (PT): users that score higher in the PT have shorter programming times

A. Participants

The study was conducted with 21 participants (10M, 11F) in the range of 18-39 years (M=24.67, SD=6.1). We recruited participants with different educational background and programming levels: 6 'CS' (either completed a degree in computer science or were currently pursuing one), 7 'non-CS' (have previously taken a programming course before), and 8 'no experience' (only had experience with office productivity software). Furthermore, 3 participants (in 'CS') have programmed a robot before, out of which 1 had intermediate experience with symbolic planning languages while the remaining participants had no experience in either. One participant in the category 'non-CS' failed to complete the majority of tasks and was excluded from the result evaluation. The two control groups included equal number of participants in all three categories.

B. Protocol

Users were first given a brief introduction to task planning concepts, the Baxter robot and the experimental set up (Fig. 1). They were then asked to complete a pre-study test to capture the participant's understanding of the presented concepts. Users were given 8 tasks to complete, where the first two were practice tasks to introduce them to the system (Table II). The tasks were designed to address different aspects to familiarise them with the system: create new actions (Task 6), modify parameter types (Tasks 4&7), modify action conditions (Tasks 3,5,8). For each task they needed to create a new problem, define the goal states, and launch the planner to generate an action sequence. When the generated plan was correct, they were executed on the robot. Otherwise, the user had to modify the existing input until the plan was correctly generated. Tasks 6-8 were similar to the previous tasks (1-5) but use both robot grippers.

C. Metrics

We captured the following data during the experiments: 1) Qualitative data: video recording of the experiment, observations during the experimental protocol. 2) Quantitative data: task duration and UI activity log, pre-study test, post-study survey. The pre-study test included 7 questions related to their understanding of the concepts presented at the start of the experiment, e.g., syntax ('If move(CUBE) describes a move action, tick all statements that are true.'), logical reasoning ('Which two conditions can never be true at the same time?'), and other concepts ('Tick all predicates that are required as preconditions for the given action'). The questions were multiple choice and the highest achievable score was 7.

In the post-study survey we used the System Usability Scale (SUS) [START_REF] Brooke | SUS: a retrospective[END_REF] where participants had to give a rating on a 5-Point Likert scale ranging from 'Strongly agree' to 'Strongly disagree'. It enabled us to measure the perceived usability of the system with a small sample of users. As a benchmark, we compare overall responses to our previous user study [START_REF] Liang | Evaluation of a Robot Programming Framework for Non-Experts using Symbolic Planning Representations[END_REF], where users were simulated a similar robot programming experience using the Wizard-of-Oz technique but had no direct interaction with a working system. Finally, participants were asked which aspects they found most useful, most difficult, and which they liked the best and the least.

D. Results

20 participants completed all tasks, while one 'non-CS' user failed to complete the majority of tasks and did not seem to understand the presented concepts. This participant was excluded in the results presented below (Table III):

H1)-H3) User performance: Users took between 22-60 minutes to complete the main tasks [START_REF] Liang | Evaluation of a Robot Programming Framework for Non-Experts using Symbolic Planning Representations[END_REF][START_REF] Stenmark | Simplified programming of re-usable skills on a safe industrial robot: Prototype and evaluation[END_REF][START_REF] Vaquero | itSIMPLE: towards an integrated design system for real planning applications[END_REF][START_REF] Cashmore | ROSPlan: Planning in the Robot Operating System[END_REF][START_REF] Konidaris | From skills to symbols: Learning symbolic representations for abstract high-level planning[END_REF][START_REF] Alexandrova | Robot programming by demonstration with interactive action visualizations[END_REF], with an average of 41.2 minutes. 'non-CS' users completed the tasks the fastest, followed by users with no programming experience. 'CS' users took on average longer as they were often interested in testing the system's functionalities that were beyond the given tasks.

Users initially had problems with different concepts that were presented at the start of the study, in particular they confused action parameters, preconditions and goal states. For example, in Task 3, 6 (or 30%) users tried to add intermediate action steps to achieve the goal state, instead of simply letting the planner generate the solution. In Task 4, 14 (or 70%) wanted to create a new action, even though they could reuse the existing action by modifying the parameter types. However, by Task 6, all users were able to use the system autonomously to create new actions and problems and navigated the system with little to no guidance. By the end of the experiment, users programmed two manipulation actions (one for each gripper) that were reused to complete all 8 benchmark tasks.

H4) Condition inference (CI):

We noticed a discrepancy in the programming strategies between the two control groups (Group 1 with CI vs. Group 2 without CI). Participants in Group 1 had the tendency to leave the inferred conditions unmodified without adding conditions that would improve the action's generalisability to different use cases. As participants in Group 2 had to add action conditions manually, they considered all predicates they deemed necessary for the action and added additional ones that were required for later tasks. Thus, Group 2 took on average longer to complete tasks where a new action had to be created (Tasks 1&6), but was faster than Group 1 for subsequent tasks, where conditions had to be modified (Tasks 3,5,7). Overall both groups had similar completion times for all tasks.

H5) Pre-study test: As expected, participants who demonstrated a better understanding of the introduced concepts in the pre-study test completed the main tasks (Tasks 3-8) faster on average (p-value< 0.05). Users scored between 4.3-6.93 out of 7 points. 'non-CS' users scored above average points and completed the fastest. As an outlier we observed that the fastest participant scored only 4.7, but easily learned how to use the system and completed the tasks in 22 minutes. Even though Group 1 performed slightly better in the pre-study test than Group 2, both completion times were on average similar.

System usability and learnability: There are several ways to interpret the System Usability Scale (SUS) scores [START_REF] Brooke | SUS: a retrospective[END_REF] obtained from the post-study survey. Using Bangor et al.'s categories [START_REF] Bangor | An empirical evaluation of the system usability scale[END_REF], 14 (70%) users ranked iRoPro as 'acceptable', 6 (30%) rated it 'marginally acceptable', and no one ranked it 'not acceptable'. Correlating this with the Net Promoter Score, this corresponds to 10 (50%) participants being 'promoters' (most likely to recommend the system), 5 (25%) 'passive', and 5 (25%) 'detractors' (likely to discourage). Overall, iRoPro was rated with a good system usability and learnability.

Overall user experience: We compare responses to our previous user study (N=11) [START_REF] Liang | Evaluation of a Robot Programming Framework for Non-Experts using Symbolic Planning Representations[END_REF], where users had no direct interaction with the robot programming system as it was simulated using the Wizard-of-Oz technique. The main differences were noted regarding difficulties encountered during the experiment (Fig. 6): In our previous study we had 11 (or 100%) agree that they encountered no difficulties, while this time only 7 (or 35%) of our users stated the same. However, all of our users claimed to have a good understanding of the action representation and how the robot learned new actions from their demonstrations, while an average of 2 (18%) disagreed in [START_REF] Liang | Evaluation of a Robot Programming Framework for Non-Experts using Symbolic Planning Representations[END_REF]. Both differences can be explained by the fact that in this study, users had to use an end-to-end system to program the robot, while in our previous work users had no direct interaction with a working system. Even though our users encountered more difficulties, they got a better understanding of the functionalities due to getting hands-on experience. This also correlates with negative responses in our survey to the question if 'no programming experience was required' where 13/20 (65%) agreed and 4 disagreed. Overall, our user study received positive responses similar to the previous study. 9 (45%) users stated 'generate solutions to defined goals automatically' as the most useful feature, followed by 'robot learns action from my demonstration' (4 or 20%) -two main aspects of our approach. 4 (20%) stated the most difficult part as 'finding out why Baxter didn't solve a problem correctly', similarly 8 (40%) stated difficulties related to 'understanding predicates and defining conditions'. 11 (55%) disliked 'assigning action conditions' the most, while the rest stated different aspects. A common feedback was 'it takes time to understand how the system works at the start'. The most liked parts were 'executing the generated plan' (8 or 40%) and 'demonstrating an action on Baxter' (7 or 35%).

VII. DISCUSSIONS

In our evaluation scenarios we could have programmed more complicated manipulation actions such as turning or pushing for packaging tasks (as done previously in [START_REF] Liang | Simultaneous End-User Programming of Goals and Actions for Robotic Shelf Organization[END_REF]). We decided to stick to simple pick-and-place manipulation actions, as our main focus was to evaluate iRoPro's usability with end-users. Both system and user evaluations demonstrated that the proposed robot programming process for manipulation tasks can be learned easily by users with or without programming experience.

The workaround based on mental models of the environment only works if the environment is static and no external entity interferes with the world. The next step would be to move from controlled environments to more dynamic ones, whereby all relevant aspects of the environment need to be fully perceivable by the system. An improved perception system would also allow tracking and verifying action executions in case of failures in more complex environments.

Due to the Baxter robot's different grippers, we did not program actions that use both arms simultaneously (e.g., for carrying a tray). A possible extension would be to include a better motion and task planning system to allow this while also considering self-collision avoidance. Furthermore, we did not program human-robot collaborative tasks, such as human-robot hand-over tasks. To allow this, more complex planning domains and better multi-modal communication would need to be implemented.

VIII. CONCLUSION

In this work we presented iRoPro, an interactive Robot Programming system that allows simultaneous teaching of low-and high-level representations of actions by demonstration. The robot reuses the actions with a task planner to generate solutions to previously unseen tasks that are more complex than the demonstrated action. The approach was implemented on a Baxter robot and we showed its generalisability on six benchmark tasks by teaching a minimal set of primitive actions that were reused for all tasks. We further demonstrated its usability with a user study (20 successful results, 1 unsuccessful result) where participants with diverse educational backgrounds and programming levels learned how to use the system in less than an hour. Both user performance and feedback confirmed iRoPro's usability, with the majority ranking it as 'acceptable' and half being promoters. Overall, we demonstrated that our approach allows users with any programming level to efficiently teach robots new actions that can be reused for complex manipulation tasks.

Future work will focus on exploring more challenging domains to extend the work to other platforms by including a wider range of predicates and probabilistic techniques to improve the condition inference. As we focused on controlled environments, further studies will involve more complex environments with factory workers who may ultimately use this technology.

Fig. 1 :

 1 Fig. 1: Users programmed the Baxter robot via a graphical interface to manipulate objects (shown with their type hierarchies) in the task domain.

Fig. 2 :

 2 Fig.2: Overview of iRoPro to teach low-and high-level actions: the user interacts with the GUI to run the demonstration, modify inferred action conditions and to create new planning problems for the robot to solve and execute.

Fig. 3 :

 3 Fig. 3: Example of a high-level action for moving an object from A to B. Conditions are inferred from the observed predicates before (O 1 ) and after (O 2 ) the demonstration.

Fig. 4 :

 4 Fig. 4: The iRoPro interface showing the action condition menu and an interactive visualisation of the Baxter robot and detected objects.

Fig. 5 :

 5 Fig. 5: Snapshots from the executions of the system evaluation showing Task 3 (top) and 4 (bottom).

#

  Task goal Pick-and-place action 1 Build tower with 3 CUBES claw from top 2 Build tower with 4 CUBES claw from top 3 Rebuild Task 2 on a different position claw from top 4 Build tower and move (w/o disassembly) claw from top & side 5 Build house with BASE, CUBE, ROOF claw & suction from top 6 Rebuild Task 5 on a different position claw & suction from top

IFig. 6 :

 6 Fig.6: User responses from the post-study survey comparing a) iRoPro (N=20) to b) our previous user study (N=11)[START_REF] Liang | Evaluation of a Robot Programming Framework for Non-Experts using Symbolic Planning Representations[END_REF]

TABLE II :

 II Benchmark tasks for the user study where the first two tasks were used to introduce participants to the system.

	# Task description	Main solution
	(1) move BASE object (suction grip) create new action (+demo)
	(2) move BASE object to any position create new problem
	3 swap two BASE objects	add condition ('is clear')
	4 stack CUBE on BASE	modify types ('OBJECT')
	5 do not stack CUBE on ROOF	add condition ('is stackable')
	6 move ROOF object (claw grip)	create new action (+demo)
	7 stack ROOF on a CUBE	modify types ('ELEMENT')
	8 build a house (BASE, CUBE, ROOF) navigate autonomously

TABLE III :

 III User performance comparing task completion times with pre-study test scores.

		Main tasks (in min)	PT score (out of 7)
		AVG	STD	AVG	STD
	no experience	43.6	5.37	5.8	0.95
	non-CS	36.6	7.46	6.2	0.55
	CS	43.8	14.13	5.3	1.11
	Overall	41.2	9.08	5.8	0.91
	Group 1	41.0	7.89	6.1	0.77
	Group 2	41.4	10.56	5.5	0.98

ACKNOWLEDGMENTS

We would like to thank Nadine Mandran for supporting the experiment design process.


E Renner

Y Gaillard

F Richard

P Delobelle

F Amiot

Single crystal plasticity parameters identification from residual imprint topography after nano-indentation

Keywords: AFM, identification, single crystal plasticity, nano-indentation

Fundamental deformation mechanisms of FCC materials under indentation have been probed at the grain scale. Experimental tests have been conducted on large-grained annealed and coldworked polycrystalline nickel samples with a Berkovich indenter. Indentation axes have been chosen to be close to the three main crystallographic directions [001], [101] and [111]. Pile-ups and slip traces have been revealed around the residual imprints by analyzing topographic measurements obtained by atomic force microscopy. It is shown that the indenter orientation in each indentation plane drives pileups and slip traces which in turn contain precious information about the crystallographic orientation and the hardening state of the studied grain. Imprint topographies after pile-up formation therefore carry information that one can exploit to assess some intrinsic material properties at the grain scale. A 3D finite element modeling of the nano-indentation test at the grain scale has been developed, making use of crystal plasticity constitutive laws. Six different virtual materials having the same macroscopic behavior have been built. The simulation results show a good agreement with experimental tests and also a great pile-up sensitivity to interaction matrix components. These results pave the way to the interaction matrix identification using an inverse finite element method.

Introduction Whether based on continuum mechanics or dislocation dynamics, crystal plasticity models involve generally a large number of material parameters, making the description of the phenomena very complete [START_REF] Méric | Single crystal modeling for structural calculations: part 1 -model presentation[END_REF]. In this way, the critical resolved shear stresses for the different slip or twinning systems (CRSS), hardening parameters accounting for dislocation interaction, dislocation annihilation or nucleation terms can lead to models making use of more than 20 parameters. The extraction of each one of them from experimental mechanical data by inverse method is thus challenging. In this aim, assessing the uniqueness and the sensitivity of the identified set of parameters is crucial.

We investigate herein the information contained in the residual topography obtained after an indentation test. As suggested by Zambaldi et al. [START_REF] Zambaldi | Plastic anisotropy of g -TiAl revealed by axisymmetric indentation[END_REF], this topography can be used as a fingerprint of the underlying crystal deformation processes. As pile-up distribution around an indentation imprint performed on a single crystal strongly depends on the indented crystal orientation, it may serve the identification of single-crystal plasticity parameters.

Experimental The experimental part makes use of three polycrystalline nickel samples. The first nickel sample (a) has very small grains (average grain size about 0.37µm) and was obtained by electrodeposition with a thickness of 300µm. The second one (b) is a 99.9% pure nickel sample (Goodfellow society) with large grains (average grain size about 140µm) and was obtained after 3 h annealing at 900 o C of a cast ingot. The last one (c) is obtained by work-hardening (30% in traction) the annealed nickel sample (average grain size of about 168µm). Samples have been indented at room temperature with a Berkovich diamond tip, so as to always obtain an indentation depth of about 900 nm. Indentations have been performed in three different crystallographic planes close to the {001}, {101} and {111} family of lattice planes, with varying indenter's orientations in the lattice plane. All indentation imprints have been observed with an atomic force microscope to reveal the pile-up distribution and sizes. These results particularly demonstrate a strong dependence of the imprint to the indenter's orientation. It is also recovered that the residual deformation amplitude strongly depends on the hardening rate. FEM simulations Three dimensional numerical simulations of the nano-indentation test have been performed using the finite element code Zebulon [START_REF] Renner | Sensitivity of the residual topography to single crystal plasticity parameters in Berkovich nanoindentation on FCC nickel[END_REF], using elastic parameters from the literature, plausible viscoplastic parameters and different sets of micro-plastic parameters obtained from a tensile stressstrain curve, and assuming a particular term of the interaction matrix is dominant. These FEM simulations yield numerical topographies which are compared to the experimental ones (See Figure 1 for the plane {001}). The comparison is qualitatively good, and these simulations additionally yield indications of the sensitivity of the topography to the various terms in the interaction matrix. Conclusion Pile-up distribution experimentally observed around residual imprint of indentation is strongly related to the indented crystallographic orientation and to the Berkovich indenter orientation in a given indented plane. Moreover, hardening rate appears to play a crucial role on the pile-up dimensions. A numerical modeling of the nano-indentation test has been implemented in a finite element code. The parameters of the single crystal plasticity material model previously identified have been introduced. Numerical simulation results are in a good agreement with the experimental observations: pile-ups are distributed in the same way. Moreover, pile-up heights and widths share the same order of magnitude. Therefore, an inverse finite element method from a Berkovich nano-indentation experiment (residual topography, indentation curve), appears to be a possible way to extract some of the material's constitutive parameters involved in the Meric-Cailletaud's model. Above all, there may be enough information in measured topographies to estimate some components of the interaction matrix.

Figure 1 :

 1 Figure 1: Experimental and various computed residual topographies (plane {001}).