Formally Explaining Neural Networks within Reactive Systems
Deep neural networks (DNNs) are increasingly being used as controllers in
reactive systems. However, DNNs are highly opaque, which renders it difficult
to explain and justify their actions. To mitigate this issue, there has been a
surge of interest in explainable AI (XAI) techniques, capable of pinpointing
the input features that caused the DNN to act as it did. Existing XAI
techniques typically face two limitations: (i) they are heuristic, and do not
provide formal guarantees that the explanations are correct; and (ii) they
often apply to ``one-shot'' systems, where the DNN is invoked independently of
past invocations, as opposed to reactive systems. Here, we begin bridging this
gap, and propose a formal DNN-verification-based XAI technique for reasoning
about multi-step, reactive systems. We suggest methods for efficiently
calculating succinct explanations, by exploiting the system's transition
constraints in order to curtail the search space explored by the underlying
verifier. We evaluate our approach on two popular benchmarks from the domain of
automated navigation; and observe that our methods allow the efficient
computation of minimal and minimum explanations, significantly outperforming
the state of the art. We also demonstrate that our methods produce formal
explanations that are more reliable than competing, non-verification-based XAI
techniques.
Shahaf Bassan, Guy Amir, Davide Corsi, Idan Refaeli, Guy Katz
# Formally Explaining Neural Networks

###### Abstract

Deep neural networks (DNNs) are increasingly being used as controllers in reactive systems. However, DNNs are highly opaque, which renders it difficult to explain and justify their actions. To mitigate this issue, there has been a surge of interest in explainable AI (XAI) techniques, capable of pinpointing the input features that caused the DNN to act as it did. Existing XAI techniques typically face two limitations: (i) they are heuristic, and do not provide formal guarantees that the explanations are correct; and (ii) they often apply to "one-shot" systems, where the DNN is invoked independently of past invocations, as opposed to reactive systems. Here, we begin bridging this gap, and propose a formal DNN-verification-based XAI technique for reasoning about multi-step, reactive systems. We suggest methods for efficiently calculating succinct explanations, by exploiting the system's transition constraints in order to curtail the search space explored by the underlying verifier. We evaluate our approach on two popular benchmarks from the domain of automated navigation; and observe that our methods allow the efficient computation of minimal and minimum explanations, significantly outperforming the state of the art. We also demonstrate that our methods produce formal explanations that are more reliable than competing, non-verification-based XAI techniques.

+
Footnote †: Both authors contributed equally.

## I Introduction

Deep neural networks (DNNs) [61] are used in numerous key domains, such as computer vision [58], natural language processing [26], computational biology [10], and more [23]. However, despite their tremendous success, DNNs remain "black boxes", uninterpretable by humans. This issue is concerning, as DNNs are prone to critical errors [19, 108] and unexpected behaviors [11, 31].

DNN opacity has prompted significant research on explainable AI (XAI) techniques [67, 85, 86], aimed at explaining the decisions made by DNNs, in order to increase their trustworthiness and reliability. Modern XAI methods are useful and scalable, but they are typically heuristic; i.e., there is no provable guarantee that the produced explanation is correct [20, 48]. This hinders the applicability of these approaches to critical systems, where regulatory bars are high [72].

These limitations provide ample motivation for _formally_ explaining DNN decisions [20, 36, 42, 72]. And indeed, the formal verification community has suggested harnessing recent developments in DNN verification [14, 22, 29, 32, 73, 76, 77, 79, 90, 95, 102, 103] to produce provable explanations for DNNs [17, 42, 47]. Typically, such approaches consider a particular input to the DNN, and return a subset of its features that caused the DNN to classify the input as it did. These subsets are called _abductive explanations_, _prime implicants_ or _PI-explanations_[17, 47, 93]. This line of work constitutes a promising step towards more reliable XAI; but so far, existing work has focused on explaining decisions of "one-shot" DNNs, such as image and tabular data classifiers [17, 46, 47], and has not addressed more complex systems.

Modern DNNs are often used as controllers within elaborate reactive systems, where a DNN's decisions affect its future invocations. A prime example is _deep reinforcement learning_ (_DRL_) [64], where DNNs learn control policies for complex systems [12, 18, 62, 68, 80, 94, 106]. Explaining the decisions of DRL agents (XRL) [35, 54, 69, 82] is an important domain within XAI; but here too, modern XRL techniques are heuristic, and do not provide formally correct explanations.

In this work, we make a first attempt at formally defining abductive explanations for _multi-step decision processes_. We propose novel methods for computing such explanations and supply the theoretical groundwork for justifying the soundness of these methods. Our framework is model-agnostic, and could be applied to diverse kinds of models; but here, we focus on DNNs, where producing abductive explanations is known to be quite challenging [17, 15, 47]. With DNNs, our technique allows us to reduce the number of times a network has to be unrolled, circumventing a potential exponential blow-up in runtime; and also allows us to exploit the reactive system's transition constraints, as well as the DNN's sensitivity to small input perturbations, to curtail the search space even further.

For evaluation purposes, we implemented our approach as a proof-of-concept tool, which is publicly available as an artifact accompanying this paper [16]. We used this tool to automatically generate explanations for two popular DRL benchmarks: a navigation system on an abstract, two-dimensional grid, and a real-world robotic navigation system. Our evaluation demonstrates that our methods significantly outperform state-of-the-art, rigorous methods for generating abductive explanations, both in terms of efficiency and in the size of the explanation generated. When comparing our approach to modern, heuristic-based XAI approaches, our explanations were found to be significantly more precise. We regard these results as strong evidence of the usefulness of
applying verification in the context of XAI.

The rest of this paper is organized as follows: Sec. II contains background on DNNs, their verification, and their formal explainability. Sec. III contains our definitions for formal abductive explanations and contrastive examples for reactive systems. In Sec. IV we propose different methods for computing such abductive explanations. We then evaluate these approaches in Sec. V, followed by a discussion of related work in Sec. VI; and we conclude in Sec. VII.

## II Background

