Jean-Luc Béchennec
email: jean-luc.bechennec@ls2n.fr

H ) Roux

Control of DES with urgency, avoidability and ineluctability

Keywords: Finite automata, Game theory, Controller synthesis, Timed systems

The synthesis of controllers for reactive systems can be done by computing winning strategies in two-player games. Timed (game) Automata are an appropriate formalism to model real-time embedded systems but are not easy to use for controller synthesis for two reasons: i) timed models require the knowledge of the precise timings of the system (for example, if an action must occur in the future, the deadline of this occurence must be known) ii) in practice, the dense state space makes the computation of the controller often impossible for complex systems. This paper introduces an extension of untimed game automata with logical time. The new semantics introduces two new types of uncontrollable actions: delayed actions which are possibly avoidable, and ineluctable actions which will eventually happen if nothing is done to abort it. The controller synthesis problem is adapted to this new semantics. This paper focuses specifically on the reachability and safety objectives and gives algorithms to generate a controller. The usefulness of this new model is illustrated by a device driver synthesis example.

I. INTRODUCTION

The theory of supervisory control has been well developed since about 30 years ago with the seminal works of [START_REF] Wonham | On the supremal controllable sublanguage of a given language[END_REF]- [START_REF] Golaszewski | Control of discrete event processes with forced events[END_REF]. It has become a basic paradigm for the control of discrete event systems (DES) modeled as finite state machines.

Since [START_REF] Ramadge | Supervisory control of a class of discrete event processes[END_REF], different formalisms have been considered to model (un)controllable actions and control problems. Formulating control problems as two-player games has provided efficient solutions [START_REF] Thomas | On the synthesis of strategies in infinite games[END_REF]. In this setting, the controller is modeled by a player and the environment by its opponent. Determining whether a controller exists amounts to determining if it can win and computing a winning strategy is equivalent to synthesizing a controller. However these turn-based games [START_REF] Thomas | On the synthesis of strategies in infinite games[END_REF] where one player chooses their action before the other chooses theirs, are sequential and do not allow to model concurrency. Therefore, concurrent games [START_REF] Chatterjee | Strategy improvement for concurrent reachability and safety games[END_REF]- [START_REF] De Alfaro | Concurrent reachability games[END_REF] have been proposed, for which, at each round of the game, player 1 (the controller) and player 2 (the environment) independently and simultaneously choose moves, and both choices are used to determine the next state of the game.

Beside the controllable and uncontrollable actions used in untimed frameworks, controlled systems often rely on additional behavioral capabilities, based in particular on two important notions: delays and urgency. Without delays, we cannot express the fact that some actions (such as analog conversions, or emissions of messages on a communication bus) take time, and that the controller can perform actions during that time, even aborting the current environment operation. In that case the controller must make use of some kind of urgency. In addition, without urgency, we cannot model ineluctable behaviors (such as the eventual arrival of a product at the end of the conveyor belt on which it is placed) of the environment since, in untimed games, the environment is expected to play every move at its disposal to make the controller fail, including choosing not to play.

The model of timed automata [START_REF] Alur | A theory of timed automata[END_REF] and timed games [START_REF] Alfaro | The element of surprise in timed games[END_REF] is an appropriate formalism to express and model these timed properties. In a timed game, the time at which the two players (controller and environment), play their moves is taken explicitly into account. Their level of expressiveness and wellknown controller synthesis techniques and tools [START_REF] Altisen | Tools for controller synthesis of timed systems[END_REF], [START_REF] Behrmann | Uppaal-tiga: Time for playing games![END_REF] allow the modeling of systems with complex interactions, while providing a formal proof on the behavior of the system. Yet, the computational complexity of the involved algorithms limits the size of the systems that can be addressed in practice.

Moreover, these timed formalisms require a good understanding of all the components of the system, including the knowledge of the timings of the actions of both players. These timings are rarely known precisely. Moreover, when these timings are known, or at least bounds on those timings, the complexity of the timed controller synthesis algorithms is still a problem.

Hence, it would be very interesting to derive a controller without explicit timed models (i.e. without precise timing quantification) while keeping the notion of urgency and delay. The behavior we would like to capture can be reduced into two types of uncontrollable actions:

• Delayed (avoidable) actions, which take time to complete or cannot happen immediately, such as writing to an external memory, sending a message on a bus, performing a specific computation on a hardware dedicated unit, etc. These actions usually come with some kind of abortion mechanism, so they are avoidable from a certain point of view. They are modeled in an explicit timed context by guard constraints with non-zero lower bounds on clocks. • Ineluctable actions, which are known to happen in a nominal context: the end of a transmission or a conversion, or more generally an acknowledgement of the reception of a command. An ineluctable action is guaranteed to happen eventually if nothing is done to abort it, which differs to the notion of fairness. In the untimed context, it is not sufficient to consider these actions as controllable. First, except if it is explicitly avoidable, an ineluctable action cannot be prevented by the controller, even if it leads to losing the game. Second, when there is a choice between two controllable actions, the controller chooses but when it is between two ineluctable actions, the environment chooses.

Our contribution.: We propose to extend the framework of untimed games with avoidability and ineluctability for uncontrollable actions and with urgency for controllable actions:

• an avoidable (delayed) action cannot happen immediately so that the controller can perform an urgent action to avoid it if needed. • an ineluctable action is guaranteed to happen eventually if nothing else is done to abort it, and the controller may want to rely on it. We revisit the controller synthesis problem for reachability and safety games in this context leading to what we call logical timed games.

This paper is organized as follows:

We first give in Section II, the basic definitions and notations for logical timed games. By using these notations, we justify our new model in Section III. Then, in Section IV, we solve the controller synthesis problem for logical timed games. In Section V and Section VI we respectively focus on reachability games and safety games. We discuss the complexity of the winning state computation algorithm implemented in our tool ROM ÉO in section VII. Finally, in Section VIII we illustrate our method on a case study based on the Microchip CAN controller.

II. LOGICAL TIMED GAMES

In this section we propose a variant of the traditional untimed game automata with new logical-timed semantics capturing avoidability and ineluctability.

Let C and U be the two players respectively called controller and environment.

Definition 1 (Game structure). A game structure is a tuple G = (Q, q 0 , A C , A U , δ) where • Q is a set of states • q 0 ∈ Q is the initial state • A C
and A U are two disjoint sets of actions for the controller and the environment, respectively.

• δ : Q × (A C ∪ A U ) × Q a set of edges between states.
We denote q a -→ q for (q, a, q ) ∈ δ.

For the sake of simplicity, we assume the underlying finite automaton is deterministic.

In addition to this definition, we define A U ⊆ A U and A U ⊆ A U the subsets of avoidable and ineluctable actions, respectively. Note that these subsets are independent, and their intersection is not necessarily empty.

We also denote A U , A U , A U , A U , A U and A U , the other subsets of A U based on these two notions. As an example, A U is the subset of actions of A U which are not avoidable and not ineluctable and A U is the subset of actions of A U which are not ineluctable but can be either avoidable or not.

A. Graphical notations

For the following figures, we will use the following notations illustrated in Figure 1: • States are represented by circles, and the initial state is denoted q 0 . • Controllable transitions are represented by solid arrows.

