Gregor Gössler

Daniel Le Métayer

A General Framework for Blaming in Component-Based Systems

In component-based safety-critical embedded systems it is crucial to determine the cause(s) of the violation of a safety property, be it to issue a precise alert, to steer the system into a safe state, or to determine liability of component providers. In this paper we present an approach to blame components based on a single execution trace violating a safety property P. The diagnosis relies on counterfactual reasoning ("what would have been the outcome if component C had behaved correctly?") to distinguish component failures that actually contributed to the outcome from failures that had little or no impact on the violation of P.

Introduction

In a concurrent, possibly embedded and distributed system, it is often crucial to determine which component(s) caused an observed failure. Understanding causality relationships between component failures and the violation of system-level properties can be especially useful to understand the occurrence of errors in execution traces, to allocate responsibilities, or to try to prevent errors (by limiting error propagation or the potential damages caused by an error).

The notion of causality inherently relies on a form of counterfactual reasoning: basically the goal is to try to answer questions such as "would event e 2 have occurred if e 1 had not occurred?" to decide if e 1 can be seen as a cause of e 2 (assuming that e 1 and e 2 have both occurred, or could both occur in a given context). For instance, we may want to determine whether the violation of a safety requirement of a cruise control system was caused by an observed buffer overflow in component C 1 or by an observed timing failure of C 2 , or by the combination of both events. But this question is not as simple as it may look:

1. First, we have to define what could have happened if e 1 had not occurred, in other words what are the alternative worlds.

2. In general, the set of alternative worlds is not a singleton and it is possible that in some of these worlds e 2 would occur while in others e 2 would not occur.

3. We also have to make clear what we call an event and when two events in two different traces can be considered as similar. For example, if e 1 had not occurred, even if an event potentially corresponding to e 2 might have occurred, it would probably not have occurred at the same time as e 2 in the original sequence of events; it could also possibly have occurred in a slightly different way (for example with different parameters, because of the potential effect of the occurrence of e 1 on the value of some variables).

Causality has been studied in many disciplines (philosophy, mathematical logic, physics, law, etc.) and from different points of view. In this paper, we are interested in causality for the analysis of execution traces in order to establish the origin of a system-level failure. The main trend in the use of causality in computer science consists in mapping the abstract notion of event in the general definition of causality proposed by Halpern and Pearl in their seminal contribution [START_REF] Halpern | Causes and explanations: A structural-model approach. part I: Causes[END_REF] to properties of execution traces. Halpern and Pearl's model of causality relies on a counterfactual condition mitigated by subtle contingency properties to improve the accurateness of the definition and alleviate the limitations of the counterfactual reasoning in the occurrence of multiple causes. While Halpern and Pearl's model is a very precious contribution to the analysis of the notion of causality, we believe that a fundamentally different approach considering traces as first-class citizens is required in the computer science context considered here: The model proposed by Halpern and Pearl is based on an abstract notion of event defined in terms of propositional variables and causal models expressed as sets of equations between these variables. The equations define the basic causality dependencies between variables (such as F = L 1 or L 2 if F is a variable denoting the occurrence of a fire and L 1 and L 2 two lightning events that can cause the fire). In order to apply this model to execution traces, it is necessary to map the abstract notion of event onto properties of execution traces. But these properties and their causality dependencies are not given a priori, they should be derived from the system under study. In addition, a key feature of trace properties is the temporal ordering of events which is also intimately related to the idea of causality but is not an explicit notion in Halpern and Pearl's framework (even if notions of time can be encoded within events). Even though this application is not impossible, as shown by [START_REF] Beer | Explaining counterexamples using causality[END_REF], we believe that definitions in terms of execution traces are preferable because (a) in order to determine the responsibility of components for an observed outcome, component traces provide the relevant granularity, and (b) they can lead to more direct and operational definitions of causality.

As suggested above, many variants of causality have been proposed in the literature and used in different disciplines. It is questionable that one single definition of causality could fit all purposes. For example, when using causality relationships to establish liabilities, it may be useful to ask different questions, such as: "could event e 2 have occurred in some cases if e 1 had not occurred?" or "would event e 2 have occurred if e 1 had occurred but not e 1 ?". These questions correspond to different variants of causality which can be perfectly legitimate and useful in different situations. To address this need, we propose two definition of causality relationships that can express these kinds of variants, called necessary and sufficient causality.

The framework introduced here distinguishes a set of black-box components, each equipped with a specification. On a given execution trace, the causality of the components is analyzed with respect to the violation of a system-level property. In order to keep the definitions as simple as possible without losing generality -that is, applicability to various models of computation and communication -, we provide a language-based formalization of the framework. We believe that our general, trace-based definitions are unique features of our framework.

Traces can be obtained from an execution of the actual system, but also as counter-examples from testing or model-checking. For instance, we can model-check whether a behavioral model satisfies a property; causality on the counter-example can then be established against the component specifications.

This article extends the preliminary work of [START_REF] Gössler | A general trace-based framework of logical causality[END_REF]. In particular, we have entirely replaced the characterization of temporal causality with the notion of unaffected prefixes (Section 5.1), which precisely distinguishes dependencies between events in the component traces on the semantic level, and does not require the user to provide an information flow relation. In order to illustrate the instantiation of our general formalization with a specific model of computation, we apply the approach to a system whose components are specified in a simple synchronous language inspired by Lustre [START_REF] Halbwachs | The synchronous dataflow programming language lustre[END_REF].

The remainder of the article is organized as follows. In the next section we discuss some fundamental issues in defining causality, and define variants of causality. In Sections 3 and 4 we introduce our language-based modeling framework and a running example. In Section 5 we formalize necessary and sufficient causality and establish some fundamental properties. Section 6 shows how the framework can be instantiated to blame components in a data-flow model à la Lustre. Section 7 compares our approach with related work, and Section 8 concludes.

Setting the Stage: Variants of Causality

Causality is a powerful but also very subtle notion, with many variants and interpretations depending on the discipline, application domain and context of use. As an illustration, legal systems introduce distinctions between actual causes, factual causes, intervening causes, intervening efficient causes, remote causes, necessary causes, probable causes, unforeseeable causes, concurrent causes, etc. This complexity is inherent to the concept of causality itself because it relies on assumptions or analyses of hypothetical actions or courses of events. Before starting the presentation of our formal framework in the next section, we first provide in this section a high-level and informal outline of a range of options for the interpretation of causality in the context of computer science.

As mentioned in the Introduction, we are interested in causality as a criterion to identify the component responsible (in a technical sense) for a failure of the system, or, more generally, for the occurrence of a given event. We assume that the minimum amount of available information to conduct the causality analysis is a set L of logs L i containing the sequence of events observed for each component C i of the system, a specification S i for each component and a global property P such that ∧ i∈ [1,n] S i ⇒ P. The set of logs L is assumed to be faulty (i.e. not to be consistent with the required property P). The next sections show how these notions can be expressed formally in terms of signatures and traces.

In the same way as in civil law, two conditions have to be met to declare a component C i responsible for a given (undesired) event: its behavior1 must have been faulty and this fault must be the (or a) cause of the event. The first condition implies that a model of the expected (correct) behavior of the component must be available; we call this model the specification of the component in the sequel. The second condition naturally leads to another question: What would have been the course of events if C i had behaved correctly? But this question is very difficult to answer because it depends on many parameters that may be or may not be available for the analysis. A key parameter is the assumptions on the actual behaviors of the components C i . Depending on the context, different types of information can be available:

• In some cases, no information at all is available on any component, which requires a "black box" analysis.

• In other cases, the code of each component is available and the assumption can be made that this code is actually the code that has been executed to produce the log (which is not necessarily obvious). This leads to what is sometimes called "white box" analysis.

• In yet other cases, partial information may be available, for example the code of certain components, or assumptions on the sequences of events that can or cannot be produced by a component.

In the sequel, we use BH i to denote the assumption on the behavior of C i : for example BH i can be the model of the actual code in a white box analysis or the set of all potential behaviors in a black box analysis.

Another type of assumption that must be made explicit to reason about alternative behaviors2 , in order to answer the question above, concerns the consistency between individual logs, for example the fact that a message cannot be received by a component if it has not first been sent by another component. We call this assumption the behavioral model B in this paper.

Starting from this set of parameters, the general structure of a causality analysis can be pictured as follows:

Observed logs L i → Potential behaviors Bh i ↓ Hypothetical logs L i ← Hypothetical behaviors Bh i
The potential behaviors Bh i ∈ BH i are the behaviors of the components that are consistent with the observed logs L i ; the hypothetical behaviors Bh i ∈ BH i are modifications of behaviors Bh i in which certain erroneous behaviors3 are replaced by correct behaviors; and the hypothetical logs are the logs produced by the execution of the hypothetical components. The causality analysis consists in performing these three steps and then checking whether the hypothetical logs L i meet the property P 4 .

This high-level picture shows that the analysis goes from logs to behaviors and back to logs: it starts from logs, tries to infer the behaviors that can have produced these logs, considers variants of these behaviors and comes back to the logs corresponding to these hypothetical behaviors. Looking at it more closely, we can see that each step in the above figure actually gives rise to a range of options:

