RECORD
Backward Responsibility in Transition Systems Using General Power Indices
Formal Languages and Automata Theory · Submitted 2 Feb 2024
abstract compiled · 2026-09-23 · no language-model review
The authors' main claim These methods can be deployed in the design phase, at runtime and at inspection time to gain insights on causal relations within the behavior of AI systems.
The compiled record
The paper's own sentences, arranged. Each label is drawn from a closed vocabulary; the number beside it is the probability the classifier gave that label. Numbers in the tables are the authors', checked by code. No sentence in this record was written by a model.
Open the compiled record
The abstract, sentence by sentence
To improve reliability and the understanding of AI systems, there is increasing interest in the use of formal methods, e.g. model checking. Model checking tools produce a counterexample when a model does not satisfy a property. Understanding these counterexamples is critical for efficient debugging, as it allows the developer to focus on the parts of the program that caused the issue. To this end, we present a new technique that ascribes a responsibility value to each state in a transition system that does not satisfy a given safety property. The value is higher if the non-deterministic choices in a state have more power to change the outcome, given the behaviour observed in the counterexample. For this, we employ a concept from cooperative game theory -- namely general power indices, such as the Shapley value -- to compute the responsibility of the states. We present an optimistic and pessimistic version of responsibility that differ in how they treat the states that do not lie on the counterexample. We give a characterisation of optimistic responsibility that leads to an efficient algorithm for it and show computational hardness of the pessimistic version. We also present a tool to compute responsibility and show how a stochastic algorithm can be used to approximate responsibility in larger models. These methods can be deployed in the design phase, at runtime and at inspection time to gain insights on causal relations within the behavior of AI systems.
background contribution method result interpretation main claim
| # | sentence | role | the authors' own work | states the main conclusion | strength |
|---|---|---|---|---|---|
| s0 | To improve reliability and the understanding of AI systems, there is increasing interest in the use of formal methods, e.g. model checking. | background 1.00 | 0.04 | 0.02 | asserted 0.98 |
| s1 | Model checking tools produce a counterexample when a model does not satisfy a property. | background 1.00 | 0.06 | 0.02 | asserted 1.00 |
| s2 | Understanding these counterexamples is critical for efficient debugging, as it allows the developer to focus on the parts of the program that caused the issue. | background 0.97 | 0.05 | 0.03 | asserted 1.00 |
| s3 | To this end, we present a new technique that ascribes a responsibility value to each state in a transition system that does not satisfy a given safety property. | contribution 1.00 | 0.94 | 0.31 | asserted 1.00 |
| s4 | The value is higher if the non-deterministic choices in a state have more power to change the outcome, given the behaviour observed in the counterexample. | method 0.84 | 0.57 | 0.11 | asserted 1.00 |
| s5 | For this, we employ a concept from cooperative game theory -- namely general power indices, such as the Shapley value -- to compute the responsibility of the states. | method 0.99 | 0.68 | 0.07 | asserted 1.00 |
| s6 | We present an optimistic and pessimistic version of responsibility that differ in how they treat the states that do not lie on the counterexample. | contribution 0.62 | 0.94 | 0.07 | asserted 1.00 |
| s7 | We give a characterisation of optimistic responsibility that leads to an efficient algorithm for it and show computational hardness of the pessimistic version. | contribution 0.62 | 0.96 | 0.21 | asserted 1.00 |
| s8 | We also present a tool to compute responsibility and show how a stochastic algorithm can be used to approximate responsibility in larger models. | contribution 0.85 | 0.96 | 0.11 | asserted 1.00 |
| s9 | These methods can be deployed in the design phase, at runtime and at inspection time to gain insights on causal relations within the behavior of AI systems. | interpretation 0.82 | 0.39 | 0.29 | hedged possibility 0.61 |
What was examined, and what was not
- arXiv listing abstract v1
- full text
- figures and tables
- references and citing sentences
- relations to other papers
- P abstract
- S sections
- T body sentences
- C citations
- R cross-paper relations
The paper
Original abstract
To improve reliability and the understanding of AI systems, there is increasing interest in the use of formal methods, e.g. model checking. Model checking tools produce a counterexample when a model does not satisfy a property. Understanding these counterexamples is critical for efficient debugging, as it allows the developer to focus on the parts of the program that caused the issue. To this end, we present a new technique that ascribes a responsibility value to each state in a transition system that does not satisfy a given safety property. The value is higher if the non-deterministic choices in a state have more power to change the outcome, given the behaviour observed in the counterexample. For this, we employ a concept from cooperative game theory -- namely general power indices, such as the Shapley value -- to compute the responsibility of the states. We present an optimistic and pessimistic version of responsibility that differ in how they treat the states that do not lie on the counterexample. We give a characterisation of optimistic responsibility that leads to an efficient algorithm for it and show computational hardness of the pessimistic version. We also present a tool to compute responsibility and show how a stochastic algorithm can be used to approximate responsibility in larger models. These methods can be deployed in the design phase, at runtime and at inspection time to gain insights on causal relations within the behavior of AI systems.
Human review
Discussion
Know something about this paper? Leave a comment, or highlight any passage above to comment on it.