Backward Responsibility in Transition Systems Beyond Safety

TL;DR

This paper provides tight complexity bounds for the computation of backward responsibility values for reachability, Buchi and parity objectives and presents a novel refinement algorithm that iteratively finds the set of responsible states.

Abstract

As the complexity of software systems rises, methods for explaining their behaviour are becoming ever-more important. When a system fails, it is critical to determine which of its components are responsible for this failure. Within the verification community, one approach uses graph games and Shapley values to ascribe a responsibility value to every state of a transition system. As this is done with respect to a specific failure, it is called backward responsibility. This paper provides tight complexity bounds for the computation of backward responsibility values for reachability, Büchi and parity objectives. For Büchi objectives, a polynomial algorithm is given to determine the set of responsible states, i.e. states with positive responsibility value. To analyse systems that are too large for standard methods, the paper presents a novel refinement algorithm that iteratively finds the set of responsible states. Several heuristics are proposed to guide the refinement algorithm. Its utility is demonstrated with a tool that implements refinement in addition to several other responsibility computation techniques.

Figures (12)

• Figure 1: Engraving path $\rho = s_0 s_2 s_4 \lightning^\omega$ in a transition system with objective $\square \lnot \lightning$, with coalition $C=\{s_4\}$. Outgoing transitions of the states of $\rho$ are removed if they do not follow $\rho$, except for $s_4$, because $s_4 \in C$.
• Figure 2: A transition system with Büchi objective $\square\lozenge \{s_2, s_5\}$ and violating run $\rho s_0 s_1 s_2 s_3^\omega$. The corresponding optimistic and pessimistic responsibility values are depicted on the right. Unlike for safety and reachability, not all states with positive optimistic responsibility have the same amount of responsibility.
• Figure 3: For Büchi objectives, minimal non-singleton winning coalitions matches the depicted layout. Each arrow $s \rightarrow t$ indicates that there is a path from $s$ to $t$, potentially visiting other states that are not depicted.
• Figure 4: The winning run in this transition system with parity objective requires jumping "forward" from $s_1$ to $s_3$, which is never required for Büchi objectives.
• Figure 5: Transition system with Büchi objective $\square \lozenge \{s_f\}$ that has exponentially many minimal winning coalitions.

Theorems & Definitions (34)

• definition thmcounterdefinition: Engraving construction
• definition thmcounterdefinition: Graph game
• definition thmcounterdefinition: Responsibility values
• remark thmcounterremark
• lemma thmcounterlemma: Responsible states for optimistic responsibility
• proof
• definition thmcounterdefinition: Responsibility problems
• proposition thmcounterproposition
• proof
• proposition thmcounterproposition