**DNNs.** Deep neural networks (DNNs) [61] are directed, layered graphs, whose nodes are referred to as _neurons_. They propagate data from the first (_input_) layer, through intermediate (_hidden_) layers, and finally onto an _output_ layer. A DNN's output is calculated by assigning values (representing input _features_) to the input layer, and then iteratively calculating the neurons' values in subsequent layers. In classification, each output neuron corresponds to a _class_, and the input is classified as the class matching the greatest output. Fig. 1 depicts a toy DNN. The input layer has three neurons and is followed by a weighted-sum layer that calculates an affine transformation of the input values. For example, given input \(V_{1}=[1,1,1]^{T}\), the second layer evaluates to \(V_{2}=[7,8,11]^{T}\). This is followed by a ReLU layer, which applies the ReLU(\(x\)) = \(\max(0,x)\) function to each value in the previous layer, resulting in \(V_{3}=[7,8,11]^{T}\). The output layer computes the weighted sum \(V_{4}=[15,-4]^{T}\). Because the first output neuron has the greatest value, \(V_{1}\) is classified as the output class corresponding to that neuron.

**DNN Verification.** We define a DNN verification query as a tuple \(\{P,N,Q\}\), where \(N\) is a DNN that maps an input vector \(x\) to an output vector \(y=N(x)\), \(P\) is a predicate over \(x\), and \(Q\) is a predicate over \(y\)[55]. A DNN verifier needs to answer whether there exists some input \(x^{\prime}\) that satisfies \(P(x^{\prime})\wedge Q(N(x^{\prime}))\) (a SAT result) or not (an UNSAT result). It is common to express \(P\) and \(Q\) in the logic of real arithmetic [66]. The problem of verifying DNNs is known to be NP-Complete [55].

**Formal Explanations for Classification DNNs.** A classification problem is a tuple \(\{F,D,K,N\}\), where (i) \(F=\{1,\ldots,m\}\) is the feature set; (ii) \(D=\{D_{1},D_{2},\ldots,D_{m}\}\) are the domains of individual features, and the entire feature space is \(\mathbb{F}=(D_{1}\times D_{2}\times\ldots\times D_{m})\); (iii) \(K=\{c_{1},c_{2},\ldots,c_{n}\}\) represents the set of all classes; and (iv) \(N:\mathbb{F}\to K\) is the classification function, represented by a neural network. A _classification instance_ is a pair \((v,c)\), where \(v\in\mathbb{F}\), \(c\in K\), and \(c=N(v)\). Intuitively, this means that \(N\) maps the input \(v\) to class \(c\).

Formally explaining the instance \((v,c)\) entails determining _whv_\(v\) is classified as \(c\). An _explanation_ (also known as an _abductive explanation_) is defined as a subset of features, \(E\subseteq F\), such that fixing these features to their values in \(v\) guarantees that the input is classified as \(c\), regardless of features in \(F\setminus E\). The features _not_ part of the explanation are _"free"_ to take on any arbitrary value, but cannot affect the classification. Formally, given an input \(v=(v_{1},\ldots,v_{m})\in\mathbb{F}\) classified by the neural network to \(N(v)=c\), we define an explanation as a subset of features \(E\subseteq F\), such that:

\[\forall x\in\mathbb{F}.\quad\bigwedge_{i\in E}(x_{i}=v_{i})\to(N(x)=c) \tag{1}\]

We demonstrate formal explanations using the running example from Fig. 1. For simplicity, assume that each input can only take the values \(0\) or \(1\). Fig. 2 shows that the set \(\{v_{1}^{1},v_{1}^{2}\}\) is an explanation for the input vector \(V_{1}=[1,1,1]^{T}\): setting the first two features in \(V_{1}\) to \(1\) ensures that the classification is unchanged, regardless of the values the third feature takes.

A candidate explanation \(E\) can be verified through a verification query \(\{P,N,Q\}=\langle E=v,N,Q_{\neg c}\rangle\), where \(E=v\) means that all of the features in \(E\) are set to their corresponding values in \(v\), and \(Q_{\neg c}\) implies that the classification of this query is _not_\(c\). If this query is UNSAT, then \(E\) is a valid explanation for the instance \((v,c)\).

It is straightforward to show that the set of all features is a trivial explanation. However, smaller explanations typically provide more meaningful information regarding the decision of the classifier; and we thus focus on finding _minimal_ and _minimum_ explanations. A _minimal explanation_ is an explanation \(E\subseteq F\) that ceases to be an explanation if any of its features are removed:

\[\begin{split}&(\forall x\in\mathbb{F}.\quad\bigwedge_{i\in E}(x_{i }=v_{i})\to(N(x)=c))\ \wedge\\ &(\forall j\in E.\quad\exists y\in\mathbb{F}.\quad\bigwedge_{i \in E\setminus j}(y_{i}=v_{i})\wedge(N(y)\neq c))\end{split} \tag{2}\]

A minimal explanation for our running example, \(\{v_{1}^{1},v_{1}^{2}\}\), is depicted in Fig. 15 of the appendix.

A _minimum explanation_ is a subset \(E\subseteq F\) which is a minimal explanation of minimum size; i.e., there is no other

Fig. 1: A toy DNN.
minimal explanation \(E^{\prime}\neq E\) such that \(|E^{\prime}|<|E|\). Fig. 16 of the appendix shows that \(\{v_{1}^{3}\}\) is a minimal explanation of minimal cardinality, and is hence a minimum explanation in our example.

**Contrastive Examples.** We define a contrastive example (also known as a _contrastive explanation (CXP)_) as a subset of features \(C\subseteq F\), whose alteration may cause the classification of \(v\) to change. More formally:

\[\exists x\in\mathbb{F}.\quad\bigwedge_{i\in F\setminus C}(x_{i}=v_{i})\wedge(N (x)\neq c) \tag{3}\]

A contrastive example for our running example appears in Fig. 3.

Checking whether \(C\) is a contrastive example can be performed using the query \((P,N,Q)=\{(F\setminus C)=v,N,Q_{-c}\}\): \(C\) is contrastive iff the quest is SAT. Any set containing a contrastive example is contrastive, and so we consider only contrastive examples that are minimal, i.e., which do not contain any smaller contrastive examples.

Contrastive examples have an important property: every explanation contains at least one element from every contrastive example [17, 46]. This can be used for showing that a _minimum hitting set_ (MHS; see Sec. II of the appendix) of all contrastive examples is a minimum explanation [84, 44]. In addition, there exists a duality between contrastive examples and explanations [46, 50]: minimal hitting sets of all contrastive examples are minimal explanations, and minimal hitting sets of all explanations are minimal contrastive examples. This relation can be proved by reducing explanations and contrastive examples to minimal unsatisfiable sets and minimal correction sets, respectively, where this duality is known to hold [46]. Calculating an MHS is NP-hard, but can be performed in practice using modern MaxSAT or MILP solvers [41, 63]. The duality is thus useful since computing contrastive examples and calculating their MHS is often more efficient than directly computing minimum explanations [17, 46, 47].