• The first step can be interpreted as a universal or an existential quantification. In other words, we may want to consider all behaviors consistent with the observed log or just require the existence of a behavior. Universal quantification leads to notions of "strong" causality and existential quantification to "weak causality" (or potential causality).

• In the second step, different choices are possible for the components whose behavior is modified: for example, if we are interested in the responsibility of a given component C i , we may replace the behavior of C i by a correct behavior or replace the behavior of all components but C i by a correct behavior. As explained below, these choices lead to two classes of causality called necessary and sufficient causality respectively.

• Just like the first step, the third step can be interpreted as a universal or an existential quantification: we may want to consider all hypothetical logs obtained from the hypothetical components or just consider the existence of hypothetical logs meeting (or not meeting) the property P. This choice has an impact on the treatment of non-determinism in the execution of the components.

The combination of the above choices leads to eight possible forms of causality which can be noted Necessary ∃,∃ , Necessary ∃,∀ , . . . , Sufficient ∃,∃ , Sufficient ∃,∀ , . . . . For example, Necessary ∀,∀ (for one component C i ) corresponds to the following informal definition:

Considering the evidence provided by the set of logs L, Component C i is a Necessary ∀,∀ cause for the failure of the system if for all potential behaviors Bh of the system consistent with L, all behaviors Bh similar to Bh except for the behavior of C i which is made correct, lead to correct execution logs.

The next sections provide a formal model of the intuitions introduced here. In the rest of this paper, we do not make any assumption on potential behaviors (black box analysis), we consider both necessary and sufficient causality, and focus on strong forms of causality.

Modeling Framework

In order to focus on the fundamental issues in defining causality on execution traces we introduce a simple, language-based modeling framework.

Definition 1 (Prefix , , ) A finite word w is a prefix of w, written w w, if there exists a word w such that w = w • w , where • stands for concatenation. Let denote the empty word. For two words w 1 and w 2 let w 1 w 2 be their longest common prefix. For a set P of prefixes of a given word let P and P denote the infimal and the supremal element of P with respect to , respectively.

A language L is upward-closed if (L, ) is a complete partial order, that is, if for any ascending chain of words w 1 w 2 ... in L, i w i ∈ L. Definition 2 (Component signature) A component signature C i is a tuple (Σ i , S i ) where Σ i is an alphabet of component actions and S i ⊆ Σ *
i is a prefix-closed and upward-closed language over Σ i called specification.

The component signature is the abstraction of an actual component. Σ i is the alphabet of actions the actual component may produce, whereas the alphabet actually used in S i may be a subset of Σ i . Prefix closure means that S i is a safety specification, while upward closure ensures the least upper bound of any ascending chain to be included in the specification.

Similarly, a system signature is the abstraction of a system composed of a set of interacting components.

Definition 3 (System signature) A system signature is a tuple (C, Σ, B) where

• C = {C 1 , ..., C n } is a finite set of component signatures C i = (Σ i , S i ) with pairwise disjoint alphabets; • Σ ⊆ Σ 1 × ... × Σ n is a system alphabet with Σ i = Σ i ∪ {∅}
where an interaction α = (a 1 , ..., a n ) ∈ Σ is a tuple of simultaneous actions, and

a i = ∅ means that component C i does not participate in α; • B ⊆ Σ * ∪ Σ ω is a prefix-closed and upward-closed behavioral model.
The behavioral model B is used to express assumptions and constraints on the possible (correct and incorrect) behaviors. For instance, in a model of components communicating by asynchronous message passing, B may be used to express the fact that a message cannot be received before it has been sent; in a real-time model it may be used to express the hypothesis that time progresses uniformly for all components.

Notations Given a word w

= α 1 • α 2 • • • ∈ Σ * and an index i ∈ N let w[1..i] = α 1 • • • α i and let w[i] = α i . For α = (a 1 , ..., a n ) ∈ Σ let α[k] = a k denote the action of component k in α (a k = ∅ if k does not participate in α); for w = α 1 • • • α k ∈ Σ * and i ∈ {1, ..., n} let π i (w) be the word obtained by removing all ∅ letters from α 1 [i] • • • α k [i].
For the sake of compactness of notations we define composition

: Σ * 1 × ... × Σ * n → Σ * such that w 1 ... w n = {w ∈ Σ * | ∀i = 1, ..., n : π i (w) = w i },
and extend to tuples of languages.

Logs

A (possibly faulty) execution of a system may not be fully observable; therefore we base our analysis on logs. A log of a system S = (C, Σ, B) with components C = {C 1 , ..., C n } of alphabets Σ i is a vector tr = (tr 1 , ..., tr n ) ∈ Σ * 1 ×...×Σ * n of component traces (i.e., words over the component alphabets) such that there exists a system-level trace (i.e., a word over the system alphabet) tr ∈ B with ∀i = 1, ..., n : tr i = π i (tr). A log tr is thus the projection of a system-level trace tr. This relation between an actual execution and the log on which causality analysis will be performed allows us to model the fact that only a partial order between the events (i.e., occurrences of component actions) in tr may be observable rather than their exact precedence 5 . Similarly, the component specifications may ignore part of the logged events. Let L(S) denote the set of logs of S. Given a log tr = (tr 1 , ..., tr n ) ∈ L(S) let tr ↑ = {tr ∈ B | ∀i = 1, ..., n : π i (tr) = tr i } be the set of behaviors resulting in tr.

Definition 4 (Consistent specification) A consistently specified system is a tuple (S, P) where S = (C, Σ, B) is a system signature with C = {C 1 , ..., C n } and C i = (Σ i , S i ), and P ⊆ B is a safety property such that for all traces tr ∈ B,

(∀i = 1, ..., n : π i (tr) ∈ S i ) =⇒ tr ∈ P
Under a consistent specification, property P may be violated only if at least one of the components violates its specification. Throughout this paper we focus on consistent specifications.

Motivating Example

Consider a database system consisting of three components communicating by message passing over point-to-point FIFO buffers. Component C 1 is a client, C 2 the database server, and C 3 is a journaling system. The specifications of the three components are as follows:

S 1 : sends a lock request lock to C 2 , followed by a request m to modify the locked data.

S 2 : receives a write request m, possibly preceded by a lock request lock. Access control is optimistic in the sense that the server accepts write requests without checking whether a lock request has been received before; however, in case of a missing lock request, a policy violation may be detected later on and signaled by an event x. After the write, a message journ is sent to C 3 .

S 3 : keeps receiving journ messages from C 2 for journaling, and acknowledges them with ok.

The system is modeled by the system signature (C, Σ, B) where and • Σ 1 = {a, m!, lock!}, Σ 2 = {m?, journ!, x, lock?, ok?}, and Σ 3 = {b, journ?, ok!}, where m! and m? stand for the emission and reception of a message m, respectively, and a, b, and x are internal actions; We are interested in the global safety property P = Σ * ok ∪ Σ ω ok with Σ ok = Σ \ {(∅, x, ∅)} modeling the absence of a conflict event x. It can be seen that if all three components satisfy their specifications, x will not occur.

