6
G. Fey and R. Drechsler
1.3.1 Formalizing Explanations
We consider explanations in terms of cause–effect relationships. Before defining
explanations we describe our system model. The system is represented by a set of
variables V composed of disjoint sets of input variables I , output variables O, and
internal variables. A variable is mapped to a value at any time while the system
executes.
This system model is quite general. For a digital system a variable may
correspond to a variable in software or to a signal in (digital) hardware. For a
cyber-physical system a variable may also represent the activation of an actuator
or a message sent over the network. A fresh variable not part of the system may be
used to model an abstract concept, e.g., “move forward” instead of actual control
signals for a motor driver. Run-time reconfiguration of a system, which may impact
explanations, is modeled as a larger system with configurations and configuration
changes stored in variables. A hierarchical system architecture can be represented
by organizing the variables—and related actions–into disjoint subsets. However,
continuous behavior in time or continuous values are not within the scope of this
work.
Based on this system model we introduce our notion of actions, events, causes,
and explanations to formalize them afterwards. An action of a system fixes a subset
of variables to certain values. 1 An observable action fixes observable output values
of the system. An input action fixes input variables that are not controlled by the
system, but by the environment. An action executed at a specific point in time by
the running system is an event. We assume that a set of requirements is available for
the system from a precise specification. A cause is an event or a requirement. An
explanation for an event consists of one or more causes.
These terms now need more formal definitions to reason about explanations.
An action assigns values to a subset of either I , O, or V /(O ∪ I ) of the
variables. We define an ordered set of actions A with i(a) for a ∈ A providing
the unique index of a, a set of requirements R, and the set of explanations
E ⊆ A × N × 2 R × 2 A × N |A| . An explanation e = (a, t, R, A, T ) ∈ E relates
the action a with unique tag t, i.e., the event (a, t) to its causes. The tag t may
be thought of as the value of a system-wide wall-clock time when executing the
action. However, such a strong notion of timing is not mandatory. Having the same
tag for a particular action occurring at most once is sufficient for our purpose and
is easier to implement in an asynchronous distributed system. The vector T in an
explanation relates all actions in A to their unique tags using the index function i(a)
such that a ∈ A is related to the event (a, T i(a) ), where T j denotes the j th element
of vector T . Since A ⊆ A the relation |A| ≤ |T | holds, so unused tags in T are
1 An extension of our formalism could consider more complex actions that include a certain series
of assignments over time, e.g., to first send an address and afterwards data over a communication
channel. However, for simplicity we assume here that an appropriate abstraction layer is available.
Nonetheless, multiple valuations of the variables may be associated to the same action, e.g., the
action “moving towards front left” may abstract from the radius of the curve followed by a system.
G. Fey and R. Drechsler
1.3.1 Formalizing Explanations
We consider explanations in terms of cause–effect relationships. Before defining
explanations we describe our system model. The system is represented by a set of
variables V composed of disjoint sets of input variables I , output variables O, and
internal variables. A variable is mapped to a value at any time while the system
executes.
This system model is quite general. For a digital system a variable may
correspond to a variable in software or to a signal in (digital) hardware. For a
cyber-physical system a variable may also represent the activation of an actuator
or a message sent over the network. A fresh variable not part of the system may be
used to model an abstract concept, e.g., “move forward” instead of actual control
signals for a motor driver. Run-time reconfiguration of a system, which may impact
explanations, is modeled as a larger system with configurations and configuration
changes stored in variables. A hierarchical system architecture can be represented
by organizing the variables—and related actions–into disjoint subsets. However,
continuous behavior in time or continuous values are not within the scope of this
work.
Based on this system model we introduce our notion of actions, events, causes,
and explanations to formalize them afterwards. An action of a system fixes a subset
of variables to certain values. 1 An observable action fixes observable output values
of the system. An input action fixes input variables that are not controlled by the
system, but by the environment. An action executed at a specific point in time by
the running system is an event. We assume that a set of requirements is available for
the system from a precise specification. A cause is an event or a requirement. An
explanation for an event consists of one or more causes.
These terms now need more formal definitions to reason about explanations.
An action assigns values to a subset of either I , O, or V /(O ∪ I ) of the
variables. We define an ordered set of actions A with i(a) for a ∈ A providing
the unique index of a, a set of requirements R, and the set of explanations
E ⊆ A × N × 2 R × 2 A × N |A| . An explanation e = (a, t, R, A, T ) ∈ E relates
the action a with unique tag t, i.e., the event (a, t) to its causes. The tag t may
be thought of as the value of a system-wide wall-clock time when executing the
action. However, such a strong notion of timing is not mandatory. Having the same
tag for a particular action occurring at most once is sufficient for our purpose and
is easier to implement in an asynchronous distributed system. The vector T in an
explanation relates all actions in A to their unique tags using the index function i(a)
such that a ∈ A is related to the event (a, T i(a) ), where T j denotes the j th element
of vector T . Since A ⊆ A the relation |A| ≤ |T | holds, so unused tags in T are
1 An extension of our formalism could consider more complex actions that include a certain series
of assignments over time, e.g., to first send an address and afterwards data over a communication
channel. However, for simplicity we assume here that an appropriate abstraction layer is available.
Nonetheless, multiple valuations of the variables may be associated to the same action, e.g., the
action “moving towards front left” may abstract from the radius of the curve followed by a system.