## III K-Step Formal Explanations

A reactive system is a tuple \(R=\langle S,A,I,T\rangle\), where \(S\) is a set of states, \(A\) is a set of actions, \(I\) is a predicate over the states of \(S\) that indicates initial states, and \(T\subseteq S\times A\times S\) is a transition relation. In our context, a reactive system has an associated neural network \(N:S\to A\). A \(k\)-step execution \(\mathcal{E}\) of \(R\) is a sequence of \(k\) states \((s_{1},\ldots,s_{k})\), such that \(I(s_{1})\) holds, and for all \(1\leq i\leq k-1\) it holds that \(T(s_{i},N(s_{i}),s_{i+1})\). We use \(\mathcal{E}_{S}=(s_{1},\ldots,s_{k})\) to denote the sequence of \(k\) states visited in \(\mathcal{E}\), and \(\mathcal{E}_{A}=(a_{1},\ldots,a_{k})\) to denote the sequence of \(k\) actions selected in these states. More broadly, a reactive system can be considered as a deterministic, finite-state transducer Mealy automaton [91]. Our goal is to better understand \(\mathcal{E}\), by finding abductive explanations and contrastive examples that explain why \(N\) selected the actions in \(\mathcal{E}_{A}\).

**K-Step Abductive Explanations.** Informally, we define an explanation \(E\) for a \(k\)-step execution \(\mathcal{E}\) as a subset of features of each of the visited states in \(\mathcal{E}_{S}\), such that fixing these features (while freeing all other features) is sufficient for forcing the DNN to select the actions in \(\mathcal{E}_{A}\). More formally, \(E=(E_{1},\ldots,E_{k})\), such that \(\forall x_{1},x_{2},\ldots,x_{k}\in\mathbb{F}\),

\[\big{(}\bigwedge_{i=1}^{k-1}T(x_{i},N(x_{i}),x_{i+1})\wedge\bigwedge_{i=1}^{k} \bigwedge_{j\in E_{i}}(x_{i}^{j}=s_{i}^{j})\big{)}\rightarrow\bigwedge_{i=1}^{ k}N(x_{i})=a_{i} \tag{4}\]