C = {C 1 , C 2 , C 3 } with component signatures C i = (Σ i , S i ),
• S 1 = {lock! • m!} 6 , S 2 = {lock? • m? • journ! • ok?, m? • journ! • ok? • x}, and S 3 = {(journ? • ok!) i | i ∈ N}; • Σ = (Σ 1 ×{∅}×{∅})∪({∅}×Σ 2 ×{∅})∪({∅}×{∅}×Σ 3 ): component actions interleave; • B = w ∈ Σ * ∪Σ ω | ∀u ∈ Σ * ∀v : w = u•v =⇒ (
Figure 1 shows the log tr = (tr 1 , tr 2 , tr 3 ). In the log, tr 1 violates S 1 at event a and tr 3 violates S 3 at b. The dashed lines between m! and m?, and between journ! and journ? stand for communications. • C i is a necessary cause for the violation of P if in all executions where C i behaves correctly and all other components behave as observed, P is satisfied.

• Conversely, C i is a sufficient cause for the violation of P if in all executions where all incorrect traces of components other than C i are replaced with correct traces, and the remaining traces (i.e., correct traces and the trace of C i ) are as observed, P is still violated.

Applying these criteria to our example we obtain the following results: If C 1 had worked correctly, it would have produced the trace tr 1 = lock! . m!. This gives us the counterfactual scenario consisting of the traces tr = (tr 1 , tr 2 , tr 3 ). However, this scenario is not consistent as C 1 now emits lock, which is not received by C 2 in tr 2 . According to B, the FIFO buffers are not lossy, such that lock would have been received before m if it had been sent before m. By vacuity (as no execution yielding the traces tr exists), C 1 is a necessary cause and C 3 is a sufficient cause according to our definitions above. While the first result matches our intuition, the second result is not what we would expect. As far as C 2 is concerned, it is not a cause since its trace satisfies S 2 .

Why do the above definitions fail to capture causality? It turns out that our definition of counterfactual scenarios is too narrow, as we substitute the behavior of one component (e.g., tr 1 to analyze sufficient causality of C 3 ) without taking into account the impact of the new trace on the remainder of the system. When analyzing causality "by hand", one would try to evaluate the effect of the altered behavior of the first component on the other components. This is what we will formalize in the next section.

Causality Analysis

In this section we improve our definition of causality of component traces for the violation of a system-level property. We suppose the following inputs to be given:

• A system signature (C, Σ, B) with component signatures C i = (C i , Σ i ).
• A log tr = (tr 1 , ..., tr n ). In the case where the behavior of two or more components is logged into a common trace, the trace of each component can be obtained by projection.

• A safety property P ⊆ B such that (S, P) is consistently specified.

• A set I ⊆ {1, ..., n} of component indices, indicating the set of components to be jointly analyzed for causality. Being able to reason about group causality is useful, for instance, to determine liability of component providers that are responsible for more than one component.

Unaffected Prefixes

Intuitively, in order to verify whether the violations of S i by tr i , i ∈ I, are a cause for the violation of P in tr, we have to identify and remove the effect of these component failures on tr, replace it with behaviors that are consistent with a correct execution of the components in I, and verify whether all obtained counterfactual traces satisfy P. In order to determine and eliminate the impact of component failures on the traces of the remaining components, we compute the set of prefixes that are unaffected by the failures. This approach has the advantage of analyzing the propagation of failures on the semantic level, in contrast to the less precise approach of [START_REF] Gössler | A general trace-based framework of logical causality[END_REF] where the impact of component failures on other components is over-approximated using a worst-case information flow relation between component actions. be the set of component indices that are least constraining the set of symbols with which the words of L may be extended, where S is the greatest element of S with respect to set inclusion, or ∅ if no greatest element exists, and

ok(w, α) = w • α ∈ B ∧ i tr i π i (w) =⇒ π i (w • α) extend i (tr 0 i , tr i ) .
Thus, consistency is checked only over traces in B whose projections are either shorter than tr i , or prefixes of the extensions. Definition 8 (Unaffected prefixes UP) Given vectors tr of traces and S of specifications, and an index set I, we define the unaffected prefixes of tr as follows. Let

tr 1 i = cp(tr i , S i ) if i ∈ I tr i otherwise
and ∀i = 1, ..., n ∀j ≥ 1:

tr j+1 i = tr j i if i ∈ lcc( tr j , L j ) tr j i π i (w) | w ∈ L j otherwise (1)
where L j = sup{w ∈ B | ∀i ∃tr ∈ extend(tr i , tr j i ) : π i (w) tr }. Let UP S ( tr, I) = (tr * 1 , ..., tr * n ) with tr * i = j tr j i , i = 1, ..., n, be the vector of prefixes of tr that are unaffected by the failures of components in I.

Intuitively, the vector of unaffected prefixes is computed by first removing the incorrect suffixes from tr i , i ∈ I, and then computing, for each component i, a decreasing sequence of prefixes tr j i until a fixpoint is reached. In each iteration we trim, for the set of components whose current prefixes constrain the possible extensions, the prefix to the longest trace that is the projection of some word in L j (that is, on which all extended prefixes agree). The unaffected prefixes (tr * 1 , ..., tr * n ) to which the sequence converges, are the maximal prefixes that could also have been observed if all components in I had behaved correctly, whereas the suffixes (s 1 , ..., s n ) -such that tr i = tr * i .s i -are impacted by the failures of components in I. In the terminology of [START_REF] Gössler | A general trace-based framework of logical causality[END_REF], the suffixes (s 1 , ..., s n ) define the cone of influence spanned by the failures of components in I.

Counterfactuals

Using the unaffected prefixes defined above we are able to define, for a given log tr and set of component indices I, the set of counterfactual traces modeling alternative worlds in which the failures of components in I do not happen, and the unaffected prefixes of the remaining components are as observed in tr. The set of counterfactuals is the set of system-level traces whose projections on the components extend the unaffected prefixes with correct behaviors. Incorrect prefixes and prefixes that amount to the whole observed trace, are not extended.

The rationale behind Definition 9 is to compute the set of alternative worlds where the failures of components in I do not occur. To this end we have to prune out their possible impact on the logged behavior, and substitute with correct behaviors. Prefixes violating their specifications, and unaffected prefixes that are equal to the observed component traces, are not extended since we want to determine causes for system-level failures observed in the log, rather than exhibiting causality chains that are not complete yet and whose consequence would have shown only in the future.

Example 2 The set of counterfactuals C S ( tr, {client}) with respect to the failure of client in our running example is computed as follows (where we use the subscripts c, db, and j for client, database, and journal, respectively):

C S ( tr, {client}) = {w ∈ B | π c (w) ∈ extend c (tr c , ) ∧ π db (w) ∈ extend db (tr db , ) ∧ π j (w) ∈ extend j (tr j , b • journ? • ok!)} = {w ∈ B | π c (w) ∈ S c ∧ π db (w) ∈ S db ∧ π j (w) = b • journ? • ok!}
The projections of the counterfactual traces on the three components are shown in Figure 2a. Figure 2b shows the unique counterfactual scenario with respect to the failure of journal.

Logical Causality and Blaming

We are now ready to formally define two variants of causality in our framework, namely, necessary and sufficient causality.

Definition 10 (Necessary cause) Given

• a consistently specified system (S, P) with S = (C, Σ, B), C = {C 1 , ..., C n }, and

C i = (Σ i , S i ),
• a log tr ∈ L(S) such that tr ↑ ∩ P = ∅, and

• an index set I, the incorrect suffixes of the traces indexed by I are a necessary cause of the violation of P by tr if C S ( tr, I) ⊆ P That is, the set of logs indexed by I is a necessary cause for the violation of P if in the observed behavior where the unaffected prefixes are extended with correct behaviors, P is satisfied. In other words, if all components had behaved as in the unaffected prefixes, and the components in I had satisfied their specifications, then P would have been satisfied.

Example 3 Coming back to our running example, we have C S ( tr, {client}) ⊆ P. According to Definition 10, the failure of client is a necessary cause for the violation of P. Since the only element of C S ( tr, {journal}) violates P, the failure of journal is not a necessary cause for the violation of P.

The definition of sufficient causality is dual to necessary causality, where in the alternative worlds we remove the failures of components not in I and verify whether P is still violated.

Definition 11 (Sufficient cause) Given

• a consistently specified system (S, P) with S = (C, Σ, B), C = {C 1 , ..., C n }, and

C i = (Σ i , S i ),
• a log tr ∈ L(S) with tr ↑ ∩ P = ∅, and

• an index set I, let I = {1, ..., n} \ I. The set of traces indexed by I is a sufficient cause for the violation of P by tr if sup C S ( tr, I) ∩ P = ∅ That is, the set of logs indexed by I is a sufficient cause for the violation of P if in the observed behavior where the incorrect suffixes of the components in the complement of I is replaced with a correct behavior, the violation of P is inevitable (even though P may still be satisfied for non-maximal counterfactual traces). In other words, even if the components in the complement I of I had satisfied their specifications and no component had failed in the cone of influence spanned by the failures of I, then P would still have been violated.

In Definitions 10 and 11 the analysis of (in)dependence between component behaviorsrepresented by the unaffected prefixes -helps in constructing alternative scenarios in B where the components indexed by I (resp. I) behave correctly while keeping the behaviors of all other components close to their observed behaviors.

Example 4 In our database example we have sup C S ( tr, {journal}) ∩ P = ∅. By Definition 11, the failure of client is a sufficient cause for the violation of P since P is still violated in the counterfactual scenario. On the other hand, sup C S ( tr, {client}) ∩ P = ∅, thus the failure of journal is not a sufficient cause for the violation of P.

Properties

Necessary causality is a safety property whereas checking sufficient causality amounts to verifying a liveness property on the counterfactual language. The following results show that our analysis does not blame any set of innocent components, and that it finds a necessary and a sufficient cause for every system-level failure.

Theorem 1 (Soundness) Each cause contains an incorrect trace.

Proof 1 Consider a set I ⊆ {i | tr i ∈ S i } and a log tr = (tr 1 , ..., tr n ). We show that the set of traces indexed by I is not a necessary, nor sufficient cause for the violation of P in tr. If all components in I satisfy their specifications, then (tr * 1 , ..., tr * n ) = UP S ( tr, I) = tr. By the hypothesis of Definition 10 there exists tr ∈ B such that tr / ∈ P ∧ ∀i : π i (tr) = tr i = tr * i . Thus I is not a necessary cause according to Definition 10.

For sufficient causality, counterfactuals are computed by extending the unaffected prefixes tr * = UP S ( tr, I). If all components in I satisfy their specifications, then C S ( tr, I) ⊆ P since (S, P) is a consistently specified system. Moreover, since the unaffected prefixes allow by construction for a common system-level trace whose projections extend them, there exists a system-level trace tr ∈ B such that tr ∈ C S ( tr, I). Thus, I is not a sufficient cause according to Definition 11.

Theorem 2 (Completeness) Each violation of P has a necessary and a sufficient cause.

Proof 2 Let tr = (tr 1 , ..., tr n ) and I = {i | tr i / ∈ S i }. Due to the duality of necessary and sufficient causality, the proof of completeness for necessary (resp. sufficient) causality is similar to the proof of soundness for sufficient (resp. necessary) causality:

For necessary causality, the vector of unaffected prefixes is (tr * 1 , ..., tr * n ) = UP S ( tr, I). By construction of tr 0 -and thus of tr * -, all traces in tr * are prefixes of the traces in tr and satisfy the component specifications. Since (S, P) is consistently specified and hence, n i=1 S i satisfies P, and P is prefix-closed, all traces satisfying the condition of Definition 10 also satisfy P. Hence, I is a necessary cause for the violation of P in tr.

For sufficient causality, let tr * = UP S ( tr, I). By the choice of I, tr * = tr. We thus have C S ( tr, I) = tr ↑ , thus C S ( tr, I) ∩ P = ∅. It follows that I is a sufficient cause for the violation of P in tr.

Application to Synchronous Data Flow

In this section we use the general framework to model a synchronous data flow example. Consider a simple filter that propagates, at each clock tick, the input when it is stable in the sense that it has not changed since the last tick, and holds the output when the input is unstable. Using

Lustre [START_REF] Halbwachs | The synchronous dataflow programming language lustre[END_REF]-like syntax the filter can be written as follows:

change = false → in = pre(in) h = pre(out) out = in if ¬change h otherwise
That is, component change is initially false, and subsequently true if and only if the input in has changed between the last and the current tick. h latches the previous value of out; its value is ⊥ ("undefined") at the first instant. out is equal to the input if change is false, and equal to h otherwise. Thus, each signal consists of an infinite sequence of values, e.g., change = change 1 , change 2 , ... . Figure 3 visualizes the architecture and signal names. We formalize the system as follows.

• Σ ch = R × B × N where the first two components stand for the current value of the input to change and the output from change and the third component is the index of the clock tick. Similarly, let

Σ h = R × (R ∪ {⊥}) × N and Σ out = R 2 × B × R × N.
In particular, for component h the tuple only encompasses the input at the previous instant, which will allow us to log the values on which the specified current output depends.

• S ch = {(r 1 , r 2 , ...) ∈ Σ * ch | r i = (in i , change i , i) ∧ change 1 = false ∧ (i ≥ 2 =⇒ change i = in i-1 = in i )} is the specification of change. Similarly, S h = {(r 1 , r 2 , ...) ∈ Σ * h | r i = (out i-1 , h i , i) ∧ (i ≥ 2 =⇒ h i = out i-1 )} and S out = (r 1 , r 2 , ...) ∈ Σ * out | r i = (in i , h i , change i , out i , i) ∧ out i = in i if ¬change i h i otherwise • Σ = {(r ch , r h , r out ) ∈ Σ ch × Σ h × Σ out | r ch = (•, •, i 1 ) ∧ r h = (•, •, i 2 ) ∧ r out = (•, •, •, •, i 3 ) | i 1 = i 2 = i 3 }
is the system alphabet (where all components react synchronously).

• B = {(r 1 , r 2 , ...) ∈ Σ * ∪ Σ ω | ∀i : r i = (in ch i , change i , i 1 ), (out h i-1 , h i , i 2 ), (in out i , h out i , ch out i , out i , i 3 ) ∧ in ch i = in out i ∧ change i = ch out i ∧ out h i = out i ∧ h i = h out i }
is the set of possible behaviors, meaning that connected flows are equal.

in i 0 0 3 2 2 change: (in i , change i ) (0,false) (0,false) (3,true) (2,true) (2,false) h: (out i-1 , h i ) (⊥, ⊥) (0,0) (0,0) (3,0)
(2,0) out: (in i , change i , h i , out i ) (0,false,⊥,0) (0,false,0,0) (3,true,0,0) (2,true,0,0) (2,false,0,2) Figure 4: A correct log of the filter.

• P = {(r 1 , r 2 , ...) ∈ B | ∀i : r i = ..., (..., out i , ...) ∧ out i = out i+1 ∨ out i+1 = out i+2 } is the stability property, meaning that there are no two consecutive changes in output.

A log of a valid execution is shown in Figure 4 (where the tick number is omitted).

Figure 5a shows the logs of a faulty execution. Two components violate their specifications (incorrect values are underlined): change and h, both at the third instant. The stability property P is violated at the fourth output. Let us apply our definitions in order to analyze causality of each of the two faulty components.

• In order to check whether change is a necessary cause, we first compute the unaffected prefixes UP S ( tr, {change}) with respect to the violation by change, as shown in Figure 5b. Next we compute the set of counterfactuals, according to Definition 9, as ( tr ) ↑ , where tr is shown in Figure 5c. P is satisfied by the (unique) counterfactual trace, hence change is a necessary cause. We can show, using the same construction, that h is not a sufficient cause for the violation of P.

• In order to check whether change is a sufficient cause, we compute the unaffected prefixes UP S ( tr, {h}) with respect to the violation by h, as shown in Figure 5d. Due to change being (incorrectly) true, the only possible counterfactual trace according to Definition 9 is the one shown in Figure 5e. P is satisfied by the unique counterfactual trace, hence change is not a sufficient cause. We can show, using the same construction, that h is a necessary cause for the violation of P.

The log of Figure 5a shows a case of joint causation: both change and h are necessary causes for the violation of P in tr.

Related Work

Causality has been studied for a long time in different disciplines (philosophy, mathematical logic, physics, law, etc.) before receiving an increasing attention in computer science during the last decade. Hume discusses definitions of causality in [START_REF] Hume | An Enquiry Concerning Human Understanding[END_REF]: Suitably to this experience, therefore, we may define a cause to be an object, followed by another, and where all the objects similar to the first are followed by objects similar to the second. Or in other words where, if the first object had not been, the second never had existed.

In computer science, various approaches to causality analysis have been developed recently. They differ in their assumptions on what pieces of information are available for causality analysis: a model of causal dependencies, program code, a program as a black-box that can be used to replay different scenarios, the observed actual behavior (e.g. execution traces, or inputs and outputs), and/or the expected behavior (that is, component specifications). Existing frameworks consider different subsets of these entities. We cite the most significant settings and approaches for these settings. in 0 0 0 0 change (0,false) (0,false) (0,true) (0,true) h (⊥, ⊥) (0,0) (0,-1) (0,1) out (0,false,⊥,0) (0,false,0,0) (0,true,-1,-1) (0,true,1,1) A specification and an observation In [START_REF] Gössler | Causality analysis in contract violation[END_REF], causality of components for the violation of a system-level property under the BIP interaction model [START_REF] Gössler | Composition for component-based modeling[END_REF] has been defined using a rudimentary definition of counterfactuals where only faulty traces are substituted but not their effects on the traces of other components. This definition suffers from the conditions for causality being true by vacuity when no consistent counterfactuals exist. A slightly improved approach is used in [START_REF] Wang | A causality analysis framework for component-based real-time systems[END_REF] for blaming in real-time systems. A preliminary version of our formalization presented here is instantiated in [START_REF] Gössler | Blaming in component-based real-time systems[END_REF] to analyze necessary causality on real-time systems whose component specifications and expected system-level property are modeled as timed automata. With a similar aim of independence from a specific model of computation as in our work, [START_REF] Reiter | A theory of diagnosis from first principles[END_REF] formalizes a theory of diagnosis in first-order logic. A diagnosis for an observed incorrect behavior is essentially defined as a minimal set of components whose failure explains the observation.

A causal model [START_REF] Halpern | Causes and explanations: A structural-model approach. part I: Causes[END_REF] proposes what has become the most influential definition of causality for computer science so far, based on a model over a set of propositional variables partitioned into exogenous variables U and endogenous variables V. A function F X associated with each variable X ∈ V uniquely determines the value of X depending on the value of all variables in (U ∪ V) \ {X}. These functions define a set of structural equations relating the values of the variables. The equations are required to be recursive, that is, the dependencies form an acyclic graph whose nodes are the variables. The observed values of a set X of variables is an actual cause for an observed property ϕ if with different values of X, ϕ would not hold, and there exists a context (a contingency) in which the observed values of X entail ϕ. With the objective of better representing causality in processes evolving over time, CP-logic defines actual causation based on probability trees [START_REF] Beckers | Counterfactual dependency and actual causation in cp-logic and structural models: a comparison[END_REF].

In [START_REF] Jobstmann | Finding and fixing faults[END_REF], fault localization and repair in a circuit with respect to an LTL property are formulated as a game between the environment choosing inputs and the system choosing a fix for a faulty component.

A model or program and a trace In several applications of Halpern and Pearl's SEM, the model is used to encode and analyze one or more execution traces, rather than a behavioral model.

The definition of actual cause from [START_REF] Halpern | Causes and explanations: A structural-model approach. part I: Causes[END_REF] is used in [START_REF] Beer | Explaining counterexamples using causality[END_REF] to determine potential causes for the first violation of an LTL formula by a trace. As [START_REF] Halpern | Causes and explanations: A structural-model approach. part I: Causes[END_REF] only considers a propositional setting without any temporal connectors, the trace is modeled as a matrix of propositional variables. In order to make the approach feasible in practice, an over-approximation is proposed. In this approach, the structure of the LTL formula is used as a model to determine which events may have caused the violation of the property. Given a counter-example in model-checking, [START_REF] Groce | Error explanation with distance metrics[END_REF] uses a distance metric to determine a cause of the property violation as the difference between the error trace and a closest correct trace.

An approach to fault localization in a sequential circuit with respect to a safety specification in LTL is presented in [START_REF] Fey | Automatic fault localization for property checking[END_REF]: given a counter-example trace, a propositional formula is generated that holds if a different behavior of a subset of gates entails the satisfaction of the specification.

For a program and a set of observations that violate a specification, automatic error localization uses SMT to identify a minimal set of program statements that must be changed in order to satisfy the specification [START_REF] Jose | Cause clue clauses: error localization using maximum satisfiability[END_REF][START_REF] Könighofer | Automated error localization and correction for imperative programs[END_REF]. Different approaches for blaming based on contracts in sequential functional languages are discussed in [START_REF] Ch | Correct blame for contracts: no more scapegoating[END_REF].

A set of traces [START_REF] Kuntz | From probabilistic counterexamples via causality to fault trees[END_REF] extends the definition of actual causality of [START_REF] Halpern | Causes and explanations: A structural-model approach. part I: Causes[END_REF] to totally ordered sequences of events, and uses this definition to construct from a set of traces a fault tree. Using a probabilistic model, the fault tree is annotated with probabilities. The accuracy of the diagnostic depends on the number of traces used to construct the model. An approach for on-the-fly causality checking is presented in [START_REF] Leitner-Fischer | Causality checking for complex system models[END_REF].

An input and a black box Delta debugging [START_REF] Zeller | Why Programs Fail[END_REF] is an efficient technique for automatically isolating a cause of some error. Starting from a failing input and a passing input, delta debugging finds a pair of a failing and a passing input with minimal distance. The approach is syntactical and has been applied to program code, configuration files, and context switching in schedules. By applying delta debugging to program states represented as memory graphs, analysis has been further refined to program semantics. Delta debugging isolates failure-inducing causes in the input of a program, and thus requires the program to be available.

Conclusion

In this article we have developed a general framework for causality analysis of system failures. Applications include identification of faulty components in black-box testing, recovery of critical systems at runtime, and determination of the liability of component providers in the aftermath of a system failure.

For the sake of simplicity and generality we have provided a low-level formalization of blaming. The tagged signal model [START_REF] Lee | A framework for comparing models of computation[END_REF] may be used as a formal basis for representing specific models of communication in our approach. As analyzing necessary (resp. sufficient) causality amounts to verifying a safety (resp. liveness) property on the possibly infinite language C S ( tr, I), blaming is undecidable in general. In order to make the definitions of causality effectively verifiable and automatize the analysis, we will reformulate them as operations on symbolic models, and use efficient data structures such as the event structures used in [START_REF] Fabre | Distributed monitoring of concurrent and asynchronous systems[END_REF] for distributed diagnosis. Previous versions of our technique have been instantiated for a subset of the Bip component framework [START_REF] Gössler | A general trace-based framework of logical causality[END_REF] and networks of timed automata [START_REF] Gössler | Blaming in component-based real-time systems[END_REF], implemented in a prototype tool called LoCA (Logical Causality Analyzer), and tested on several case studies.

In closed-loop control systems, an alternative (counterfactual) behavior of the controller is likely to impact the physical process. For instance, when analyzing causality in a cruise control system, a counterfactual trace with different brake or throttle control will impact the speed of the car. Therefore the model of computation has to be expressive enough to include a faithful model of the physical environment in the system.

The presented approach is not a push-button solution for blaming. For instance, in the case of two component failures f 1 and f 2 where f 2 does not lie within the unaffected prefixes of f 1 , our framework lacks information to decide whether f 2 was entailed by f 1 , or occurred independently. Future work will refine the approach by taking additional available pieces of information into account. For example, in some situations such as post-mortem analysis the (black-box) components may be available, in which case counterfactual scenarios could be replayed on the system to evaluate their outcome more precisely.

Going a step further, we intend to investigate how to ensure accountability [START_REF] Küsters | Accountability: definition and relationship to verifiability[END_REF] by construction, that is, designing systems in such a way that, under some hypotheses, causes for system-level failures can be determined without ambiguity. To this end, the code of the components should be instrumented so as to log relevant information for analyzing causality with respect to a set of properties to be monitored. For instance, precise information on the actual (partial) order of execution can be preserved by tagging the logged events with vector clocks [START_REF] Fidge | Timestamps in message-passing systems that preserve the partial ordering[END_REF][START_REF] Mattern | Virtual time and global states of distributed systems[END_REF]. Whenever component failures are not observable, we have to use fault diagnosis [START_REF] Sampath | Diagnosability of discrete-event systems[END_REF] before performing causality analysis. Similar to the approach of [START_REF] Biswas | Transforming privacy policies to auditing specifications[END_REF] to derive logging requirements from a privacy policy that produce minimal but sufficient logs for auditing the policy, an interesting work direction will be to study how to automatically determine from the system signature, a minimal logging requirement for blaming.

Figure 1 :

 1 Figure 1: A scenario with three component logs.

Definition 5 (Definition 7 (

 57 Critical prefix cp) Given a trace tr = α 1 α 2 • • • over Σ and a language S over Σ, let cp(tr, S) = {tr | tr tr ∧ tr ∈ S} be the critical prefix of tr with respect to S. cp(tr, S) is the supremum of all prefixes of tr that satisfy S. Since by definition the component specifications S i are upward-closed, cp(tr, S) ∈ S. Definition 6 (Trace extension extend) Given a vector S of specifications, let extend i (tr 0 , tr) = {tr ∈ S i | tr tr } if tr = tr 0 ∧ tr ∈ S i {tr} otherwise The definition of trace extension plays a pivotal role in our definitions of causality. Before formalizing the notion of unaffected prefixes, we need the following auxiliary definition. Least constraining components lcc) Consider a language B over Σ and a log tr 0 . For a vector of traces tr over Σ, w ∈ Σ * , and α ∈ Σ let cons( tr, w, α) = i | π i (w • α) extend i (tr 0 i , tr i ) be the indices of components whose extension of tr i is consistent with w • α. Let lcc( tr, L) = {cons( tr, w, α) | w ∈ L ∧ α ∈ Σ ∧ ok(w, α)}

Example 1

 1 Coming back to the example of Section 4, the unaffected prefixes UP S ( tr, {client}) of the database example of Figure 1 with respect to client are ( , , b•journ?•ok!). The unaffected prefixes with respect to journal are UP S ( tr, {journal}) = (m!, m? • journ! • ok? • x, ).

Definition 9 (

 9 Counterfactuals C) Given vectors tr of traces and S of specifications, and an index set I, let C S ( tr, I) = {w ∈ B | ∀i : π i (w) ∈ extend i (tr i , tr * i )} where (tr * 1 , ..., tr * n ) = UP S ( tr, I), be the set of counterfactuals to tr.

  C S ( tr, {client}) C S ( tr, {journal})

Figure 2 :

 2 Figure 2: The counterfactual scenarios with respect to the failure of (a) and (b) journal. Extensions of the unaffected prefixes are blue.

Figure 3 :

 3 Figure 3: Architecture of the filter.

  false,⊥,0) (0,false,0,0) (b) UP S ( tr, {change}) false,⊥,0) (0,false,0,0) (0,false,-1,0) (0,false,0,0) (c) tr such that ( tr ) ↑ = C S ( tr, {change} true) (0,true) h (⊥, ⊥) (0,0) out (0,false,⊥,0) (0,false,0,0) (d) UP S ( tr, {h}) false,⊥,0) (0,false,0,0) (0,true,0,0) (0,true,0,0) (e) tr such that ( tr ) ↑ = C S ( tr, {h}

Figure 5 :

 5 Figure 5: Blaming in the scenario of joint causation.

  |u| m? ≤ |u| m! ∧|u| journ? ≤ |u| journ! ∧|u| lock? ≤ |u| lock! ∧ |u| ok? ≤ |u| ok! ∧ w respects lossless FIFO semantics) , where |u| a stands for the number of occurrences of a in w: communication buffers are point-to-point FIFO queues.