• Uncontrollable transitions are represented by dashed arrows.

• Avoidable transitions start with a circle.

• Ineluctable transitions end with a double arrowhead.

q 0 q 1 q 2 q 3 q 4 q 5 c u ua ui uai

B. Behaviors in game structures

The behaviors in game structures are timed behaviors, but only at a logical level, in which we distinguish immediate actions from others: we thus denote by ∆ the set {0, •}, which represents the logical time at which an action is played. It can be instantaneous (0), or unknown (•). Semantically, a, 0 means that the action a is performed immediately, whereas in a, • , the action is performed at an unknown time, possibly zero.

Avoidable actions: From a given state q an avoidable action u (as in Figure 4) can be prevented by any other action c from the same state q by the timed action c, 0 .

Ineluctable actions: From a given state, an ineluctable action u, • will eventually happens if we do not do anything else from this state, that is to say if we wait long enough.

Avoidability and Ineluctability vs fairness: An ineluctable action can also be avoidable from a given state and the reachability game shown in Figure 2 is winning by doing c, 0 . Moreover, like any non-avoidable uncontrollable action, an ineluctable (non-avoidable) action can not be prevented by a controllable action. On the other hand it can be prevented

q 0 G Bad c u Figure 2.
Avoidable action (even ineluctable) can be prevented by the controller by an uncontrollable action that would perform a loop in null time. Hence the reachability games of Figure 3 are not winning showing the difference from the notion of fairness.

q 0 G u u i q 0 G q 1 u 1 u 2 u i

C. Predecessor, successor and run

For Σ ⊆ A C ∪A U , we define the predecessor and successor functions pre

Σ : 2 Q → 2 Q , suc Σ : 2 Q → 2 Q : Let X ⊆ Q, ∀q ∈ Q, q ∈ pre Σ (X) iff ∃a ∈ Σ and q ∈ X, s.t. q a - → q , and ∀q ∈ Q, q ∈ suc Σ (X) iff ∃a ∈ Σ and q ∈ X, s.t. q a - → q . If Σ = A C ∪ A U , we note pre(X) and suc(X)
A run of a game structure is a sequence q 0 a 1 , t 1 q 1 a 2 , t 2 q 2 . . . with a i ∈ A C ∪ A U , t i ∈ ∆, q i ∈ Q, and such that q i ai -→ q i+1 for all i >= 0. We denote by R the set of runs, and by R the set of finite runs. Note that a finite run always ends with a state.

For a run r ∈ R, we define First(r) the first state of r, States(r) the set of states which appear in r, and Act(r) the set of actions which appear in r. If r ∈ R, we define Last(r) the last state of r. We define the length |r| of a run r as the size of the subsequence a 1 , t 1 a 2 , t 2 . . ..

For R ⊆ R and X ⊆ Q, we denote by R| X the subset of R such that ∀r ∈ R| X , States(r) ⊆ X.

III. JUSTIFICATION FOR THIS NEW MODEL

For the examples used in this section, we consider a reachability game (formally defined in Section V) starting in q 0 where the goal is to reach a state denoted G.

A. Avoidable action

The problem of avoidable (delayable) actions can be solved by using timed models such as timed automata. The avoidable actions can be translated directly into guards with a non-zero lower bound on clocks as depicted in Figures 4.a and 4.b. Hence, timed games [START_REF] Alfaro | The element of surprise in timed games[END_REF], [START_REF] Maler | On the synthesis of discrete controllers for timed systems[END_REF] allow to solve the controller synthesis problem for reachability or safety goal. In [START_REF] Tripakis | On-the-fly controller synthesis for discrete and dense-time systems[END_REF], the authors consider an abstraction of timed automata [START_REF] Alur | A theory of timed automata[END_REF] where a transition τ represents the fact that some time elapse. The authors argue that the abstract timed transitions (τ ) can be considered as controllable for the purposes of controller synthesis. This abstraction does not require explicit delays and if τ represents non-null elapsing of time, from a state q 0 , an action τ followed by an uncontrollable action u is equivalent to an avoidable action u from q 0 as depicted in Figure 4.c. In [START_REF] Tripakis | On-the-fly controller synthesis for discrete and dense-time systems[END_REF], this abstraction is generated by a quotient of the timed game automata by a time-abstracting bisimulation and can be viewed as a game graph on which the complexity of the controller synthesis algorithm is quadratic in the size of the graph.

B. Ineluctable action

Ineluctable actions are known to happen in a nominal context: the end of a transmission or a conversion, or more generally an acknowledgement of the reception of a command.

Ineluctable action vs controllable action: In the untimed context, it is not sufficient to consider these actions as controllable. First, an ineluctable action cannot be prevented by the controller, even if it leads to losing the game (see Figure 5). Second, when there is a choice between two controllable actions, the controller chooses but when it is between two ineluctable actions, the environment chooses. For example, in Figure . 6, assume the emission of a message on a communication bus (action c). It can lead to an immediate success (action u 2 ) or it can first fail (action u 1 ) and can become a success later. It is ineluctable that either u 1 or u 2 occurs, but the choice between u 1 and u 2 does not depend from the controller which have to ensure that both states q 1 and q 2 are winning.

q 0 G Bad c u Figure 5
. Ineluctable action cannot be prevented by the controller

q 0 q 1 G q 2 G c u 2 u 1 w Figure 6.
Ineluctable action is not selected by the controller

Ineluctable action vs timed action: In the timed context, ineluctability cannot be translated as-is into and from timed automata. We can use invariants on locations to force the environment to play, but this requires the knowledge of an upper bound on the delay, which is often not possible.

Moreover invariants apply to all players, including the controller, whereas ineluctable actions only restrict the behaviour of the environment. In [START_REF] Th | Playing games with timed games[END_REF], Timed Games are based on Timed Automata with invariants which are restricted to constraints of the form x ≤ k (where x is a clock and k is a constant). However, the environment can decide not to take action if an invariant requires to leave a state and the controller can do so.

Although the current work has not done so, it is possible to extend Timed Game Automata in order to take into account ineluctability for example by extending the notion of deadline or urgency [START_REF] Bornot | An algebraic framework for urgency[END_REF]. However, reachability and safety timed games are decidable but are EXPTIME-complete and the symbolic states manipulated by the algorithms are regions or zones that are too powerful for untimed models and limit the size of the systems that can be addressed in practice.

Our model eliminates the need to put explicit values on time invariants and only restricts the behaviour of the environment and not that of the controller.

IV. CONTROLLER SYNTHESIS

In this section, we will solve the controller synthesis problem using our modified semantics. The goal is to derive a strategy for the controller to restrict the behavior of the game. Those strategies prescribe either a set of controllable moves that should be done either immediately, or with no timing restriction, or to wait and do nothing until some action happens, which is represented by an empty set.

Definition 2 (Strategy).

A strategy s i for player i ∈ {C, U } is a function s i : R → 2 (Ai×∆) . It is said to be memoryless if it only depends on the current state of the run, i.e. s i : Q → 2 (Ai×∆) .

We impose that if a, d ∈ s(r), then a is indeed possible from Last(r).

