1 Introduction

It is becoming the norm that software artefacts participate in actions and decisions that affect humans. This trend has been catching momentum for decades, and is now amplified considerably by the remarkable abilities of machine-learnt methods.

However, our understanding of what is the cause of a specific automated decision is lagging far behind. More severe, we are lacking the scientifc basis to explain how several such applications interact in cascades of automated decisions. With the increase in cyber-physical technology impacting our lives, the consequences of this gradual loss in understanding are becoming severe.

The long-term ambition of this track of ISOLA is to explore how computer aided verification techniques can be leveraged to master the explanation challenge. Our focus are algorithmic and tool-supported approaches that aim at making the behaviour of software and CPS systems understandable.

2 Context

Scientifc work on explanations has not been an explicit focus of past research in the verification community, but nevertheless there are a number of prominent techniques that can be considered individual attack points for orchestrated efforts. We review the (according to our limited understanding) major research directions below.

Explaining negative verification results. Most model-checking tools accompany negative verification results with counterexamples to provide an evidence why the model violates its specification. These are finite prefixes of erroneous executions of the model. Although such counterexamples can support debugging, they often tend to be long and identifying the failure in the counterexample trace becomes a non-trivial task. This observation has motivated research on how to extract the relevant information from counterexamples that is needed for debugging purposes. Following the structural equation approach of Halpern and Pearl, the causality-based analysis of counterexamples has been first proposed by Beer et al. [2] with the intention to generate and visualise user-understandable explanations in terms of diagrams for selected paths. This approach has been further advanced by analysing sets of counterexample traces for the purpose of extracting causal relations and representing them by logical formulas, which are then used to generate visualisable fault trees [32, 31]. Other techniques aiming at explanations of negative model-checking results rely on distance metrics for program executions to support understanding and the localisation of errors [17, 18]. An approach for cause consequence analysis using temporal logics has been presented in [36, 20].

Explaining positive verification results. Orthogonal to the approaches for explaining negative verification results is vacuity detection and the certification of verification results. Vacuity detection [3, 27, 5] is motivated by the observation that positive verification results cannot rule out cases where the model is wrong or where there is no perfect match between the formal specification and the desired requirements. It relies on a stronger (“non-vacuous”) satisfaction relation than in standard model checking and aims to report sufficiently informative witnesses for non-vacuously valid temporal formulas in a given model. Another direction is the certification of formal verification results [28, 38] where the task is to accompany positive model-checking results with a certificate that serves as evidence for the successful system verification and can be checked separately to confirm that the system indeed meets its specification. Certification techniques for probabilistic models have been proposed that are based on Farkas certificates [16, 23, 22] and shown to be related to the construction of witnessing subsystems as in [1, 40, 21]. There is also recent work on certification techniques for timed automata [43, 42]. One step further is the line of research that addresses the verification and certification of formal verifiers using theorem-proving techniques, see, e.g., [13, 24].

Causality Reasoning. Besides the above mentioned work on the causality-based analysis of counterexamples to extract user-understandable explanations of model-checking results, combinations of causality-based reasoning and model-checking techniques have also been used by Chockler et al. [8, 9, 4, 7,8,] to reason about the degree of the responsibility of components for the satisfaction or violation of system properties as well as related coverage metrics. First steps towards compositional causality reasoning in nonprobabilistic systems and for temporal events of a simple modal logic have been presented recently in [6].

Another research direction is to exploit synergies between causality techniques and model checking. An on-the-fly approach to detect causal relationships and to classify execution traces as good or bad with respect to the property to be checked has been presented in [32] and extended in [33] for the quantitative analysis of Markov chains. The essential idea of the causality-based model-checking [29, 30, 15] is to avoid the explicit reference to states of a system model as it is the case for standard model checking. Instead it relies on a notion of concurrent traces and causal links between them and proof rules given by trace transformers. Together with sophisticated data structures, this approach can reduce the complexity of model checking for multi-threaded programs from exponential to polynomial time.

Verfication Explanations for Humans. Many forms of graphical models have been introduced to reason about causality. Examples include cause-effect graphs that have been introduced in the context of software testing [35] or Petri nets [10], or causal graphs [12] that have been used to design tractable algorithms for deciding different forms for causes in Halpern and Pearl’s structural-model approach.

In the probabilistic setting, various graphical models have been proposed in the literature to represent causal dependencies. Most prominent are Bayesian networks that rely on directed acyclic graphs where the nodes represent variables and the edges indicate conditional dependencies (see, e.g., [37]). To overcome the limitations of classical Bayesian networks that assume discrete variables and do not support reasoning about time, several extensions have been proposed in the literature to formalise how the dependencies evolve over time slices (dynamic Bayesian networks) or to reason about continuous variables (e.g., hybrid or heterogeneous Bayesian networks). Another prominent visualisable model are (dynamic) fault trees [39, 11], a well-established industrial standard and graphical notation to illustrate how a hazard can be caused by a combination of so called basic events. In the context of probabilistic model checking, the generation of fault trees from probabilistic counterexamples for Markov chains has been studied by Leitner-Fischer et al. [26, 34, 31].

Aiming at human-understandable textual explanations, the translations of minimal critical sub-MDPs (counterexamples for MDPs as in [40]) into guarded command language has been developed in [41]. The recent paper [14] proposes an alternative approach based on structural natural language sentences to describe the behaviour that leads to a violation of system requirements.

3 Contributions in this Track

For the 2020 edition of ISOLA, the track editors have selected two contribution that represent the spectrum of research on verification methods for explanations very well.

The paper by Kölbl and Leue entitled An Algorithm to Compute a Strict Partial Orderering of Actions in Action Trees [25] focusses on tool support for causality checking. At its core is a novel method for computing a causal explanation. This explanation here takes the form of an ordered sequences of actions that lead to a violation of a reachability property. Earlier work in this context was able to compute the unordered set of such actions, while the present contribution additionally provides them in a strictly partial ordered form, thus giving more specific axplanatory feedback to the user. The approach is implemented in the tool QuantUM and its performance and usability is discussed.

The paper by Gros et al. entitled TraceVis: Towards Visualization for Deep Statistical Model Checking [19] showcases a very innovative explanation component for neural network behaviour. It starts off from deep statistical model checking (DSMC), a recently proposed approach to statistically analyse the behaviour of a neural network employed as a decision entity to solve a family of two-dimensional navigation problems, known as the Racetrack. The DSMC analysis delivers a variety of estimates of numerical nature. The present paper explores the use of visualization techniques to support human analysts and domain engineers when exploringthese results. The authors present an interactive visualization tool which enables visual exploration of Racetrack crash probabilities as well as in-depth examination of the policy traces generated by DSMC. By this, the authors succesfully demonstrate how visualization can foster the effective model-checking-based analysis for the purpose of advanced explanation support for neural network behaviour.