In the sequence of events leading to the undesired event.

We call alternative behaviors the other possible behaviors of the components in the counterfactual reasoning, which typically involves the replacement of the behavior of a component by a correct behavior.

Typically the behaviors of the components which are suspected of being the causes of the failure of the system.

In which case, causality will be established.

It is straight-forward to allow for additional information in traces tr ∈ B that is not observable in the log, by adding to the cartesian product of Σ another alphabet that does not appear in the projections. For instance, events may be recorded with some timing uncertainty rather than precise time stamps[START_REF] Wang | Runtime verification of traces under recording uncertainty[END_REF].

For the sake of readability we omit the prefix closure of the specifications in the examples.


Pierre Ceccaldi

Marta Marques

Vincent Fourmond

Inês Cardoso Pereira

Christophe Léger
email: christophe.leger@imm.cnrs.fr

Oxidative inactivation of NiFeSe hydrogenase †

NiFeSe hydrogenases differ from standard NiFe hydrogenases by the replacement of one Ni-bound cysteine with selenocysteine. We used direct electrochemistry to characterize the kinetics of (in)activation of Desulfovibrio vulgaris Hildenborough NiFeSe hydrogenase under various conditions. We conclude that two oxidized inactive forms of the enzyme reductively reactivate at a significant rate, one much faster than the other, at potentials above the H + /H 2 equilibrium potential. Both inactive states can be formed upon either aerobic or anaerobic oxidation, in a "CE" mechanism. We propose a resolution to the paradox that, in contrast with standard NiFe hydrogenases, spectroscopic studies of NiFeSe hydrogenase have not revealed any major signal attributable to Ni(III) states formed upon reaction with O 2 , despite the fact that two inactive states are formed under oxidizing conditions.