Definition 3 (Strategies with ineluctable and avoidable actions). Let s U : R → 2 (A U ×∆) be a strategy of the environment and let r be a run in the game, with Last(r) = q.

If there exists a ∈ A U , d ∈ ∆, and a state q such that q a, d

- → q then s U (r) = ∅.
If there exists a ∈ A U , d ∈ ∆, and a state q such that q a, d -→ q , and if a, d ∈ s U (r), then d = 0.

Starting from a run consisting of some state (usually the initial state), both players inductively build a set of runs (because of non-determinism) by playing their strategy. Since we are interested in the strategies for the controller to win whatever the (legal) strategy of the environment, we directly define outcomes of a strategy of the controller, as the union over all strategies of the environment of all such sets of runs.

Definition 4 (Outcome). Let G = (Q, q 0 , A C , A U , δ) be a game structure, r one of its runs, and s C a strategy for the controller. The outcome Outcome(q, s C ) of s C from state q is the subset of R defined inductively by:

• q ∈ Outcome(q, s C ) • If r ∈ Outcome(q, s C ) is finite, r = r a, d - → q ∈ Outcome(q, s C ) if r ∈ R
and one of the following holds true:

-a ∈ A U and d = • if (r a - → q s.t. a , 0 ∈ s C (r)), or d = 0 otherwise; -a ∈ A U , d = •, and (r a - → q s.t. a , 0 ∈ s C (r)). -a, d ∈ s C (r).
• An infinite run belongs to Outcome(q, s C ) if all its finite prefixes also belong to Outcome(q, s C )

Intuitively, we are interested in runs that are long enough to have a chance to fulfill the objective. Maximality distinguishes those runs that are the longest that the controller can produce, through its actions (possibly with diverting moves from the environment) or by relying on the ineluctable actions of the environment.

A run r is maximal in a set of runs R if either it is finite and there is no a ∈ A C ∪ A U , and no q ∈ Q such that r a -→ q ∈ R, or it is infinite and none of its finite prefixes are maximal. We denote by MaxOutcome(q, s C ) the set of runs that are maximal in Outcome(q, s C ).

The control synthesis problem can be stated using objectives, or winning conditions. For a given game structure G, a winning condition C W is a set of allowed runs. We call the pair (G, C W ) a game.

In such a game, a strategy s for the controller is winning from state q if MaxOutcome(q, s) ⊆ C W . A state q is winning if there exists a winning strategy from q. The game itself is winning if q 0 is winning.

V. REACHABILITY GAMES

A reachability objective of the controller is to force the game to reach a certain set of states. Formally: Definition 5 (Reachability objective). Let G = (Q, q 0 , A C , A U , δ) be a game structure, and Goal ⊆ Q a set of goal states. The reachability objective Reach(Goal) for Goal is the set of runs r that are maximal in R and such that States(r) ∩ Goal = ∅.

For example, for the game of Figure 7, the objective is to reach the state G and we have Goal = {G} and Reach(Goal) = {q 0 c, • q 1 u, • G}.

q 0 q 1 G c u

A. Computing the strategy

The computation of the strategy is obtained from the set of winning states. A state is winning for the controller if it is possible to reach a goal state from the strategy i.e. if the controller has a strategy to reach a goal state against all strategies of the environment. The main algorithm for computing winning strategies for reachability games is a backwards fixedpoint algorithm over the controllable predecessor function.

Intuitively, a state s is a controllable predecessor of X if the following conditions are met:

• there is an action which is guaranteed to happen (either controllable or uncontrollable ineluctable) and leads to X; • all other actions of the environment cannot prevent the game to reach a state in X.

Definition 6 (Controllable predecessors).

Let G = (Q, q 0 , A C , A U , δ) be a game structure, and X ⊆ Q a set of states. The controllable predecessors π(X) of X is the subset of Q defined by:

π(X) = pre A C (X) \ pre A U (X) ∪ pre A U (X) \ pre A U (X) (1)
The two parts of the formula represent two different ways to win:

• if there is a controllable action from s to a state in X, all uncontrollable actions must either be avoidable, or also lead to states in X • if there is an ineluctable uncontrollable action, all other uncontrollable actions must also lead to a state in X. Given this new definition of π, the set of winning states is computed using the following classic backwards fixed-point algorithm: W 0 = Goal and W n+1 = W n ∪ π(W n ). When it exists, the final fixed-point set is noted W.

Algorithm 1 Winning states computation algorithm for reachability game

Input: G = (Q, q 0 , A C , A U , →) , Goal ⊆ Q Output: W W ← Goal while π(W) ⊆ W do W ← W ∪ π(W) end while return W Lemma 1.
Let (G, C W ) be a reachability game. Let q 1 and q 2 be two states of G. Let s 1 be a memoryless strategy that is winning from q 1 and s 2 be a memoryless strategy that is winning from q 2 . Let Q 1 be the set of states of runs r in Outcome(q 1 , s 1 ) such that States(r) ∩ Goal = ∅ (i.e. the states that are traversed before reaching Goal).

Let s be the memoryless strategy defined by: for all q ∈ Q, if q ∈ Q 1 then s(q) = s 1 (q), otherwise s(q) = s 2 (q). Then s is winning from both q 1 and q 2 .

Proof. The fact that s is winning from q 1 is obvious. Now, from q 2 this is also quite straightforward. Let r be a run in MaxOutcome(q 2 , s). If States(r) ∩ Q 1 = ∅ then r ∈ MaxOutcome(q 2 , s 2 ) and therefore it eventually goes through Goal. Otherwise, we can write r as r 2 r 1 , with r 2 ∈ Outcome(q 2 , s 2 ), Last(r 2 ) ∈ Q 1 and r 1 ∈ Outcome(Last(r 2 ), s 1 ). Since Last(r 2 ) ∈ Q 1 , and since from there we follow the s 1 , then for sure r 1 eventually goes through Goal.

Lemma 2. If q ∈ W n (i.e. the value of W at the end of the n-th iteration of the while loop) then there exists a winning memoryless strategy from q that permits to win in n action steps or less.

Proof. By induction on n.

Base case: before the first iteration of the while loop, W 0 = Goal, and q ∈ Goal implies that we have a strategy to win without doing anything. It is indeed equivalent to having a run with no action step from q to Goal.

Induction step: suppose the property holds for some n ≥ 0. Let q ∈ W n+1 . Then either q ∈ W n or q ∈ π(W n ).

If q ∈ W n , then the induction hypothesis directly gives the result.

If q ∈ W n and therefore q ∈ π(W n ). Two more cases arise:

• either q ∈ pre A C (W n ) \ pre A U (W n ):
then there exists some a ∈ A C and q a ∈ W n such that q a -→ q a . Let {b 1 , . . . , b p } be the set of uncontrollable, non-ineluctable actions possible in q and let q i be the state such that q bi -→ q i for all i. Then q i ∈ W n , because q ∈ pre A U (W n ). By the induction hypothesis, we know that there are memoryless winning strategies s a from q a , and s i for each of the q i 's. By Lemma 1, we can merge all those strategies in one memoryless strategy s . Now, we exhibit a winning strategy: let s be the memoryless strategy such that s(q) = { a, 0 } and s(q ) = s (q ) for all q = q. Let us prove that s is indeed winning from q. Let r be a run in MaxOutcome(q, s). Note that the run consisting of only q cannot be maximal since a ∈ A C . Therefore we have at least one action in r. Consider the first of those and call it x:

