Backward Responsibility in Transition Systems Beyond Safety
Fuente:
arXiv
Saved in:
| Main Authors: | , , , , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866910027427610624 |
|---|---|
| author | Baier, Christel Klatt, Rio Klüppelholz, Sascha Korn, Max Lehmann, Johannes |
| author_facet | Baier, Christel Klatt, Rio Klüppelholz, Sascha Korn, Max Lehmann, Johannes |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2506_05192 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Backward Responsibility in Transition Systems Beyond Safety Baier, Christel Klatt, Rio Klüppelholz, Sascha Korn, Max Lehmann, Johannes Formal Languages and Automata Theory 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. |
| title | Backward Responsibility in Transition Systems Beyond Safety |
| topic | Formal Languages and Automata Theory |
| url | https://arxiv.org/abs/2506.05192 |