1 Self-explaining Digital Systems
7
simply disregarded. Technically, the reference to prior events directly refers to their
explanations. Note that there may be multiple justifications for the same action, e.g.,
the light may be turned off because there is sufficient ambient light or because the
battery is low. We require such ambiguities to be resolved during run time based
on the actual implementation of the system. Only for simplicity this formalization
precludes the dependence of an event on multiple previous events executing the
same action.
Lewis [19] requires for counterfactual dependence of an event e on its cause
c that c → e and ¬c → ¬e. However, an event is identified with precisely the
actual occurrence of this event. There may be alternative ways to cause a similar
event, but the actual event e was precisely due to the cause c. Consider the event
that “the window was broken by a stone thrown by Joe.” The window may have
alternatively been broken by a ball thrown by Joe, but this would have been a
different “window broken” event. Lewis achieves this precision by associating the
actual event e with a proposition O(e) that is true iff e occurs and false otherwise.
These propositions allow to abstract from the imprecise natural language. Here we
achieve this precision by adding tags to actions.
Lewis [19] defines causation as a transitive relationship where the cause of an
event is an event itself that has its own causes. Similarly, we traverse the cause–effect
chain of events to identify root causes for some observable action as formalized in
the following.
Definition 1.1 For an explanation e = (a, t, R, A, T ), the immediate set of
explanations is given by
E(e) =
e
= (a
, t
, R
, A
, T
) ∈ E|a
∈ A and t
= T i(a )
Definition 1.2 The full set of explanations E ∗ (e) is the transitive closure of E(e)
with respect to the causing events, i.e.,
if e = (a , t , R , A , T ) ∈ E ∗ (e) and
there exists e = (a , t , R , A , T ) ∈ E with a ∈ A and t = T
i(a ) ,
then e ∈ E ∗ (e).
Now we define well-formed explanations that provide a unique explanation for
any action and must ultimately be explained by input data and requirements only.
Definition 1.3 A set of explanations E is well-formed, iff
1. for any e = (a, t, R, A, T ) ∈ E there does not exist e = (a, t, R , A , T ) ∈
E ∗ (e) with (R, A, T ) = (R , A , T ),
2. for any e ∈ E if e = (a , t , R , A , T ) ∈ E ∗ (e), then for any a ∈ A /A
↓I ,
where A
↓I is the set of actions in A that fix values of inputs I there exists
(a , t , R , A , T ) ∈ E ∗ (e).
Our notation is similar to classical message-based events for formalizing asynchronous distributed systems, e.g., used in the seminal work of Lamport [18] that
explains how to deduce a system-wide wall-clock time. An important difference is,
7
simply disregarded. Technically, the reference to prior events directly refers to their
explanations. Note that there may be multiple justifications for the same action, e.g.,
the light may be turned off because there is sufficient ambient light or because the
battery is low. We require such ambiguities to be resolved during run time based
on the actual implementation of the system. Only for simplicity this formalization
precludes the dependence of an event on multiple previous events executing the
same action.
Lewis [19] requires for counterfactual dependence of an event e on its cause
c that c → e and ¬c → ¬e. However, an event is identified with precisely the
actual occurrence of this event. There may be alternative ways to cause a similar
event, but the actual event e was precisely due to the cause c. Consider the event
that “the window was broken by a stone thrown by Joe.” The window may have
alternatively been broken by a ball thrown by Joe, but this would have been a
different “window broken” event. Lewis achieves this precision by associating the
actual event e with a proposition O(e) that is true iff e occurs and false otherwise.
These propositions allow to abstract from the imprecise natural language. Here we
achieve this precision by adding tags to actions.
Lewis [19] defines causation as a transitive relationship where the cause of an
event is an event itself that has its own causes. Similarly, we traverse the cause–effect
chain of events to identify root causes for some observable action as formalized in
the following.
Definition 1.1 For an explanation e = (a, t, R, A, T ), the immediate set of
explanations is given by
E(e) =
e
= (a
, t
, R
, A
, T
) ∈ E|a
∈ A and t
= T i(a )
Definition 1.2 The full set of explanations E ∗ (e) is the transitive closure of E(e)
with respect to the causing events, i.e.,
if e = (a , t , R , A , T ) ∈ E ∗ (e) and
there exists e = (a , t , R , A , T ) ∈ E with a ∈ A and t = T
i(a ) ,
then e ∈ E ∗ (e).
Now we define well-formed explanations that provide a unique explanation for
any action and must ultimately be explained by input data and requirements only.
Definition 1.3 A set of explanations E is well-formed, iff
1. for any e = (a, t, R, A, T ) ∈ E there does not exist e = (a, t, R , A , T ) ∈
E ∗ (e) with (R, A, T ) = (R , A , T ),
2. for any e ∈ E if e = (a , t , R , A , T ) ∈ E ∗ (e), then for any a ∈ A /A
↓I ,
where A
↓I is the set of actions in A that fix values of inputs I there exists
(a , t , R , A , T ) ∈ E ∗ (e).
Our notation is similar to classical message-based events for formalizing asynchronous distributed systems, e.g., used in the seminal work of Lamport [18] that
explains how to deduce a system-wide wall-clock time. An important difference is,