2025/06/05 by Baier, Christel, Klatt, Rio, Klüppelholz, Sascha +1
#FOS: Computer and information sciences #Formal Languages and Automata Theory (cs.FL)
paper · doi:10.48550/arxiv.2506.05192
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 the Shapley value 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 backward responsibility for reachability, Büchi and parity objectives. For Büchi objectives, a polynomial algorithm is given to determine the set of responsible states. To analyse systems that are too large for standard methods, the paper presents a novel refinement algorithm that iteratively computes responsibility and demonstrates its utility with a prototypical implementation.