The enzymes that can reversibly oxidize and produce H 2 use inorganic active sites that contain either Fe, or Ni and Fe 1,2 . In the latter case, the two metal ions are bridged and attached to the protein by the sulfur atoms of two cysteine residues, and the Ni is also coordinated by either two additional cysteine residues, or, in the so-called NiFeSe hydrogenases, by one cysteine and one selenocysteine. 3 Selenium is more acidic and more nucleophilic than sulfur, but it is not clear how this gives selenoproteins particular properties.

All NiFe hydrogenases inactivate under oxidizing conditions. Oxidizing a standard NiFe hydrogenase produces the so-called Ni-A and Ni-B inactive states, which can be reactivated by reduction, the former more slowly than the latter. Both states are EPR-active Fe II Ni III , and one-electron more oxidized than the most oxidized catalytic intermediate, called Ni-Si. There is a consensus about the Ni bearing a hydroxo ligand in the Ni-B state, but the structure of Ni-A is debated. 4,5 The situation is even less clear regarding NiFeSe hydrogenases. These enzymes were once believed to be O 2 resistant because aerobically-prepared samples are essentially EPR-silent and appeared to be active with no lag (in the case of NiFe hydrogenases, a lag phase reveals reductive activation over the course of the assay). However, Armstrong and coworkers use electrochemistry experiments to establish that O 2 fully inhibits Desulfomicrobium baculatum (Dbm) NiFeSe hydrogenase, to form two states which are distinguished by the potential at which they undergo rapid reactivation. 6 The recent finding that the enzyme from Dbm is 6-times more active after anaerobic purification than when it has been exposed to air 7 is further evidence that NiFeSe hydrogenases are actually inhibited by O 2 . In addition, crystallographic studies of Dbm and Desulfovibrio vulgaris Hildenborough (DvH) NiFeSe hydrogenases showed the presence of oxidative modifications both to the active site and to the proximal cluster for the oxidized enzyme purified and crystallized aerobically. [7][8][9] Crystallography also revealed multiple conformations and redox states of the (seleno)cystein residues. FTIR was also used to investigate the transformations of the active site of NiFeSe hydrogenases, with the complication that two conformations of each redox state are detected. 10,11 Of the four catalytic intermediates of standard NiFe hydrogenases (Ni-Si, Ni-C, Ni-L and Ni-R) 1,2 , only Ni-C and Ni-R have been observed in the seleno-enzyme from DvH. Two oxidized inactive states, Ni-IS and Ni-Ox, are stable in air, EPR-silent, and disappear upon reduction: the former was observed after aerobic purification; the latter was obtained by reductive activation followed by exposure to air. 11 Using either microbes or enzymes to produce H 2 in the presence of O 2 is a challenge. In this context, it has been emphasized that NiFeSe hydrogenases, 6 but also standard NiFe hydrogenases, 12 sustain partial activity for H 2 production in the presence of small amounts of O 2 , but only the former appears to resist long exposure to O 2 . 12 This must be related to differences in the kinetics of (an)aerobic (in)activation, which we characterize in this work.