-First suppose that x ∈ A C . Then we must have x = a because s says to play a in q. Now, remark that since q ∈ W n , it is clear that it never appears in the outcomes of s from q a or any of the q b 's, so the outcomes of s and s from those states are the same. Consequently, all maximal runs from q that start with a will eventually go through Goal because s is winning. -Suppose now that x ∈ A U . Then we must have

x ∈ A U because s says to play immediately in q. Furthermore, the state reached by taking x is one of the q i 's defined above, from which s is winning, and with the same argument as in the previous point, the maximal runs that start with x also eventually go through Goal.

• or q ∈ pre A U (W n ) \ pre A U (W n ).
This case is fairly similar to the previous one: we know there exists some a ∈ A U and q a ∈ W n such that q a -→ q a . Let {b 1 , . . . , b p } be the set of uncontrollable actions possible in q and let q i be the state such that q bi -→ q i for all i. Then q i ∈ W n , because q ∈ pre A U (W n ). By the induction hypothesis, we know that there are memoryless winning strategies s a from q a , and s i for each of the q i 's. By Lemma 1, we can merge all those strategies in one memoryless strategy s . Let s be the memoryless strategy such that s(q) = ∅ and s(q ) = s (q ) for all q = q. We prove that s is winning from q. Let r be a run in MaxOutcome(q, s). Note that the run consisting of only q cannot be maximal since a ∈ A U . Therefore we have at least one action in r. Consider the first of those and call it x. Since the strategy says to wait, we cannot have x ∈ A C . So x ∈ A U , and the state reached by taking x is one of the q i 's above and we get the result with the same reasoning as before. Lemma 3. If there exists a winning strategy from state q that permits to win in n action steps or less, then q ∈ W n .

Proof. By induction on n.

Base case: If we can win without changing states, it must be the case that q ∈ Goal = W 0 .

Induction step: suppose the property holds for some n ≥ 0. Suppose that we have a winning strategy s from state q such that all runs in MaxOutcome(q, s) reach Goal in at most n+1 steps.

Consider the possible actions from q. If they all are uncontrollable and not ineluctable, or there is also controllable transitions but s(q) = ∅, then q is itself a maximal run and therefore q ∈ Goal = W 0 , which implies that q ∈ W n+1 . Otherwise:

• either there is at least a controllable action a in s(q). Then it will be present in the outcome of s from q, leading to a state q a , and then, since s is winning from q it is also from q a , but in at most n steps. So we can apply the induction hypothesis and conclude that q

∈ pre A C (W n ).
By definition of the outcome, uncontrollable, nonineluctable actions always appear in the outcome of s from q and, with the same reasoning, they all lead to states in W n . So q ∈ pre A U (W n ). And finally q ∈ W n+1 . • or there is no controllable action in s(q) but there is at least an ineluctable uncontrollable action x possible from q. So x appears in the outcome of s from q and, as before, q ∈ pre A U (W n ). Similarly all possible uncontrollable actions appear in the outcome (since the strategy must be to wait) and, again as before, they therefore all lead to W n . Consequently, q ∈ W n+1 .

From Lemmas 2 and 3, we can deduce the following two results:

Theorem 1 (Completeness and Soundness). q ∈ W if and only if q is winning.

Proof. If q is winning then there is a strategy from q that permits to win in a finite number of steps. So, by Lemma 3, q ∈ W n for some n. Reciprocally, if q ∈ W, it is in W n for some n and, by Lemma 2, it is winning.

Theorem 2 (Memoryless strategies). If the game is winning then it is winning with a memoryless strategy.

Proof. If the game is winning then its initial state q 0 is winning with a strategy that permits to win in a finite number of steps then, by Lemma 3, q 0 is in W n for some n and, by Lemma 2, there is therefore a winning memoryless strategy from q 0 . The proof of Lemma 2 shows how one can effectively build a memoryless winning strategy when the game is winning: at each iteration, each new state added to W has either at least a controllable or an uncontrollable ineluctable transition to a state of W that was added in a previous iteration. The strategy can be the set (or any of its subsets) of those controllable actions. Those controllable actions are played at time 0 in the proof to keep it simple, but it is clear that if no delayable action to W is possible, they can also be played at time •.

It is clear that this strategy also ensures that the goal states are reached in the minimal number of steps possible.

Also note that, as always for reachability games, the canonical strategy that would always allow to move to any state in W is not winning in general since it might allow loops within W, and thus infinite runs never reaching to goal states.

B. Reachability game example

Let us consider the reachability game G = (Q, q 0 , A C , A U , δ) of Figure 8 where the objective is to reach the state G: Goal = {G}. By applying the backward fixedpoint algorithm 1: W 0 = Goal and W n+1 = W n ∪ π(W n ), we obtain successively:

W 0 = {G}, π(W 0 ) = {q 4 }, W 1 = {G, q 4 }, π(W 1 ) = {q 3 , q 4 }, W 2 = {G, q 3 , q 4 }, π(W 2 ) = {q 2 , q 3 , q 4 }, W 3 = {G, q 2 ,
q 3 , q 4 }, π(W 3 ) = {q 0 , q 2 , q 3 , q 4 }, W 4 = {G, q 0 , q 2 , q 3 , q 4 }, π(W 4 ) = {q 0 , q 2 , q 3 , q 4 } A winning memoryless strategy is s(q

0 ) = { c 1 , 0 }, s(q 3 ) = { c 2 , 0 }, s(q 4 ) = { c 3 , • } and s(q 1 ) = s(q 2 ) = s(G) = ∅. q 0 q 1 q 2 q 4 q 3 G a 1 a 2 u 1 c 1 c 2 u 3

VI. SAFETY GAME

A safety objective for the controller is to force the game to stay in a specified set of states, or equivalently, to avoid a set of states.

Definition 7 (Safety objective).

Let G = (Q, q 0 , A C , A U , →) be a game structure and Safe ⊆ Q a set of safe states. The safety objective for Safe is the set of all infinite maximal runs r of G such that States(r) ⊆ Safe.

Note that we exclude finite maximal runs from the objective because we do not want the controller to win by deadlocking or by reaching an uncontrollable livelock i.e. a set of states with no outgoing controllable transition. It means that when the environment decides to not play, the controller must be able to move. Hence, the safety games of Figure 9 where all the states are in the set of safe states, are loosing. Indeed, for the game of Figure 9.a, we have q 0 ∈ π({q 0 }) and for the games of Figures 9.b and 9.c, we have q 1 ∈ π({q 0 , q 1 , q 2 }) meaning that the environment can block in q 1 (by not playing u 1 since it is not ineluctable) and to avoid q 1 , the controller must block in q 0 . A contrario, the games of Figure 10

q 0 u q 0 q 1 q 2 c 1 u 1 u 2 q 0 q 1 q 2 c 1 u 1 u 2 c 2
q 0 u c q 0 q 1 q 2 c 1 c 2 u 1 u 2 Figure 10
. All the states are safe and the games are winning.