We continue with our running example. Consider the transition relation \(T=\{(s,a,s^{\prime})\mid s^{3}=s^{\prime 3}\}\); i.e., we can transition from state \(s\) to state \(s^{\prime}\) provided that the third input neuron has the same value in both states, regardless of the action selected in \(s\). Observe the \(2\)-step execution \(\mathcal{E}:s_{1}=(1,1,1)\xrightarrow{c_{1}}s_{2}=(1,0,1)\xrightarrow{c_{1}}\), depicted in Fig. 4 (for simplicity, we omit the network's hidden neurons), and suppose we wish to explain \(\mathcal{E}_{A}=\{c_{1},c_{1}\}\). Because \(\{s^{3}\}\) is an explanation for the first step, and because fixing \(s_{1}^{3}\) also fixes the value of \(s_{2}^{3}\), it follows that fixing \(s_{1}^{3}\) is sufficient to guarantee that action \(c_{1}\) is selected twice -- i.e., \((\{s^{3}\},\varnothing)\) is a multi-step explanation for \(\mathcal{E}\).

Given a candidate \(k\)-step explanation, we can check its validity by encoding Eq. 4 as a DNN verification query. This is achieved by _unrolling_ the network \(N\) for \(k\) subsequent steps; i.e., by encoding a network that is \(k\) times larger than \(N\), with input and output vectors that are \(k\) times larger than the original. We must also encode the transition relation \(T\) as a set of constraints involving the input values, to mimic \(k\) time-steps within a single feed-forward pass. We use \(N_{[i]}\) to denote an unrolling of the neural network \(N\) for \(i\) steps, for \(1\leq i\leq k\).

Using the unrolled network \(N_{[k]}\), we encode the negation of Eq. 4 as the query \((P,N,Q)=\langle E=\mathcal{E}_{S},N_{[k]},Q_{-\mathcal{E}_{A}}\rangle\), where \(E=\mathcal{E}_{S}\) means that we restrict the features in each subset \(E_{i}\in E\) to their corresponding values in \(s_{i}\); and \(Q_{-\mathcal{E}_{A}}\) indicates that in some step \(i\), an action that is not \(a_{i}\) was selected by the
DNN. An UNSAT result for this query indicates that \(E\) is an explanation for \(\mathcal{E}\), because fixing \(E\)'s features to their values forces the given sequence of actions to occur.

We can naturally define a _minimal_\(k\)-step explanation as a \(k\)-step explanation that ceases to be a \(k\)-step explanation when we remove any of its features. A _minimum_\(k\)-step explanation is a minimal \(k\)-step explanation of the lowest possible cardinality; i.e., there does not exist a \(k\)-step explanation \(E^{\prime}=(E^{\prime}_{1},E^{\prime}_{2},\ldots,E^{\prime}_{k})\) such that \(\sum_{i=1}^{k}|E^{\prime}_{i}|<\sum_{i=1}^{k}|E_{i}|\).

**K-Step Contrastive Examples.** A contrastive example \(C\) for an execution \(\mathcal{E}\) is a subset of features whose alteration can cause the selection of an action not in \(\mathcal{E}_{A}\). A \(k\)-step contrastive example is depicted in Fig. 5: altering the features \(s^{3}_{1}\) and \(s^{3}_{2}\) may cause action \(c_{2}\) to be chosen instead of \(c_{1}\) in the second step. Formally, \(C\) is an ordered set of (possibly empty) subsets \(C=(C_{1},C_{2},\ldots,C_{k})\), such that \(C_{i}\subseteq F\), and for which \(\exists x_{1},x_{2},\ldots,x_{k}\in\mathbb{F}\) such that

\[\begin{split}&\big{(}\bigwedge_{i=1}^{k-1}T(x_{i},N(x_{i}),x_{i+1}) \big{)}\wedge\\ &\big{(}\bigwedge_{i=1}^{k}\bigwedge_{j\in F\setminus C_{i}}(x_{i }^{j}=s_{i}^{j})\big{)}\wedge\big{(}\bigvee_{i=1}^{k}N(x_{i})\neq a_{i}\big{)} \end{split} \tag{5}\]

Similarly to multi-step explanations, \(C\) is a multi-step contrastive example iff the verification query: \((P,N,Q)=\langle(F\setminus C_{1},F\setminus C_{2},\ldots,F\setminus C_{k})= \mathcal{E}_{S},N_{[k]},Q_{\neg\mathcal{E}_{A}}\rangle\) is SAT.

## IV Computing Formal K-Step Explanations

We now propose four different methods for computing formal \(k\)-step explanations, focusing on _minimal_ and _minimum_ explanations. All four methods use an underlying DNN verifier to check candidate explanations, but differ in how they enumerate different explanation candidates until ultimately converging to an answer. We begin with the more straightforward methods.

**Method 1: A Single, K-Sized Step.** The first method is to encode the negation of Eq. 4 by unrolling all \(k\) steps of the network, as described in Sec. III. This transforms the problem into explaining a non-reactive, single-step system (e.g., a "one-shot" classifier). We can then use any existing abductive explanation algorithm for explaining the unrolled DNN (e.g., [17, 46, 47]).

This method is likely to produce small explanation sets but is extremely inefficient. Encoding \(N_{[k]}\) results in an input space roughly \(k\) times the size of any single-step encoding. Such an unrolling for our running example is depicted in Fig. 6. Due to the NP-completeness of DNN verification, this may cause an exponential growth in the verification time of each query. Since finding minimal explanations requires a linear number of queries (and for minimum explanations -- a worst-case exponential number), this may cause a substantial increase in runtime.

**Method 2: Combining Independent, Single-Step Explanations.** Here, we dismantle any \(k\)-step execution into \(k\) individual steps. Then, we _independently_ compute an explanation for each step, using any existing algorithm, and without taking the transition relation into account. Finally, we concatenate these explanations to form a multi-step explanation. Fixing the features of the explanation in each step ensures that the ensuing action remains the same, guaranteeing the soundness of the combined explanation.

The downside of this method is that the resulting \(E\) need not be minimal or minimum, even if its constituent \(E_{i}\) explanations are minimal or minimum themselves; see Fig. 7. In this instance, finding a minimum explanation for each step results in the 2-step explanation (\(\{s^{3}\},\{s^{3}\}\)), which is _not minimal_ -- even though its components are minimum explanations for their respective steps. The reason for this phenomenon is that this method ignores the transition constraints and information flow across time-steps. This can result in larger and less meaningful explanations, as we later show in Sec. V.

**Method 3: Incremental Explanation Enumeration.** We now suggest a scheme that takes into consideration the transition

Fig. 5: (\(\{s^{3}\},\{s^{3}\}\)) is a multi-step contrastive example for \(\mathcal{E}\).

Fig. 6: Finding explanations using a 2-step unrolling.
constraints between steps (unlike Method 2), but which encodes the verification queries for validating explanations in a more efficient manner than Method 1. The scheme relies on the following lemma:

**Lemma 1**.: _Let \(E=(E_{1},E_{2},\ldots,E_{k})\) be a \(k\)-step explanation for execution \(\mathcal{E}\), and let \(1\leq i\leq k\) such that \(\forall j>i\) it holds that \(E_{j}=F\). Let \(E^{\prime}\) be the set obtained by removing a set of features \(F^{\prime}\subseteq E_{i}\) from \(E_{i}\), i.e., \(E^{\prime}=(E_{1},\ldots,E_{i-1},E_{i}\smallsetminus F^{\prime},E_{i+1},\ldots, E_{k})\). In this case, fixing the features in \(E^{\prime}\) prevents any changes in the first \(i-1\) actions \((a_{1},\ldots,a_{i-1})\); and if any of the last \(k-i+1\) actions \((a_{i},\ldots,a_{k})\) change, then \(a_{i}\) must also change._

A proof appears in Sec. III of the appendix. The lemma states that "breaking" an explanation \(E\) of \(\mathcal{E}\) at some step \(i\) (by removing features from the \(i\)'th step), given that the features in steps \(i+1,\ldots,k\) are fixed, causes \(a_{i}\) to change before any other action. In this scenario, we can determine whether \(E\) explains \(\mathcal{E}\) using a simplified verification query: we can check whether \((E_{1},\ldots,E_{i})\) explains the first \(i\) steps of \(\mathcal{E}\), regardless of steps \(i+1,...,k\). If so, then \(a_{i}\) cannot change; and from Lemma 1, no action in \(\mathcal{E}_{A}\) can change, and \((E_{1},\ldots,E_{k})\) is an explanation for \(\mathcal{E}\). Otherwise, \(E\) allows an action in \(\mathcal{E}_{A}\) to change, and it does not explain \(\mathcal{E}\). We can leverage this property to efficiently enumerate candidates as part of a search for a minimal/minimum explanation for \(\mathcal{E}\), as explained next.

**Finding Minimal Explanations with Method 3.** A common approach for finding minimal explanations for a "one-shot" classification instance is via a greedy algorithm, which dispatches a linear number of queries to the underlying verifier [47]. Such an algorithm can start with the explanation set to be the entire feature space, and then iteratively attempt to remove features. If removing a feature allows misclassification, the algorithm keeps it as part of the explanation; otherwise, it removes the feature and continues. A pseudo-code for this approach appears in Alg. 1.

```
1:\(N\) (DNN), \(F\) (\(N\)'s features), \(v\) (values), \(c\) (predicted class)
2:\(\text{Explanation}\leftarrow\ F\)
3:for each\(f\in F\)do
4:if verify ((Explanation\(\smallsetminus\{\)f\(\}\))=v,N,\(Q_{\neg c}\)) is UNSAT then
5:\(\text{Explanation}\leftarrow\text{Explanation}\smallsetminus\{f\}\)
6:return Explanation
```

**Algorithm 1**Greedy-Minimal-Explanation

We suggest performing a similar process for explaining \(\mathcal{E}\). We start by fixing all features in all states of \(\mathcal{E}\) to their values; i.e., we start with \(E=(E_{1},\ldots,E_{k})\) where \(E_{i}=F\) for all \(i\), and then perform the following steps:

First, we iteratively remove individual features from \(E_{1}\), each time checking whether the modified \(E\) remains an explanation for \(\mathcal{E}\). Since all features in steps \(2,\ldots,k\) are fixed, it follows from Lemma 1 that checking whether the modified \(E\) explains \(\mathcal{E}\) is equivalent to checking whether the modified \(E_{1}\) explains the selection of \(a_{1}\). Thus, we perform a process that is identical to the one in the greedy Alg. 1 for finding a minimal explanation for a "one-shot" classification DNN. At the end of this phase, we are left with \(E=(E_{1},\ldots,E_{k})\) where \(E_{i}=F\) for all \(i>1\) and \(E_{1}\) was reduced by removing features from it. We keep all current features in \(E\) fixed for the following steps.

Second, we begin to iteratively remove features from \(E_{2}\), each time checking whether the modified \(E\) still explains \(\mathcal{E}\). Since the features in steps \(3,\ldots,k\) are entirely fixed, it suffices (from Lemma 1) to check whether the modified \((E_{1},E_{2})\) explains the selection of the first two actions \((a_{1},a_{2})\) of \(\mathcal{E}_{A}\). This is performed by checking whether

\[\begin{split}&(\forall x_{1},x_{2}\in\mathbb{F},\quad T(x_{1},a_{ 1},x_{2})\wedge\bigwedge_{j\in E_{1}}(x_{1}^{j}=s_{1}^{j})\wedge\\ &\bigwedge_{j\in E_{2}}(x_{2}^{j}=s_{2}^{j}))\to N(x_{2})=a_{2} \end{split} \tag{6}\]

We do not need to require that \(N(x_{1})=a_{1}\) (as in Method 1) -- this is guaranteed by Lemma 1. This is significant, because it exempts us from encoding the neural network twice as part of the verification query. We denote the negation of Eq. 6 for validating \((E_{1},E_{2})\) as: \((P,N,Q)=((E_{1},E_{2})=\mathcal{E}_{S_{[1]}},N,Q_{\neg a_{2}})\).

Third, we continue this iterative process for all \(k\) steps of \(\mathcal{E}\), and find the minimal explanation for each step separately. In step \(i\), for each query we encode \(i\) transitions and check whether the modified \(E\) still explains the first \(i\) steps of \(\mathcal{E}\) (by encoding \(((E_{1},\ldots,E_{i})=\mathcal{E}_{S_{[i]}},N,Q_{\neg a_{i}})\)), which _does not_ require encoding the DNN \(i\) times. The correctness of each step follows directly from Lemma 1.

The pseudo-code for this process appears in Alg. 2. The minimality of the resulting explanation holds because removing any feature from this explanation would allow the action in that step to change (since minimality is maintained in each step of the algorithm). An example of the first two iterations of this process on our running example appears in Fig. 8: in the first iteration, we attempt to remove features from the first step, until converging to an explanation \(E_{1}\). In the second iteration, while the features in \(E_{1}\) remain fixed to their values, we encode the constraints of the transition relation \(T(s_{1},a_{1},s_{2})\) between the first two steps, and dispatch queries to verify candidate explanations for the second step -- until converging to a minimal explanation \((E_{1},E_{2})\). In this case, \(E_{2}=\varnothing\), and \((\{s^{3}\},\varnothing)\) is a valid explanation for the \(2\)-step execution, since fixing the value of \(s_{1}^{3}\) determines the value of \(s_{2}^{3}\) -- which forces the selection of \(a_{2}\) in the second step.

We emphasize that incrementally enumerating candidate explanations for a \(k\)-step execution in this way is preferable to simply finding a minimal explanation by encoding verification queries that encompass all \(k\)-steps, a la Method 1: (i) in each iteration, we dispatch a verification query involving only a single invocation of the DNN, thus circumventing the linear growth in the network's size -- which causes an exponential worst-case increase in verification times; and (ii) in each iteration, we do not need to encode the entire set of \(k\) disjuncts
(from the negation of Eq. 4), since we only need to validate \(a_{i}\) on the \(i\)'th iteration, and not all actions of \(\mathcal{E}_{A}\).

```
1:\(N\) (DNN), \(F\) (\(N\)'s features), \(\mathcal{E}\) (execution of length \(k\) to explain)
2:\(\text{Explanation}\leftarrow(E_{1},\dots,E_{k})\) where \(E_{i}=F\) for all \(1\leq i\leq k\)
3:for each\(i\in\{1,...,k\}\) and \(f\in E_{i}\)do
4:ifverify (\((E_{1},\dots,E_{i}\smallsetminus f)\)=\(\mathcal{E}_{S_{\{i\}}},N,Q_{\neg a_{i}}\)) is UNSAT then
5:\(E_{i}\gets E_{i}\smallsetminus f\)
6:return Explanation
```

**Algorithm 2**Incremental-Minimal-Explanation-Enumeration

**Finding Minimum Explanations with Method 3.** We can also use our proposed enumeration to efficiently find _minimum_ explanations, using a recursive approach. In each step \(i=1,\dots,k\), we iterate over all the possible explanations, each time considering a candidate explanation and recursively invoking the procedure for step \(i+1\). In this way, we iterate over all the possible multi-step explanation candidates and can return the smallest one that we find. This process is described in Alg. 3.

Finding a minimum explanation in this manner is superior to using Method 1, for the same reasons noted before. In addition, the exponential blowup here is in the number of explanations in each step, and not in the entire number of features in each step -- which is substantially smaller in many cases. Nevertheless, as the method advances through steps, it is expected to be significantly harder to iterate over all the candidate explanations. We discuss more efficient ways for finding global minimum explanations in Method 4.

**Method 4: Multi-Step Contrastive Example Enumeration.** As mentioned earlier, a common approach for finding minimum explanations is to find all contrastive examples, and then calculate their minimum hitting set (MHS). Because DNNs tend to be sensitive to small input perturbations [96], small contrastive examples are often easy to find, and this can expedite the process significantly [17]. When performing this procedure on a multi-step execution \(\mathcal{E}\), we show that it is possible to enumerate contrastive example candidates in a more efficient manner than simply using the encoding from Method 1.

**Lemma 2**.: _Let \(\mathcal{E}\) be a \(k\)-step execution, and let \(C=(C_{1},\dots,C_{k})\) be a minimal contrastive example for \(\mathcal{E}\); i.e., altering the features in \(C\) can cause at least one action in \(\mathcal{E}_{A}\) to change. Let \(1\leq i\leq k\) denote the index of the first action \(a_{i}\) that can be changed by features in \(C\). It holds that: \(C_{i}\neq\emptyset\); \(C_{j}=\emptyset\) for all \(j>i\); and if there exists some \(l<i\) such that \(C_{l}\neq\emptyset\), then all sets \(\{C_{l},C_{l+1},\dots,C_{i}\}\) are not empty._

The lemma gives rise to the following scheme. We examine some contrastive example \(C^{\prime}\) of _a set of subsequent steps of \(\mathcal{E}\)_. For simplicity, we discuss the case where \(C^{\prime}=(C^{\prime}_{i})\) involves only a single step \(i\), but the technique generalizes to subsets of steps, as well. Such a \(C^{\prime}_{i}\) can be found using a "one-shot" verification query on step \(i\), without encoding the transition relation or unrolling the network. Our goal is to use \(C^{\prime}\) to find many contrastive examples for \(\mathcal{E}\), and use them in computing the MHS. We observe that there are three possible cases:

1. \(C=(\emptyset,\dots,\emptyset,C^{\prime}_{i},\emptyset,\dots,\emptyset)\) already constitutes a contrastive example for \(\mathcal{E}\). In this case, we say that \(C^{\prime}=(C^{\prime}_{i})\) is an _independent contrastive example_.
2. The features in \(C^{\prime}_{i}\) can cause a skew from \(\mathcal{E}\) only when features from preceding steps \(l,\dots,i-1\) (for some \(l<i\)) are also altered. In this case, we say

Fig. 8: Running Method 3 for finding minimal explanations, for two iterations.
that \(C^{\prime}\) is a _dependent contrastive example_, and that it depends on steps \(l,\ldots,i-1\); and together, the features from all these steps form the contrastive example \(C=(\varnothing,\ldots,\varnothing,C_{l},\ldots,C_{i-1},C^{\prime}_{i}, \varnothing,\ldots,\varnothing)\) for \(\mathcal{E}\).
3. \(C^{\prime}\) is a _spurious contrastive example_: the first \(i-1\) steps in \(\mathcal{E}\), and the constraints that the transition relation imposes, prevent the features freed by \(C^{\prime}_{i}\) from causing any action besides \(a_{i}\) to be selected in step \(i\).

Fig. 9 illustrates the three cases. The first case is identical to the one from Fig. 5, where \((\{s^{3}\})\) is a dependent contrastive example of the second step, which depends on the previous step and is part of a larger contrastive example: \((\{s^{3}\},\{s^{3}\})\). In the second case, assume that \(T\) requires that \(s^{1}_{3}+s^{2}_{3}\neq 1\) for any feasible transition. Thus, the assignment for \(s^{2}_{3}\) which may cause the second action in the sequence to change is not reachable from the previous step, and hence \((\{s^{3}\})\) is a spurious contrastive example of the second step. In the third case, assume that \(T\) allows all transitions, and hence \((\{s^{3}\})\) is an independent contrastive example for the second step; and so \((\varnothing,\{s^{3}\})\) is a contrastive example of the entire execution.

It follows from Lemma 2 that one of these three cases must always apply. We next explain how verification can be used to classify each contrastive example of a subset of steps into one of these three categories. If \(C^{\prime}\) is independent, it can be used as-is in computing the MHS; and if it is spurious, it should be ignored. In the case where \(C^{\prime}\) is dependent, our goal is to find all multi-step contrastive examples that contain it, for the purpose of computing the MHS. We next describe a recursive algorithm, termed _reverse incremental enumeration_ (RIE), that achieves this.

**Reverse Incremental Enumeration.** Given a contrastive example \(C^{\prime}\) containing features from a set of subsequent steps of \(\mathcal{E}\), we propose to classify it into one of the three categories by iteratively dispatching queries that check the reachability of \(C^{\prime}\) from the previous steps of the sequence. We execute this procedure by recursively enumerating contrastive examples in previous steps. For simplicity, we assume again that \(C^{\prime}=(C^{\prime}_{i})\) is a single-step contrastive example of step \(i\).

1. For checking whether \(C^{\prime}\) is an independent contrastive example of \(\mathcal{E}\), we set \(C_{i-1}=\varnothing\) and \(C_{i}=C^{\prime}_{i}\), and check whether \(C=(C_{i-1},C_{i})\) is a contrastive example for steps \(i-1\) and \(i\). This is achieved by dispatching the following query: \(\exists x_{i-1},x_{i}\in\mathbb{F}\) such that: \[\begin{split}& T(x_{i-1},N(x_{i-1}),x_{i})\wedge\\ &\quad\big{(}\bigwedge_{l=i-1}^{i}\bigwedge_{j\in\mathcal{F}\smallsetminus C _{l}}(x_{l}^{j}=s_{l}^{j})\big{)}\wedge(N(x_{i})\neq a_{i})\end{split}\] (7) If the verifier returns SAT, \(C^{\prime}_{i}\) is independent of step \(i-1\), and hence independent of all steps \(1,\ldots,i-1\). Hence, \(C^{\prime}\) is an independent contrastive example of \(\mathcal{E}\).
2. If the query from Eq. 7 returns UNSAT, we now attempt to decide whether \(C^{\prime}\) is dependent. We achieve this through additional verification queries, again setting \(C_{i}=C^{\prime}_{i}\), but now setting \(C_{i-1}\) to a _non empty_ set of features -- once for every possible set of features, separately. We again generate a query using the encoding from Eq. 7, and if the verifier returns SAT it follows that \(C^{\prime}\) is dependent on step \(i-1\), and that \(C^{\prime\prime}=(C_{i-1},C_{i})\) is a contrastive example for steps \(i-1\) and \(i\). We recursively continue with this enumeration process, to determine whether \(C^{\prime\prime}\) is independent, dependent of step \(i-2\), or a spurious contrastive example.
3. In case the previous phases determine that \(C^{\prime}\) is neither independent nor part of a larger contrastive example, we conclude that it is spurious.

An example of a single reverse incremental enumeration step on a contrastive example \(C^{\prime}\) in our running example is depicted in Fig. 10, and its recursive call is shown in Alg. 5 (Cxps denotes the set of all multi-step contrastive examples containing the initial \(C^{\prime}\)).

```
1:if\(\varnothing\)=1then
2:returnC'\(\triangleright\)C' is trivially independent of steps \(j\!<\!1\)
3:if\((\varnothing,C^{\prime}_{j},\ldots,C^{\prime}_{i})\) is a contrastive example of steps \(j-1\ldots i\)then
4:return\((C_{l}\mid\forall 1\leq l\leq j-1,\ C_{l}=\varnothing)\cdot C^{\prime}\)\(\triangleright\)C' is independent of step \(j-1\)
5:Cxps\(\leftarrow\varnothing\)
6:for each subset \(C_{f}\) of F do
7:if\((C_{f},C^{\prime}_{j},\ldots,C^{\prime}_{i})\) is a contrastive example of steps \(j-1\ldots i\)then
8:Cxps\(\leftarrow\)Cxps\(\cup\)RIE(\(i,j-1,C_{f}\))\(\triangleright\)C' is dependent of step \(j-1\)
9:returnCxps\(\triangleright\) if Cxps is empty, C' is spurious
```

**Algorithm 5**Reverse Incremental Enumeration (RIE)

Using reverse incremental enumeration, we can find all multi-step contrastive examples of \(\mathcal{E}\):

1. First, we find all contrastive examples for the first step of \(\mathcal{E}\). This is again the same as finding contrastive examples of a "one-shot" classification problem, and can be performed efficiently [17], via Alg. 7. We first enumerate all contrastive examples of size \(1\) (i.e., contrastive _singletons_); then all contrastive examples of size \(2\) that do not contain contrastive singletons within them; and then continue this process for all \(1\leq i\leq|F|\) ("skipping" all non-minimal cases).
2. Next, we search for all contrastive examples for the second step of \(\mathcal{E}\), in the same manner. We perform a reverse incremental enumeration on each contrastive example found, obtaining all contrastive examples for steps 1 and 2.
3. We continue iteratively, each time visiting a new step \(i\) and reversely enumerating all contrastive examples that affect steps \(1,\ldots,i\). We stop when we reach the final step, \(i=k\).

The full enumeration process for finding all contrastive examples of \(\mathcal{E}\) is described fully in Alg. 6, which invokes Alg. 7.
We also make the following observation: we can further expedite the enumeration process by discarding sets that contain contrastive examples within them since we are specifically searching for minimal contrastive examples. For instance, in the given example in Fig. 10, if we find \((\varnothing,s^{1},\varnothing)\) as a contrastive example for the entire multi-step instance, we no longer need to consider sets in step \(2\) that contain \(s^{1}\) when iterating in reverse from step \(3\) to step \(2\). Our evaluation shows that this approach can significantly improve performance as the increasing number of contrastive examples found in previous steps greatly reduces the search space.

Of course, our approach's worst-case complexity is still exponential in the number of steps, \(k\), because each dependent contrastive example requires a recursive call that potentially enumerates all contrastive examples for the previous step. However, the number of recursive iterations is limited by the dependency between steps. For instance, if contrastive examples in step \(i\) are only dependent on step \(i\) - \(1\) and

Fig. 10: An illustration of reverse incremental enumeration. We start with a single-step contrastive example, \(C^{\prime}_{3}=\{s^{3}\}\) for the third step of the execution. In the second iteration, we find that \((C^{\prime}_{3})\) is dependent on the previous step, and that \((\{s^{3}\},\{s^{3}\})\) constitutes a contrastive example for steps 2 and 3. In the third iteration, \(\big{(}\{s^{3}\},\{s^{3}\}\big{)}\) is found to be independent of the first step, and hence \((\varnothing,\{s^{3}\},\{s^{3}\})\) is a contrastive example for \(\mathcal{E}\).

Fig. 9: \((\{s^{3}\})\) as a dependent, spurious and independent contrastive example.
not on step \(i-2\), the recursive iterations will be limited to \(2\). Additionally, skipping the verification of candidates containing contrastive examples found in previous steps can also significantly reduce runtime.

## V Evaluation

**Implementation and Setup.** We created a proof-of-concept implementation of all aforementioned approaches and benchmarks [16]. To search for explanations, our tool [16] dispatches verification queries using a backend DNN verifier (we use _Marabou_[56], previously employed in additional studies [3, 4, 5, 21, 83], although other engines may also be used). The queries encode the architecture of the DNN in question, the transition constraints between consecutive steps of the reactive system, and the candidate explanation or contrastive example being checked. Calculating the MHS, when relevant, was done using RC-2, a MaxSAT-based tool of the PySat toolkit [45].

**Benchmarks.** We trained DRL agents for two well-known reactive system benchmarks: GridWorld [97] and TurtleBot [99] (see Fig. 11). GridWorld involves an agent moving in a 2D grid, while TurtleBot is a real-world robotic navigation platform. These benchmarks have been extensively studied in the DRL literature. GridWorld has 8 input features per state, including agent coordinates, target coordinates, and sensor readings for obstacle detection. The agent can take \(4\) possible actions: UP, DOWN, LEFT, or RIGHT. TurtleBot has \(9\) input features per state, including lidar sensor readings, target distance, and target angle. The agent has \(3\) possible actions: LEFT, RIGHT, or FORWARD. We trained our DRL agents with the state-of-the-art PPO algorithm [88]. Additional details appear in Sec. V and VI of the appendix.

**Generating Executions.** We generated 200 unique multi-step executions of our two benchmarks: \(100\) GridWorld executions (using \(10\) agents, each producing \(10\) unique executions of lengths \(6\leq k\leq 14\)), and \(100\) TurtleBot executions (using \(100\) agents, each producing a single execution of length \(6\leq k\leq 8\)). Next, from each \(k\)-step execution, we generated \(k\) unique sub-executions, each representing the first \(i\) steps of the original execution (\(1\leq i\leq k\)). This resulted in a total of \(931\) GridWorld executions and \(647\) Turtlebot executions. We used these executions to assess the different methods for finding minimal and minimum explanations. Each experiment ran with a timeout value of \(3\)-\(i\) hours, where \(i\) is the execution's length.

**Experiments.** We begin by comparing the performance of the four methods discussed in Sec. IV: (i) encoding the entire network as a "one-shot" query; (ii) computing individual explanations for each step; (iii) incrementally enumerating explanations; and (iv) reversely enumerating contrastive examples and calculating their MHS. We note that we use Methods 1-3 to generate both minimal and minimum explanations, whereas Method \(4\) is only used to generate minimum explanations. To generate minimum explanations using the "one-shot" encodings of Methods \(1\) and \(2\), we use the state-of-the-art approach of Ignatiev et al. [47]. We use two common criteria for comparison [47, 17, 46]: the _size_ of the generated explanations (small explanations tend to be more meaningful), and the overall runtime and timeout ratios.

**Results.** Results for the GridWorld benchmark are presented in Table I. These results clearly indicate that Method 2 (generating explanations in independent steps) was significantly faster in all experiments, but generated drastically larger explanations -- about two times larger when searching for a _minimal_ explanation, and about five times larger for a _minimum_ explanation, on average. This is not surprising; as noted earlier, the explanations produced by such an approach do not take the transition constraints into account, and hence, may be quite large. In addition, we note again that this approach does not guarantee the minimality of the combined explanation, even when combining minimal/minimum explanations for each step. The corresponding results for TurtleBot appear in Sec. VII of the appendix, and also demonstrate similar outcomes.

When comparing the three approaches that can guarantee minimal explanations, the incremental enumeration approach (Method 3) is clearly more efficient than the "one-shot" scheme (running for about \(1\) second compared to above \(5\) minutes, on average, across all solved instances), as depicted in Fig. 12. For the minimum explanation comparison, the results show that the reversed-enumeration-based strategy (Method 4) ran significantly faster than all other methods that can find guaranteed minimum explanations: on average, it ran for \(39\) seconds, while the other methods ran for more than \(6\) and \(23\) minutes. In addition, out of all methods guaranteed

\begin{table}
\begin{tabular}{c||c||c||c c c||c} \hline \hline \multirow{2}{*}{**setting**} & \multirow{2}{*}{**experiment**} & **time (s)** & \multicolumn{3}{c||}{**size**} & **solved** \\  & & **avg.** & **min** & **avg.** & **max** & **(\%)** \\ \hline \multirow{3}{*}{\begin{tabular}{c} minimal \\ (local) \\ \end{tabular} } & one-shot (1) & 304 & 5 & 33 & 112 & 98 \\  & independent (2) & 1 & 5 & 34 & 97 & 99.9 \\  & **incremental (3)** & **1** & **5** & **18** & **78** & **99.7** \\ \hline \multirow{3}{*}{
\begin{tabular}{c} minimum \\ (global) \\ \end{tabular} } & one-shot (1) & 405 & 5 & 14 & 32 & 29.8 \\  & independent (2) & 4 & 5 & 35 & 98 & 98.3 \\ \cline{1-1}  & incremental (3) & 1,396 & 5 & 7 & 9 & 17.9 \\ \cline{1-1}  & **reversed (4)** & **39** & **5** & **7** & **16** & **99.7** \\ \hline \hline \end{tabular}
\end{table} TABLE I: _GridWorld_: columns from left to right: experiment type, method name (and number), time and size of returned explanation (out of experiments that terminated), and the percent of solved instances (the rest timed out). The bold highlighting indicates the method that generated the explanation with the optimal size.

Fig. 11: Benchmarks: (A) GridWorld; and (B) TurtleBot.
to produce a minimum explanation, experiments that ran with the "reversed" strategy hit significantly fewer timeouts. The "reversed" strategy outperforms the competing methods significantly, on both benchmarks (see Fig. 13).

Next, we analyzed the strategies at a higher resolution -- focusing on a _step-wise_ level comparison, i.e., on analyzing how the length of the execution affected runtime. The results (see Figs. 17- 20 of the appendix) demonstrate the drastic performance gain of our "reversed" strategy as \(k\) increases: this strategy can efficiently find explanations for longer executions, while the competing "one-shot" strategy fails. This again is not surprising: when dealing with large numbers of steps, the transition function, the unrolling of the network, and the underlying enumeration scheme become more taxing on the underlying verifier. A full analysis of both benchmarks, and all explanation types, appears in Sec. VII of the appendix.

**Explanation Example.** We provide a visual example of an instance from our GridWorld experiment identified as a minimum explanation. The results (depicted in Fig. 14) include a minimum explanation for an execution of \(8\) steps. They show the following meaningful insight: fixing part of the agent's location sensors at the initial step, and a single sensor in the sixth step, is sufficient for forcing the agent to move along the original path, regardless of any other sensor reading.

**Comparison to Heuristic XAI Methods.** We also compared our results to popular, non-verification-based, heuristic XAI methods. Although these methods proved scalable, they often returned unsound explanations when compared to our approach. For additional details, see Section VIII of the appendix.

## VI Related Work

This work joins recent efforts on utilizing formal verification to explain the decisions of ML models [17, 28, 47, 59, 92, 93, 104]. Prior studies primarily focused on formally explaining _classification_ over various domains [17, 47, 48, 49, 104] or specific model types [38, 43, 49, 51, 71]. while others explored alternative ways of defining explanations over classification tasks [9, 37, 52, 59, 74, 81, 104, 101].

Methods closer to our own have focused on formally explaining DNNs [17, 40, 47, 59, 104], where the problem is known to be complex [47, 65]. This work relies on the rapid development of DNN verification [1, 13, 30, 33, 55, 57, 105]. There has also been ample work on heuristic XAI [34, 85, 86, 89, 34], including approaches for explaining the decisions of reinforcement-learning-based reactive systems (XRL) [35, 54, 69, 82]. However, these methods do not provide formal guarantees.

## VII Conclusion

Although DNNs are used extensively within reactive systems, they remain "black-box" models, uninterpretable to humans. We seek to mitigate this concern by producing formal explanations for executions of reactive systems. As far as we are aware, we are the first to provide a formal basis of explanations in this context, and to suggest methods for efficiently producing such explanations -- significantly outperforming the competing approaches. We also note that our approach is agnostic to the type of reactive system, and can be generalized beyond DRL systems, to any k-step reactive DNN system (including RNNs, LSTMs, GRUs, etc.). Moving forward, a main extension could be scaling our method, beyond the simple DRLs evaluated here, to larger systems of higher complexity. Another interesting extension could include evaluating the attribution of the hidden-layer features, rather than just the input features.

Fig. 14: _GridWorld_: a \(5\)-sized explanation for an \(8\)-step execution. The steps are numbered (in blue circles), the target is the yellow square, and the obstacles are depicted in red.

Fig. 12: _Minimal explanation_: number of solved instances depending on (accumulative) time, for the methods that guarantee minimality.

Fig. 13: _Minimum explanation_: number of solved instances depending on (accumulative) time, for the methods that guarantee minimality.
**Acknowledgments.** The work of Bassan, Amir, Refaeli, and Katz was partially supported by the Israel Science Foundation (grant number 683/18). The work of Amir was supported by a scholarship from the Clore Israel Foundation. The work of Corsi was partially supported by the "Dipartimenti di Eccellenza 2018-2022" project, funded by the Italian Ministry of Education, Universities, and Research (MIUR).