We carried out electrochemical experiments with a soluble recombinant form of the NiFeSe hydrogenase from DvH, covalently attached 13 to a pyrolytic graphite edge rotating disc electrode. The cell solution was saturated with H 2 , in a glovebox filled with N 2 , and the enzyme-electrode was rotated quickly to minimize substrate depletion near the electrode surface. The catalytic H 2 oxidation is proportional to turnover The (in)activation can also be detected in voltammetric experiments, where the electrode potential is swept upward and downward. Figure 2 shows four cyclic voltammograms (CVs) recorded at a slow scan rate (ranging from 0.3 to 5 mV/s), at 50 • C, pH 7, under one atm. of H 2 . The arrows indicate the directions of the sweeps. On the sweep upward, the H 2 oxidation current increases as a result of the competition between the increase in turnover rate of the active enzyme and the anaerobic inactivation, which decreases the amount of active enzyme. As the potential is reversed, the current decreases (the driving force decreases and the enzyme keeps inactivating), until the potential becomes lower than about 0V and the enzyme starts reactivating. The downward trace has a complex shape, with two current peaks (around 0 and -350mV at low scan rate) which result from the reactivation of two different inactive species. 6 The lower the scan rate, the more pronounced the hysteresis. Panel B shows the 1st-order derivatives of the return scans, to emphasize that the positions of the inflexion points on the return scans (the "switch potentials" 15 where the reactivations suddenly occur) shift to lower potential as the scan rate increases, as observed with all hydrogenases. 16,[START_REF] Hamdan | Proc. Nat. Acad. Sc[END_REF] This occurs because the rate of reactivation increases as the potential decreases (see e.g. fig 1C), and reactivation significantly proceeds when the reactivation becomes faster than the scan rate ν (more rigorously, faster than νF/RT , so that the units match). Therefore, the faster the scan rate, the lower the potential where reactivation occurs. It is actually possible to deduce the rate of reactivation at each inflexion point using the following relation: k a (at the inflexion point) = Fν/RT . [START_REF] Hamdan | Proc. Nat. Acad. Sc[END_REF] Since the position of the inflexion points is defined by the kinetics of the reactivation of each species, 16,[START_REF] Hamdan | Proc. Nat. Acad. Sc[END_REF] we refer to the two inactive states as "fast" and "slow" hereafter, to imply that one inactive species reactivates more quickly than the other. Figure 1C shows that the slow (low potential) process (triangles) corresponds to the reactivation that we have characterized above by performing CA experiments (fig 1); the "fast" inactive species was not detected in these experiments because a potential greater than about 100mV vs SHE is required to trigger its formation. 4 The sharp decrease in current observed at about 0V, on the downward scan recorded at 0.3mV/s in Fig 2 (red trace) suggests that the enzyme inactivates as the potential is made more negative, which is surprising considering that hydrogenases inactivate under oxidizing conditions. The chronoamperometry experiments in figure 3 demonstrate that indeed, the enzyme reactivates in an unprecedented manner when the potential is taken down. The experiments plotted in red and black were carried out under atmospheres of 10 and 100% H 2 , respectively. In both experiments, we start from a low potential, where the enzyme is fully active. We step the potential at a very high value (0.34V, panel A), where the enzyme inactivates in a 1st order process (hence the exponential decrease in current against time, visible as a straight line in the log-lin plot in panel B). On the downward step at -0.06V (at t = 400s), we observe first an increase then a decrease in current (after t = 420s) that cannot result from film loss. 18 Therefore, during the step at -60mV, the enzyme activates and then inactivates. The control experiment in fig S2 † shows that the maximal fraction of active enzyme at -60mV is about 10%. Complete reactivation is observed after the potential is stepped to its initial value (cf the dashed horizontal lines). We illustrate this totally unprecedented sequence of events using the ternary the case of the Ni-B state of NiFe hydrogenase [15][16][START_REF] Hamdan | Proc. Nat. Acad. Sc[END_REF] and the two inactive states of FeFe hydrogenase. [START_REF] Fourmond | [END_REF] )

At this point, it is not clear if the inactive species that are formed on the time scale of the electrochemical experiments correspond to any of those that have been crystallized before, since the aerobic crystallization process involves long term exposure to oxidizing conditions. Two reversible modifications are detected in the structures: the oxidation of the proximal cluster and the binding of an exogenous S at the active site.

The lack of any EPR signal arising from an inactive state more oxidized than the most oxidized catalytic intermediate has been bewildering. To resolve this paradox, we note the following: the fact that the enzyme inactivates under oxidative conditions does not imply that the "E" reaction following the "C" chemical step is an oxidation (as indeed occurs in NiFe and FeFe hydrogenases); it merely implies that the inactive species exists in two different redox states, and only the reduced form activates at a significant rate. We show in fig 4 how the inactive form(s) may be connected to the catalytic intermediates in the case of NiFe (left) and NiFeSe hydrogenase (right). This alternative had actually been considered in a paper of Limoges and Savant (scheme 3 in ref 20), in the very first attempt at modelling the hysteresis in the voltammetry of NiFe hydrogenase, but not ever since, and not in any paper about NiFeSe hydrogenase.