A. Computation of the strategy

The strategy is computed from the set of winning states. A state is winning for the controller if it is possible to force the game to stay in Safe.

Given our new definition of π, the set of winning states for the controller is computed using the following classic backwards fixed-point algorithm:

W 0 = Safe and W n+1 = W n ∩ π(W n ).
When it exists, the final fixed-point set is noted W. Like in Section V, we can prove the soundness and completeness of Algorithm 2, by proving the following two Algorithm 2 Winning states computation algorithm for safety games

Input: G = (Q, q 0 , A C , A U , →) , Safe ⊆ Q Output: W W ← Safe while W ⊆ π(W) do W ← W ∩ π(W) end while return W
lemmas. The proof are very similar to those of Section V and are therefore omitted. Lemma 4. If q ∈ W n then there exists a memoryless strategy s such that for any prefix r of length n of a run in MaxOutcome(q, s), we have States(r) ⊆ Safe. Lemma 5. If there exists a strategy s and a run r such that for any prefix r of length n of a run in MaxOutcome(q, s), we have States(r ) ⊆ Safe, then Last(r) ∈ W n .

From those two lemmas, the main results follow: Theorem 3 (Completeness and Soundness). q ∈ W if and only if q is winning.

Proof. If q is winning then there is a strategy s from q such that prefixes r of any length of runs in MaxOutcome(q, s) are such that States(r) ⊆ Safe. So, by Lemma 3, q ∈ W n for all n and, in particular, q ∈ W. Reciprocally, if q ∈ W, let n be such that W = W n , then for all m ≥ n, q ∈ W n . So for all m ≥ n, there is a memoryless strategy from q that stays in Safe for at least m steps. Since there is only a finite number of states and of actions, there is only a finite number of memoryless strategies on the game structure. So there is one that is winning for an infinity of m ≥ n, which implies that no prefix of the maximal runs in its outcome ever goes out of Safe, and therefore that strategy is winning.

Theorem 4 (Memoryless strategies). If the game is winning then it is winning with a memoryless strategy.

For safety games, and following the previous results, it is clear that moving to any winning state is always a winning strategy for the controller. We define a canonical memoryless strategy s s : W → 2 (A C ×∆) that does exactly that:

Let

s s (q) = { a, d |a ∈ A C , q a - → q ⇒ q ∈ W}, with d = 0 if ∃a ∈ A U , q ∈ W and d = • otherwise.
Permissive strategies are a key notion in supervisory control [START_REF] Ramadge | Supervisory control of a class of discrete event processes[END_REF]. In reactive synthesis, permissiveness is measured in terms of the set of behaviours allowed by the strategy [START_REF] Bernet | Permissive strategies: from parity games to safety games[END_REF]. Hence most permissive strategies need not exist, depending on the type of winning objectives.

Theorem 5. Strategy s s is the most permissive winning strategy for the safety objective Safe, i.e, for all winning strategies s , Outcome(q 0 , s ) ⊆ Outcome(q 0 , s s ).

Proof. Ab absurdo. Assume that s s is not the most permissive winning strategy. Then there exists a winning strategy s and a run in Outcome(q 0 , s )\Outcome(q 0 , s s ). Let r be the longest prefix of that run that is in Outcome(q 0 , s s ). Let q = Last(r).

Then we have, for some action a, q a, d -→ q ∈ Outcome(s , q) and q a, d -→ q ∈ Outcome(s s , q). We must have q ∈ W or s cannot be winning because of Theorem 3. Then, by definition of s s , it is not possible that a ∈ A C , so it must be the case that a ∈ A U . And, by definition of Outcome, the only possibility is that a ∈ A U , d = •, there is an action b ∈ A C , such that b, 0 ∈ s s (r), and there is no such action in s (r). This in turn implies that there is a third action c ∈ A U and a state q such that q c, • -→ q and q ∈ W. Since there is no immediate controllable action in s (r) then clearly r c, • -→ q ∈ Outcome(q 0 , s ), which, by Theorem 3, contradicts the fact that s is winning.

B. Safety game example

Let us consider the safety game G = (Q, q 0 , A C , A U , →) of Figure 11 where the objective is to avoid the state B. Hence Safe = {q 0 , q 1 , q 2 } is the set of safe states.

By applying the backward fixed-point algorithm 2: W 0 = Safe and W n+1 = W n ∩ π(W n ), we obtain successively:

W 0 = {q 0 , q 1 , q 2 }, π(W 0 ) = {q 0 , q 1 }, W 1 = {q 0 q 1 }, π(W 1 ) = {q 0 , q 1 }.
The most permissive memoryless strategy is s(q 0 ) = ∅ and s(q 1 ) = { c, 0 }.

q 0 q 1 q 2 B i a

VII. COMPLEXITY AND IMPLEMENTATION

While the algorithms we give are well-suited for pedagogical exposition and proofs, and possibly for an implementation using symbolic decision diagrams based representations of sets of states, they are not optimal for an explicit enumeration of states. Nonetheless, plugging our definition of the controllable predecessors operator π into the untimed algorithm of [START_REF] Cassez | Efficient on-the-fly algorithms for the analysis of timed games[END_REF], we can compute the winning states for reachability, or their complement for safety, in time linear with respect to the number of edges in the automaton.

Based on this latter algorithm, we have implemented the computation of the winning states and the synthesis of the strategy in our tool ROM ÉO [START_REF] Lime | Romeo: A parametric model-checker for Petri nets with stopwatches[END_REF]. With its textual input language, ROM ÉO handles a model called Clock Transition Systems (CTS) [START_REF] Jard | Clock Transition Systems[END_REF] which encompasses both finite automata and Petri Nets. We have extended CTS with controllable, uncontrollable, avoidable and ineluctable actions in order to model logical timed games. The CTS can be generated from the ROM ÉO GUI.

VIII. CASE STUDY

Device drivers synthesis is a good example of logical time game controllers synthesis. Here the environment is i) the hardware device along with its connections to external systems: communication networks, analog signals, etc and ii) the application using the driver. In the former case uncontrollable actions are interrupts that are triggered to signal, for instance, the availability of a data in a hardware buffer. In the latter case they are requests made by the application. In both cases exact timings are unknown since they depend on the actual hardware and on the execution time of the actual binary program which is not available yet. However some time related rules are known like the inter-arrival time of messages on a communication network or the time between two interrupts of a timer for instance. So, when reacting to an uncontrollable action the controller has time to perform its task before the arrival of the next same uncontrollable action. In such case the second action is avoidable.

A. CAN controller driver modelling

The device chosen for the case study is the Microchip CAN controller available in PIC18Cxx8 microcontroller family [START_REF]PIC18CXX8 Data Sheet (DS30475A)[END_REF]. This CAN controller features two receive buffers, RXB0 and RXB1 and three transmit buffers, TXB0, TXB1 and TXB2. Each of these buffers can hold a complete CAN message. For the sake of simplicity, we consider only one transmit buffer, which is called TXB, in this case study. The device is configured so that i) when a message is received from the bus it is put in one of the receive buffers and an interrupt is asserted. ii) when a message is written to the transmit buffer the device sends it as soon as possible and asserts an interrupts to notify TXB has just been emptied.

