1 Self-explaining Digital Systems
3
– We discuss implementation aspects enabling a trade-off between the degree
of completeness in explanations and implementation cost. In particular, when
certain actions of the system and certain specification aspects are known to be
more important than others, this guides the trade-off.
– We consider a robot controller implemented at the register transfer level in
Verilog as a case study. Besides giving details of the implementation, we prove
completeness of explanations for the main controller of the robot.
This chapter extends the overview on self-explanation in combination with selfverification published in [7] that mainly considered methodology without giving
technical details. The work in [10] gives the formal definition, but no conceptual
framework for different abstraction levels, provides fewer properties about the robot
controller, and does not prove completeness.
The chapter is structured as follows: While there is no directly related work,
Sect. 1.2 considers the aspect of explanation in other areas. Section 1.3 formalizes
explanations, defines a self-explaining system, its implementation, and verification.
Section 1.4 studies a self-explaining controller for an autonomous robot. Extensions
and automation for self-explanation are discussed in Sect. 1.5. Section 1.6 draws
conclusions.
1.2 Related Work
The concept of self-explaining digital systems is new but related to explanation as
understood in other domains.
Causation has a long history in philosophy where [19] is a more recent approach
that relates events and their causes in chains such that one event can cause a next
one. Often underlying hidden relations make this simple approach controversial.
A rigorous mathematical approach instead can use statistical models to cope with
non-understood as well as truly non-deterministic dependencies [31]. Artificial
intelligence particularly in the form of artificial neural networks made a significant
progress in the recent past modeling such relations. A large number of training
samples train the neural network that afterwards carries out a task or performs a
classification on new samples. However, given an artificial neural network it is not
understandable how it internally processes data, e.g., what kind of features from the
data samples are used or extracted, how they are represented, etc. First approaches
to reconstruct this information in the input space have been proposed [12, 26].
Decision procedures are a class of very complex algorithms producing results
needed to formally certify the integrity of systems. The pairing of complexity
and certification stimulated the search for understanding the verdict provided by
a decision procedure. Typically, this verdict either yields a feasible solution to some
task, e.g., a satisfying assignment in case of Boolean satisfiability (SAT), or denies
the existence of any solution at all, e.g., unsatisfiability in case of SAT solving.
A feasible solution can easily be checked, e.g., as a recipe to solve some task.
3
– We discuss implementation aspects enabling a trade-off between the degree
of completeness in explanations and implementation cost. In particular, when
certain actions of the system and certain specification aspects are known to be
more important than others, this guides the trade-off.
– We consider a robot controller implemented at the register transfer level in
Verilog as a case study. Besides giving details of the implementation, we prove
completeness of explanations for the main controller of the robot.
This chapter extends the overview on self-explanation in combination with selfverification published in [7] that mainly considered methodology without giving
technical details. The work in [10] gives the formal definition, but no conceptual
framework for different abstraction levels, provides fewer properties about the robot
controller, and does not prove completeness.
The chapter is structured as follows: While there is no directly related work,
Sect. 1.2 considers the aspect of explanation in other areas. Section 1.3 formalizes
explanations, defines a self-explaining system, its implementation, and verification.
Section 1.4 studies a self-explaining controller for an autonomous robot. Extensions
and automation for self-explanation are discussed in Sect. 1.5. Section 1.6 draws
conclusions.
1.2 Related Work
The concept of self-explaining digital systems is new but related to explanation as
understood in other domains.
Causation has a long history in philosophy where [19] is a more recent approach
that relates events and their causes in chains such that one event can cause a next
one. Often underlying hidden relations make this simple approach controversial.
A rigorous mathematical approach instead can use statistical models to cope with
non-understood as well as truly non-deterministic dependencies [31]. Artificial
intelligence particularly in the form of artificial neural networks made a significant
progress in the recent past modeling such relations. A large number of training
samples train the neural network that afterwards carries out a task or performs a
classification on new samples. However, given an artificial neural network it is not
understandable how it internally processes data, e.g., what kind of features from the
data samples are used or extracted, how they are represented, etc. First approaches
to reconstruct this information in the input space have been proposed [12, 26].
Decision procedures are a class of very complex algorithms producing results
needed to formally certify the integrity of systems. The pairing of complexity
and certification stimulated the search for understanding the verdict provided by
a decision procedure. Typically, this verdict either yields a feasible solution to some
task, e.g., a satisfying assignment in case of Boolean satisfiability (SAT), or denies
the existence of any solution at all, e.g., unsatisfiability in case of SAT solving.
A feasible solution can easily be checked, e.g., as a recipe to solve some task.