Surprisingly, the experiments in fig 3 show that the rate of oxidative inactivation at high potential increases when the concentration of H 2 increases. The effect is also clear in the experiments shown in fig S4, † where we observe that increasing the concentration of H 2 while the enzyme is inactivating at high potential causes an increase of both the current and the rate of inactivation. The opposite trend is observed for the Ni-B state of standard hydrogenases, where H 2 binding to the catalytically competent, oxidized, Ni-Si state competes with the formation of the Ni-B state. [START_REF] Hamdan | Proc. Nat. Acad. Sc[END_REF] Regarding NiFeSe hydrogenase, we therefore propose that the high potential inactivation is related to H 2 binding. This is reminiscent of the behavior of FeFe hydrogenases, where inactive species are formed under oxidizing anaerobic conditions as a result of the nonproductive binding of hydrogen to the active site H-cluster. [START_REF] Fourmond | [END_REF] This observation is certainly a clue to design experiments that will help understand the structures of the inactive states of NiFeSe hydrogenase, and the how the replacement of sulfur by selenium gives the enzyme its peculiar kinetic properties.

1- 4

 4 | 1 rate and electroactive coverage; the latter cannot be measured, but the grafting procedure makes the film very stable.That DvH NiFeSe hydrogenase reversibly inactivates under anaerobic, oxidizing conditions is clear from the experiment in fig1where we show the change in turnover rate (panel B) resulting from the sequence of potential steps shown in panel A. Each step up results in a slow decrease in activity, on the time scale of hundreds of seconds, which reveals an inactivation; a step down reactivates the sample. The process is fully reversible, judging from the values of the current at t = 0 and t = 1500s (horizontal dashed line), and each current relaxation is fairly mono-exponential: this suggests that, under these conditions, the inactivation results from the reversible formation of a single inactive state (however, see below). We used the same model as in ref14 (section 2-3 therein) and the open-source program that we recently released (www.qsoas.org) to analyse the chronoamperometric data and to measure k i and k a , the 1st order rate constants of inactivation and reactivation. As an example, the red line in fig is the best fit of a model that assumes that a single inactive species is formed, adjusting 8 parameters: the 3 values of the current of the fully active enzyme at each of the three potentials, and the values of k i and k a at each potential (forcing k i = 0 at the lowest potential). We ran and analyzed a number of experiments such as that in fig 1AB, changing the values of the potential steps, to measure the dependence on E of k i and k a . The results are shown as empty symbols in fig 1C. The value of k a decreases exponentially as E increases whereas k i is independent of potential.

Fig. 1

 1 Fig. 1 Oxidative anaerobic inactivation of DvH NiFeSe hydrogenase detected in chronoamperometry (CA) experiments. A. Electrode potential against time. B. Resulting H 2 oxidation current, after baseline subtraction (black). The red line is a fit of a model 14 that assumes that a single inactive species is formed. The best parameters were: k i = 0, 4.26 ± 0.03 10 -3 s -1 , 5.66 ± 0.01 10 -3 s -1 ; k a = 1.3 ± 0.01 10 1 s -1 , 1.67 ± 0.01 10 -2 s -1 , 1.31 ± 0.01 10 -3 s -1 at -360, -260, 110 mV vs SHE, respectively. C. Activation (empty squares) and inactivation (empty circles) rate constants against electrode potential, deduced from the analysis of a series of CA experiments. The filled symbols are the rate constants of reactivation deduced from fig 2B.

  Using this equation and the data in fig 2, we determined the dependence on potential of the rate constants of reactivation of the two different inactive species. The result is shown using a series of triangles and stars in fig 1C, each pair of data points being deduced from a single CV in fig 2.