The model of the driver is presented at Figure 12. We added boolean variables: PW (Pending Write), RXB0IF (RXB0 Interrupt flag), RXB1IF (RXB1 Interrupt Flag), TXBIF (TXB Interrupt Flag) to simplify the drawing of the model. The driver is cut into two parts: the part that is executed in user mode, represented by white states and the part that is executed in the interrupt handler represented by gray states. In addition a black bad state that has to be avoided by the controller is added. Starting from the no init state the device can be configured as described above and the driver waits requests in the wait state. From there three uncontrollable actions, corresponding to a write request from the application (write TXB) or the arrival of a message in one of the receive buffer (can it 0 or can it 1), may occur and the corresponding boolean variable is set accordingly. From the write state we find again the two uncontrollable actions corresponding to the arrival of a message and also an ineluctable action which is done by the device when TXB is emptied. The state event represents the entry point of the device interrupt handler. From there the controller can play the actions corresponding to the processing of the event: read the receive buffer which has been filled (read0 or read1) or acknowledge the emptying of the transmit buffer (ack write).

During the execution of the interrupt handler uncontrollable actions are avoidable because i) device interrupts are masked ii) the controller has enough time to play its actions before the occurence of a new interrupt.

B. Winning strategy

We used our tool ROM ÉO [START_REF] Lime | Romeo: A parametric model-checker for Petri nets with stopwatches[END_REF] for the modelling of this case study and to compute the winning states and the synthesis of the strategy. We first verify that the safety property, where BAD is never reached, holds. But for safety ROM ÉO actually computes the complement of the fixed-point given in section VI and therefore computes a strategy for the environment to falsify the property. Of course it finds none. So in order to get the strategy for the controller we also verify a reachability objective.

To express this objective, we need to add two boolean variables called PLAYED wait, which is set when the environment plays an action to leave state wait, and PLAYED write which is set when the environment plays an action to leave state write. That way staying in state x (PLAYED x is false) and returning to this state after the environment has played (PLAYED x is true) can be distinguished. An additional state is also added, shutd. The shutd state models the fact that the system may be off. The start transition is the switching on of the system and the stop transition is the switching off of the system. If the environment decides to not play any action, shutdown will be reachable eventually. The goal of the controller is to reach one of the following states:

• shutdown,

• wait with PLAYED wait = true, • write with PLAYED write = true The strategy is summarized in Table I. Starting from no init the controller must play init to reach a winning state. In wait, if the environment plays can it 0 or can it 1, PLAYED is set and the controller has to play immediately read B0 -ret0 or read B1 -ret1, respectively, to go back to wait. If the environment plays write TXB, both PW and PLAYED are set. From write the environment may choose to play can it 0 pw or can it 1 pw. Then the controller has to play immediately read B0 -ret0 pw or read B1 -ret1 pw, respectively, to go back to write. If the environment decides to not play uncontrollable actions, inevitably can it w happens and the controller returns immediately to state wait by playing ackTX -retw.

IX. CONCLUSION

We have presented an extension of finite automata with logical time. This extension introduces two new properties of uncontrollable actions that extend the model of the environment:

• the delayed action cannot happen instantaneously so that the controller may preemptively perform another action if needed. • the ineluctable action is guaranteed to happen eventually, and the controller can hence rely on it. This model combines some of the expressiveness of timed games, with the simplicity of finite automata. It allows an easier implementation of these models, more suitable to embedded real-time systems. We have adapted the notion of control, reachability and safety games for this extension and defined and proved algorithms to solve these problems in the general case. Finally we have implemented the computation of the winning states and the synthesis of the strategy in our tool ROM ÉO.

Further work includes extending the approach to more complex control objectives, such as Büchi conditions, and deal with concurrent behaviors modelled by networks of finite automata.

Figure 1 .

 1 Figure 1. Graphical notation example: Here q 0 is the initial state, and c ∈ A C , u ∈ A U , ua ∈ A U , ui ∈ A U and uai ∈ A U .

Figure 3 .

 3 Figure 3. Ineluctability is not fairness.

Figure 4 .

 4 Figure 4. Avoidable uncontrollable action can be prevented by the controller

Figure 7 .

 7 Figure 7. The objective is to reach the state G.

u 2 c 3 iFigure 8 .

 38 Figure 8. A reachability game. The objective is to reach the state G.

Figure 9 .

 9 Figure 9. All the states are safe but the games are not winning.

Figure 11 .

 11 Figure 11. A winning safety game. The objective is to avoid the state B.

Figure 12 .

 12 Figure 12. PIC18Cxx8 CAN controller driver model. Guards are noted with a '?', negations are noted with a and updates are noted inside parenthesis with a ←.


V Pirenne

G Kurtay

S Voci

L Bouffier

N Sojic

F Robert

D M Bassani

Y Landais

Eosin-mediated Alkylsulfonyl-cyanation of Olefins

Eosin-Y (EY)-mediated alkylsulfonyl-cyanation of olefins was shown to afford alkylsulfonyl nitriles in good yields. On the basis of transient absorption spectroscopy, the reaction was shown to proceed via a photoinduced electron transfer from 3 EY* to an O-cyanated derivative of the photocatalyst, formed in situ, with generation of the corresponding sulfinate, finally oxidized by EY .+ into a sulfonyl radical. Addition of the latter on the olefin, followed by a radical cyano group transfer then furnished the nitrile along with a RSO2 radical sustaining the radical chain.

