Backward Responsibility in Transition Systems Beyond Safety

TL;DR

This paper advances the understanding of backward responsibility in transition systems by establishing complexity bounds, providing polynomial algorithms for B"uchi objectives, and introducing a refinement method for large systems.

Contribution

It offers tight complexity bounds, a polynomial algorithm for responsible states in B"uchi objectives, and a novel refinement approach for large systems, enhancing responsibility analysis methods.

Findings

Polynomial algorithm for responsible states in B"uchi objectives.

Refinement algorithm effectively handles large systems.

Heuristics improve the efficiency of responsibility computation.

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\"uchi and parity objectives. For B\"uchi 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.