Fig. 2 Figure 2

 22 Fig. 2 Figure 2 Oxidative anaerobic inactivation of DvH NiFeSe hydrogenase detected in voltammetric experiments. Panel B shows the 1st order derivative of the return scans shown in panel A (the local maxima mark the "switch potentials". pH 7.0, 1 bar H 2 , T = 50 • C, 3.5 krpm.

Fig. 3

 3 Fig. 3 Transient reactivation after inactivation at 340 mV/SHE. Panel A. Electrode potential as function of time. panel B. Resulting catalytic current (after subtraction of the capacitive current) under 100% (black line) or 10% (red line) H 2 . At t = 400s, transient reactivation occurs before the enzyme inactivates again. pH 7, T=50 • C, 3.5 krpm

  diagrams in fig S3. † Combining the results in fig 1C and the observation that the rate of inactivation at very high potential is independent on potential (fig S2A in ref 6), we conclude that both inactive species are reversibly formed, under oxidizing conditions, in a two-step, CE mechanism: a chemical step, C, limits the rate of inactivation, whereas the reactivation is triggered by a reduction, E. The reactivation proceeds along the reverse sequence: reduction followed by chemical transformation. (This is also 1-4 | 3

Fig. 4

 4 Fig. 4 Oxidative inactivation can result from the formation of a species that is either more oxidized (panel A, standard NiFe Hase) or as oxidized (panel B, NiFeSe Hase) than Ni-Si, the oxidized catalytic intermediate that undergoes inactivation. Horizontal arrows depict chemical steps, vertical arrows are redox transformations, the more oxidized species being on top. A single pair of inactive species is shown in each case. The Ni-L intermediate 2 is not shown here.


D Foerster

On an "interaction by moments" property of four center integrals

The four center integrals needed in the Hartree Fock approximation and in TDDFT linear response are known to be difficult to calculate for orbitals of the Slater type or of finite range. We show that the interaction of pairs of products that do not mutually intersect may be replaced by the interaction of their moments, of which there are O(N). Only quadruplets of orbitals 'close' to one another need an explicit calculation and the total calculational effort therefore scales as O(N). We provide a new and concise proof of this "interaction by moments" property.

Motivation

This note is motivated by the occurrence of four center integrals in the TDDFT linear response equation [1], [START_REF] Casida | Recent Advances in Density Functional theory[END_REF] χ = δρ(r, t) δVext(r ′ , t ′ ) = 1

χ -1 KS -δ(t-t ′ ) |r-r ′ | + δVxc(r,t) δρ(r ′ t ′ ) (1)
where χ KS = δρ δV KS and χ = δρ δVext are the free and interacting density response, where ρ denotes the electronic density and where Vext is an external potential acting on the electrons. In a basis of local orbitals {f a (r)}, the electronic density ρ and the external potential Vext may be expanded in terms of products of such orbitals according to

ρ = a,b f a * f b ρ ab , V ab ext = drVextf a * f b (2)
Equation ( 1) then turns into a matrix equation for the response χ ab,cd = δρ ab δV cd of ρ ab (t) with respect to variations of V cd ext (t ′ ) and this equation then contains the Coulomb interaction between products of orbitals or 'four center integrals'

< 12| 1 r |34 >= drdr ′ f 1 * (r)f 2 (r) 1 |r -r ′ | f 3 * (r ′ )f 4 (r ′ ) (3)
A technique for calculating these quantities in terms of two center integrals was developed in [START_REF] Talman | [END_REF]. In an alternative "resolution of identity" method, products of orbitals are replaced by auxiliary functions, see [4], [5].

For orbitals of finite range, there are, for N atoms, O(N 2 ) pairs ( 12), (34) of individually intersecting orbitals suggesting the need of O(N 2 ) distinct calculations. Here we show that only the subset of < 12| 1 r |34 > where a pair (1, 2) intersects with a pair [START_REF] Talman | [END_REF]4) must be calculated explicitly, while the remaining ones can be taken into account by their multipolar interactions. Since there are only O(N ) such quadruplets of orbitals and because the effort of calculating the moments scales like N , the cost of calculating four center integrals then scales as O(N ).

The present note arose in an ongoing effort to implement linear response for extended molecular systems, an effort prompted by recent work [7]. We prove and exploit an observation of Greengard on the exact character of the "interaction by moments". This observation was rederived previously in the literature [6] and its consequence has recently been absorbed in a corresponding computer code [8], but our concise and simple deduction of this important property may still be of interest.

Reduction from four centers to two centers

We first need a reduction of products of orbitals to a set of single center functions. Following the discussion of [START_REF] Talman | [END_REF] we obtain an expansion in spherical harmonics of a translated function f ( -→ r --→ a ) by using its momentum representation We use spherical Bessel functions j l (x) with l integer, that are related to conventional Bessel functions for half integers by j l (x) = π 2x J l+ 1 2 (x). In practice, fast Hankel transform routines [9] are needed to speed up the calculation.

ψ lm ( - → r -- → a ) = d 3 p (2π) 3/2 ψ lm ( - → p )e -ip(r-a) (4)
ψ lm ( - → p ) = i l ψ l (p)Y lm ( - → p ), ψ l (p) = 2 π ∞ 0 r 2 ψ l (r)j l (pr)dr
Expanding e i - → p • - → r in spherical waves, one finds ψ lm ( - → r -- → a ) = l 1 m 1 Y l 1 m 1 ( - → r )G l 1 m 1 (r) (5)
where the coefficients G l 1 m 1 (r) that multiply the spherical harmonics Y l 1 m 1 ( -→ r ) now depend on both quantum numbers l1 and m1 because spherical symmetry is lost. One has the following expression for G l 1 m 1 (r)

G l 1 m 1 (r) = 2 √ 8π l 2 F l l 1 l 2 (r)Y * l 2 ,m 1 -m ( - → a )(-) l 1 (-) 1 2 (l 2 +l 1 +l) G lm,l 1 m 1 l 2 m 1 -m (6)
F l l 1 ,l 2 (r) = ∞ 0 j l 1 (pr) ψ l (p)j l 2 (pa)p 2 dp
where G l 1 m 1 ,l 2 m 2 l 3 m 3 are Gaunt coefficients for the overlap of three spherical harmonics. To bring this approach into perspective, it is interesting to consider an orbital with a cusp singularity such as e -r and to study the convergence of the translated orbital towards a translated cusp with increasing angular momentum cutoff jmax, see the figure . The figure shows that a fairly large number of angular harmonics is required for the representation of orbitals having such a cusp. By applying translations to two overlapping orbitals we may obtain an expansion of their product about a common midpoint

ψ l 1 m 1 ( - → r -- → a 1)ψ l 2 m 2 ( - → r -- → a 2) = l=0..lmax, m=-l..l G lm (r)Y lm ( - → r ) (7)
Using such expressions we can compute the Coulomb interaction of two pairs of mutually overlapping orbitals from the point of view of their associated effective centers.

Exact interaction by moments of non intersecting centers

We have seen that pairs of orbitals may be replaced by effective centers. Now we wish to show that the interaction between effective centers may be simplified when their spheres of support no longer intersect. We begin by quoting formulas for the computation of two center integrals in Fourier space, see [START_REF] Talman | [END_REF], [10]

< 1| 1 r |2 >= ψ * l 1 m 1 (r1) 1 |r1 -r2| ψ l 2 m 2 (r2)d 3 r1d 3 r2 = 4π ψ * l 1 m 1 ( - → p ) 1 p 2 ψ l 2 m 2 ( - → p )e i - → p • - → R d 3 p
where we used that

ψ * l 1 m 1 (r1) 1 |r1 -r2| ψ l 2 m 2 (r2)d 3 r1d 3 r2 = lm Y lm ( - → R )C l 1 m 1 ,l 2 m 2 lm (R) (8)
with

C l 1 m 1 ,l 2 m 2 lm (R) = C l 1 l 2 l (R)G l 1 m 1 ,l 2 m 2 ,lm (9)
C l 1 l 2 l (R) = (4π) 2 (-) 1 2 (l+l 2 -l 1 ) ∞ 0 ψ * l 1 (p) ψ l 2 (p)j l (pR)d
where G l 1 m 1 ,l 2 m 2 ,lm are the previously encountered Gaunt coefficients and C l 1 l 2 l (R) are Wigner-Eckart like couplings, see [START_REF] Talman | [END_REF], [10] for details of the derivation. We use eq(4) to rewrite the C l 1 ,l 2 ,l (R) in terms of the original radial wave functions as follows:

C l 1 ,l 2 ,l = 32π(-) l+l 2 -l 1 2 dr1dr2r 2 1 ψ * l 1 (r1)r 2 2 ψ l 2 (r) ∞ 0 j l 1 (pr1)j l 2 (pr2)j l (pR)dp (10)
The "interaction by moments" property we are after is contained in the following integral of Bessel functions

I l 1 ,l 2 ,l (r1, r2, R) = ∞ 0 j l 1 (pr1)j l 2 (pr2)j l (pR)dp (11)
The Coulomb interaction coefficients C l 1 ,l 2 ,l would reduce to I l 1 ,l 2 ,l (r1, r2, R) if the original orbitals functions were concentrated at, respectively, radii r1 and r2. This integral therefore represents the Coulomb interaction of two charged hollow shells of radii r1, r2 at a distance of R, and with the charge densities having the appropriate multipolar angular dependences. For R > r1 + r2 where these shells no longer intersect, we expect their interaction to simplify. Because of the Gaunt coefficients in eq (9) we only need this interaction for even values of l1 + l2 + l and where a triangle inequality |l1 -l2| ≤ l ≤ l1 + l2 holds. In this case the integrand associated with the dp integration in eq (10) is symmetric as a function of p and we may therefore extend the domain of integration to the entire p axis:

I l 1 ,l 2 ,l (r1, r2, R) = 1 2 ∞ -∞ j l 1 (r1p)j l 2 (r2p)j l (Rp)dp for l1 + l2 + l even
It is convenient to use j l (z) = Re h l (z) and to consider a corresponding complex integral

I c l 1 ,l 2 ,l with I l 1 ,l 2 ,l = Re I c l 1 ,l 2 ,l
that involves the Hankel function h l (z) :

I c l 1 ,l 2 ,l (r1, r2, R) = 1 2 ∞ -∞ j l 1 (r1p)j l 2 (r2p)h l (Rp)dp, (12)
For R > r1 + r2 the contour of integration in I c l 1 ,l 2 ,l (r1, r2, R) can be be closed at infinity in view of the relation

hn(p) = (-) n p n d pdp n -ie ip p (13)
Clearly, the exponential factor e iRp from j l (Rp) dominates, for R > r1 + r2, the factors e ±ipr 1 e ±ipr 2 that arise in the integrand in eq(12) from the product jn 1 (r1p)jn 2 (r2p). Since the integrand in I c l 1 ,l 2 ,l is analytic, except for possible singularities at p = 0 and since the contour of integration can be closed in the upper half plane, a non zero contribution to I c l 1 ,l 2 ,l can only be due to a residue at p = 0. From eq(13) the most singular term in h l (Rp) at p = 0 is

h l (Rp) = -i(2l -1)!! e iRp (Rp) l+1 + O(p -l ) Because of j l 1 (r1p) ∼ (r 1 p) l 1
(2l 1 +1)!! and an analogous relation for j l 2 (r2p) a non zero residue is impossible in eq(12) unless l attains the maximal value permitted by the triangle inequality, l = l1 + l2. When setting l = l1 + l2 and closing the contour of integration in eq(12) at infinity, there is a term ∼ 1/p that provides a non zero result by elementary contour integration. Rewriting the result in terms of conventional Γ functions, one then finds, for l + l1 + l2 even and with 0 ≤ l ≤ l1 + l2, the following simple result

I l 1 ,l 2 ,l (r1, r2, R) = δ l,l 1 +l 2 π 3/2 8 r l 1 1 r l 2 2 R l+1 Γ(l + 1/2) Γ(l1 + 3/2)Γ(l2 + 3/2) ( 14
)
Applied to the Coulomb interaction coefficients of eq (10) one concludes

C l 1 ,l 2 ,l = (-) l+l 2 -l 1 2 π 1/2 2 l 1 +l 2 -l+2 ρ * l 1 ρ l 2 R l+1 Γ(l + 1/2) Γ(l2 + 3/2)Γ(l1 + 3/2) δ l,l 1 +l 2 (15) ρ l 1,2 = 4π r 1,2 0 drr 2+l 1,2 ψ l 1,2 (r) for R ≥ r1 + r2
This last equation shows very clearly that non overlapping orbitals interact exactly via their moments, as shown first by Greengard [START_REF] Greengard | The rapid evaluation of potential fields in particle systems[END_REF]. For another proof, see [6].

Conclusion

We conclude that only the subset of four center integrals < 12| 1 r |34 > of "close" pairs where (1, 2) intersects (3, 4) must be calculated explicitly. Because there are only O(N ) such pairs of orbitals for a system of N atoms and because the multipoles are associated with only O(N ) products, the calculational effort scales as O(N ).

The conclusion that Coulomb integrals should be divided into far and near field ones has already been incorporated in a quantum chemistry code [8]. But our derivation of the "interaction by moments property" of four center integrals from a plain integral of a product of three spherical Bessel functions is the simplest and most concise proof of this property that is available.

Figure 1 :

 1 Figure 1: convergence towards a cusp with j max

1 |r 1

 11 -r 2 | = -4π △ , △ being the Laplace operator. Expanding e i - → p • -→ r in spherical waves one finds

Acknowledgements

It is a pleasure to thank James Talman from the University of Western Ontario, Canada, for continued correspondence and for kindly providing a computer code of his Hankel transform algorithm.

Useful comments by Xavier Blase (Lyon), Daniel Sanchez (San Sebastian) and Andrei Postnikov (Metz) and discussions with the quantum chemistry group of Ross Brown(Pau) and Isabelle Baraille (Pau) are gratefully acknowledged.

Figure caption: Translation away from the origin of e -r by one unit, with j ≤ jmax = 4, 6, 8, 10 and the convergence of the result towards a cusp with increasing angular momentum cutoff jmax.