Sulfones represent an important subclass in the family of organosulfur compounds, exhibiting a wide range of biological activities. 1 They serve as key synthetic intermediates 2 for the construction of important building blocks in the total synthesis of natural products, 3 and the development of methodologies to access structurally complex sulfones is currently flourishing. 4 These are mostly based on the use of SO2, 5,6 or the free-radical addition of RSO2X (X = Cl, I, Br, CN, oxime, vinyl, alkynyl,…) to alkenes or alkynes. 7 The sulfonyl-cyanation of alkenes was reported by Fang et al. using AIBN as an initiator, 9 and later by Barton et al. using the photolysis of PTOC esters (Scheme 1). 10 These processes however require a large excess of olefin (10 equiv) and are limited to electron-rich olefins in the latter case. We envisioned extending the scope and application of the sulfonyl-cyanation reaction using conditions which would avoid desulfonylation and allow the incorporation of functionalized alkyl groups. Visible-light photocatalyzed processes are attracting a growing interest, [START_REF] Prier | For selected reviews on visible-light photoredox catalysis[END_REF] and appear well-suited to generate the required sulfonyl radical at room temperature from sulfonyl cyanide. 12 We now show that eosin-Y (EY) is able to promote the photoinduced sulfonylcyanation of alkenes from alkylsulfonyl cyanides in spite of energetically unfavorable electron transfer, thanks to an unexpected mechanism involving the cyanation of the photocatalyst which generates a co-catalytic intermediate (Scheme 1). This mechanism contrasts with the related addition of p-TsCN onto olefins proposed to occur by direct electron transfer. 13 To the best of our knowledge, the participation of EY adducts in photocatalyzed transformations has not been previously reported and provides an important new aspect to EY photocatalyzed processes. These results provide a general protocol for the formation of β-sulfonyl nitriles under mild reaction conditions. Preliminary studies starting from cyanide 1a and olefin 2a as model substrates in the presence of various organic and organometallic photocatalysts (Table S1-S2), showed that the conjunction of eosin-Y, visible light and K2HPO4 is required for optimal efficiency of the sulfonyl-cyanation process. The reaction was slow in CH2Cl2, whereas DMF leads to full conversion and an excellent yield after 20 h of irradiation (Table 1, entries 1-3). Decreasing the stoichiometry of the sulfonyl cyanide below 1.5 equiv (Table 1, entries 4-5), increasing the amount of EY to 10 mol % (Table 1, entry 6), or the presence of oxygen (Table 1, entry 7) lead to a lower yield. Scaling up of the process (1 mmol) using the optimal conditions led to high yields and similar reaction time (Table 1,entry 8). Finally, it was found that polar solvents such as acetonitrile or iPrOH were also effective for this reaction (Table 1, entries 9-11). The optimized reaction conditions were applied to a series of olefins using sulfonyl cyanide 1a (Scheme 2). 14 The EY-mediated sulfonyl-cyanation showed a broad scope with the corresponding alkylsulfonyl nitriles formed in high and reproducible yields. α-Pinene led to nitrile 3f in excellent yield, in agreement with a radical-based reaction mechanism. 14 Lower yields were, however, obtained from 1,1-disubstituted olefins (i.e. 3i-j-3p), but this could be circumvented using a larger amount of sulfonyl cyanide (e.g. 3i). The reaction was also found to be compatible with various functional groups including ketones (3b), bromides (3c), ester (3e), carbamate (3g) and silyl protecting groups (3l). With alkenes bearing free hydroxyl groups, the corresponding imidate was also formed. Treatment of the crude mixture of 3d with p-TsOH led to the corresponding lactone in one-pot operation and 54% over 2 steps (Supporting Information (SI)). The sulfonyl-cyanation also proceeds well with cyclic olefins such as 3,4-dihydro-2H-pyran (3m), cyclohexene (3n) and cyclopropene (3k), affording the corresponding nitriles as trans-diastereomers with high dr. Alkynes were found to be poorly reactive, although the stereoselectivity was high (3o). Finally, styrene did not react under our standard conditions. Scheme 2. Alkylsulfonyl-cyanation of olefins. Olefin scope.

Sulfonyl cyanation may be carried out with sulfonyl cyanides 1 (SI) bearing ester, ether, trifluoroacetate or aromatic groups attached to the sulfur atom (Scheme 3). The process is also efficient with secondary sulfonyl groups (4b-c), which showed no desulfonylation under the reaction conditions. A reaction of sulfonyl cyanide 1j with olefins 2b and 2j led to the corresponding trifluoroacetates 4j and 4k when purification was carried out through silica gel and free alcohols 4h and 4i when alumina was used. With 1,1-disubstituted olefins (e.g. 4-methylenepyrane), an excess of sulfonyl cyanide 1j was however necessary (e.g. 4k). The reaction of vinyl pivalate with sulfonyl cyanide 1e led to the carbocyanation product 4l in good yield. 14 Here, loss of SO2 is fast as a result of the formation of a stabilized C-centered radical resulting from the α-scission. Scheme 3. Alkylsulfonyl-cyanation of olefins. Sulfonyl cyanide scope.

A further illustration of the utility of this process is provided with the synthesis of metalloproteinase inhibitor 5 15 (Scheme 4). EYmediated sulfonyl-cyanation of alkene 2j led to the desired nitrile 4k, affording alcohol 6 in 69% yield after trifluoroacetate deprotection over alumina. The latter was then subjected to the Mitsunobu reaction, leading to ether 7 in 61% yield. Direct nitrile aminolysis of 7 in the presence of hydroxylamine (AcONa, EtOH-H2O, 80 °C) proved to be difficult, leading essentially to the corresponding amide (SI). Nitrile 7 was thus first hydrolyzed under basic aqueous conditions, leading to carboxylic acid 8, which was then converted into the desired hydroxamic acid 5 15 via the corresponding acyl chloride and NH2OH.

Scheme 4. Synthesis of metalloproteinase inhibitor 5.

In order to evidence radical chain processes, we carried out light-dark experiments using olefin 2a and 1a over a 50 h period (Figure S4). the reaction appears to stop the was off, we noticed that the formation of 3a at a slower rate in the dark. This suggests that an inefficient radical chain mechanism is operating, in contrast with what was previously reported for the addition of p-TsCN. 13 When the reaction was in the presence of 2 of TEMPO, no trace of 3a was detected, supporting the radical nature of the addition process. Eosin-Y possesses a short-lived singlet and a long-lived triplet excited state that can undergo oxidative or reductive photoinduced electron transfer (PET) quenching, depending on the nature of the substrate. [START_REF] Hari | use of eosin as a photoredox catalyst[END_REF] Fluorescence lifetime quenching measurements rule out a reaction from the singlet excited state (Figure S22), whereas time-resolved absorption experiments revealed the formation of a species possessing a transition at 420 nm, typically assigned to the formation of EY •+ (Figure S5). In the absence of 1a, only the transient absorption of 3 ET* (λmax = 440 nm) could be detected. The lack of electrochemical data for RSO2CN 17 led us to estimate the redox potential of several sulfonyl cyanides using cyclic voltammetry (Figure S7-8, Table S3). Alkylsulfonyl cyanides exhibit highly negative irreversible reduction potentials, rendering direct electron transfer from EY* very unlikely. For comparison, we find PET from 3 EY* to p-TsCN to be slightly endothermic (∆GPET = +5.3 Kcal/mol, SI). [START_REF]claims of Sun et al. 13 Reduction potentials for the sulfonyl cyanides are however irreversible, thereby explaining some variability in potentials[END_REF] In the case of sulfonyl cyanide 1a, we estimate ∆GPET = +5.1 or +14.1 Kcal/mol from 1 EY* or 3 EY*, respectively, assuming the energies of the singlet and triplet states of EY to be 2.28 and 1.89 eV, respectively, and E1/2(EY /EY +• ) = + 0.78 V vs SCE (SI). 16a- c Energy transfer from 3 EY* to the substrate followed by homolytic bond cleavage 19 is also unlikely since bond dissociation energies (Table S5) are systematically above those available from the triplet sensitizer (43 Kcal/mol). Greater complexity in the reaction mechanism is obvious from the electronic absorption spectra collected in parallel with these studies. In DMF solutions, the EY dianion absorbs strongly in the visible with an absorption maximum at 544 nm. [START_REF] Hari | use of eosin as a photoredox catalyst[END_REF] We observed a fast discoloration of the solution when mixing EY with 1a, accompanied by the appearance of a new, structured absorption with λmax = 475 nm (Figure S17). Although slower, the same process was also observed with p-TsCN. 1 H and 13 C NMR spectra as well as ROESY experiments did not reveal weak or through-space interactions between EY and the sulfonyl cyanides. [START_REF] Quint | [END_REF] Based on tabulated data for substituted EY derivatives, 21 we assign this new species to the formation of the cyanate derivative of EY (EY-CN, Figure 1). Indeed, the reaction of phenoxides with p-TsCN to yield the corresponding cyanate is reported to occur rapidly, even at low temperature through an addition-elimination reaction releasing the sulfinate anion. 22 To verify this hypothesis, we compared the absorption spectrum of the intermediate with that of the O-methylated derivative of EY. In agreement with the proposed structure, the two spectra are nearly identical (Figure 1). Furthermore, we find that the adduct is rapidly hydrolyzed by the addition of water (see Figure S17), and that the addition of K2HPO4, which may contain traces of water, partly converts the adduct to release EY. From the absorption spectrum, we estimate the proportion of EY that is converted to EY-CN to be ca. 75%. The absorption envelope of the EY-CN adduct is broad and overlaps well with the emission profile of the light source.

