Backward Responsibility in Transition Systems Beyond Safety
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.
Cite
@article{arxiv.2506.05192,
title = {Backward Responsibility in Transition Systems Beyond Safety},
author = {Christel Baier and Rio Klatt and Sascha Klüppelholz and Max Korn and Johannes Lehmann},
journal= {arXiv preprint arXiv:2506.05192},
year = {2026}
}