To verify whether the adduct exhibits photocatalytic activity, we compared the photoreaction yields using sulfonyl cyanide 1a and olefin 2a, with those obtained upon monochromatic irradiation at 436 nm (where EY does not absorb) or in the presence of EY-Me. In all cases, only a low yield of the corresponding sulfonyl-cyanation product 3a was obtained, suggesting that the EY-CN adduct generated upon EY bleaching is not, or only weakly, photoactive. In contrast with 1a, the greater electrophillicity of EtO2CCH2SO2CN (1e) or ClCH2SO2CN (1i) led to the complete conversion of EY to the adduct, thereby explaining the absence of sulfonyl cyanation products in these cases (SI).

Although the EY-CN adduct was found to be photoactive under reaction conditions, it is formed in concentrations that are sufficiently high (ca. 15 mM) to undergo a bimolecular reaction with 3 EY*. In agreement with this hypothesis, laser flash photolysis studies of DMF solutions of EY in the presence of EY-Me showed the formation of a transient species strongly resembling that of the semi-oxidized form of EY (EY •+ ), despite overlap with the bleaching of EY-Me, which partly absorbs the 532 nm excitation. EY-Me possesses a reversible reduction at E1/2(EY-Me/EY-Me •-) = -0.65 V vs SCE (Figure S9, Table S4) and we may expect that 3 EY* can undergo efficient oxidative PET to EY-Me (∆GPET = -10.6 Kcal/mol).

On the basis of the above observations, we propose a mechanism that reconciles the apparently contradictory results involving PET (Figure 2). In the presence of sulfonyl cyanides, EY undergoes cyanation to afford the EY-CN adduct and the corresponding sulfinate RSO2 -. The latter was shown by König and co-workers to react efficiently with EY •+ to generate the sulfonyl radical. 23 Therefore, we expect that 3 EY* undergoes oxidative PET with the EY-CN adduct, and that the ensuing EY •+ then oxidizes sulfinate into the sulfonyl radical II. Reversible addition of the latter onto the olefin affords a nucleophilic C-centered radical III, which may evolve through two different pathways: (1) a cyano group radical transfer to afford product V, 14 or (2) the oxidation of III into a carbocation IV, eventually trapped by a cyanide anion. In the latter case, EY •+ is reduced back to EY. The proposed mechanism also explains the excess of sulfonyl cyanides (1.5 equiv) needed to obtain optimal yields. Estimation of the oxidation potential of modelsulfonyl radicals III in DMF, through DFT calculations (SI), indicates that oxidation of III into IV is slightly exergonic (∆GET ~ -2 Kcal/mol), or favored with for more substituted olefins (IIIc, ∆GET = -14.1 Kcal/mol, SI). The absence of elimination products, alcohols or ethers, when water or iPrOH were used as co-solvents is however in sharp contrast with literature reports on radical-polar cross-over processes. 13,23,24 Our experimental evidence thus rules out the involvement of a cation such as IV as an intermediate and a back electron transfer (BET) from III to EY •+ cation-radical. Direct conversion of III into product V, through a cyano group transfer process, would then constitute a viable alternative pathway, as shown by the light ON/OFF experiment (Figure S4). Quantum yields for the formation of V measured in DMF and acetone upon monochromatic excitation at 546 nm led respectively to values of ΦDMF = 0.2 and ΦAcetone = 1.17 (SI). Considering the intersystem crossing efficiency of EY (ΦISC = 0.32 in methanol), 25 these values suggest that a moderately efficient radical chain is operating. In summary, we have shown that the photocatalyzed alkylsulfonyl-cyanation of a variety of olefins affords the corresponding β-sulfonyl nitriles in good yield. Combined with a safe protocol for the preparation of sulfonyl cyanides, this methodology provides a convenient access to β-sulfonyl nitriles, useful synthetic intermediates, as shown by the synthesis of a metalloproteinase inhibitor. We find that the reaction proceeds through a photoinduced electron transfer mechanism involving a cyanated derivative of EY formed in situ. This mechanism circumvents the energetically unfavored direct electron transfer from the excited EY triplet state to the alkylsulfonyl cyanide and instead relies on the oxidation of the sulfinate anion by the ground state oxidized EY .+ . 23a The present mechanistic studies provide an in-depth and more general picture of the unique reactivity of alkyl-and arylsulfonyl cyanides in the presence of eosin, 13 which adds to the direct ET or energy transfer mechanisms usually proposed in EY-mediated processes. Further work will be necessary to establish whether this mechanism is also present in other photocatalyzed transformations involving xanthene dyes.

Corresponding Author * yannick.landais@u-bordeaux.fr

Scheme 1 .

 1 Scheme 1. Sulfonyl cyanation of olefins.

Figure 1 .

 1 Figure 1. Proposed structure of the adduct formed between EY and RSO2CN (EY-CN) and electronic spectrum of EY in DMF (black curve, divided by 10) and of the O-methylated derivative (EY-Me, blue curve). The red curve shows the absorption spectrum of the EY-CN adduct obtained by the addition of 10 mM 1a to a 20 µM solution of EY. The exact concentration of the adduct is unknown.

Figure 2 .

 2 Figure 2. Proposed mechanism for EY-mediated sulfonyl-cyanation of olefins involving PET to an O-CN adduct of EY.

Table 1 .

 1 Optimization of the alkylsulfonyl-cyanation conditions.

	entry a	1a (equiv)	solvent	time/h	yield/% b
	1	2	DCE	24	53
	2	2	DCE	112	81
	3	2	DMF	20	98
	4	1.5	DMF	18	quant
	5	1	DMF	18	68
	6 c	1.5	DMF	20	86
	7 d	1.5	DMF	20	48
	8 e	1.5	DMF	20	quant
	9	1.5	acetone	19	94
	10	1.5	CH3CN	19	97
	11	1.5	iPrOH	23	86
	a Conditions: Eosin-Y (2 mol %), 1a (1.5-2.0 equiv), 2a (1 equiv), K2HPO4 (0.2 equiv), solvent (0.5 mL, [C] = 1 mol/L), blue
	LED, rt.

b Isolated yield of 3a after purification through silica gel. c Eosin-Y (10 mol %). d The reaction mixture was not degassed prior to irradiation. e 2a (1 mmol).