Responsibility in Actor-Based Systems

TL;DR

This work tackles the challenge of explainability in complex systems by formalizing responsibility notions for reactive systems using Shapley values. It presents forward and backward responsibility, defined via safety games, and introduces three actor-generation schemes—module-based, value-based, and action-based—each supported by model-transformations (scheduler and action-separation) that preserve safety invariants. The paper provides complexity results (e.g., NP-complete positivity, NP-hard threshold, #P-hard computation) and reports on a Prism-backed experimental evaluation, including a Bounded Retransmission Protocol case study, to illustrate debugging utility and scalability with modest actor counts. Overall, the approach enables pinpointing influential components or actions to improve correctness and guide debugging in verification workflows, with potential integration into model-checking pipelines for practical impact.

Abstract

The enormous growth of the complexity of modern computer systems leads to an increasing demand for techniques that support the comprehensibility of systems. This has motivated the very active research field of formal methods that enhance the understanding of why systems behave the way they do. One important line of research within the verification community relies on formal notions that measure the degree of responsibility of different actors. In this paper, we first provide a uniform presentation of recent work on responsibility notions based on Shapley values for reactive systems modeled by transition systems and considering safety properties. The paper then discusses how to use these formal responsibility notions and corresponding algorithms for three different types of actor sets: the module-based notion serves to reason about the impact of system components on the satisfaction or violation of a safety property. Responsibility values for value-based actor sets and action-based actors allow for the identification of program instructions and control points that have the most influence on a specification violation. Beyond the theoretical considerations, this paper reports on experimental results that provide initial insights into applicability and scalability.

Figures (8)

• Figure 1: Model of the tracks leading into a train station. The switches are controlled by the three controllers Alice, Bob and Charlie. The train must not reach $\lightning$, as this track is already occupied.
• Figure 2: Example program in the reactive modules language
• Figure 3: Model of Ada and Julia throwing rocks at a potentially rock-proof window
• Figure 4: Model of Ada and Rebeca's drive from Malmö to Västerås.
• Figure 5: Action-separation transformation applied to a state with three actions.

Theorems & Definitions (20)

• definition thmcounterdefinition: Actor
• definition thmcounterdefinition: Safety games for coalitions of agents -- forward
• definition thmcounterdefinition: Safety games for coalitions of agents -- backward
• definition thmcounterdefinition: Foward and backward cooperative games
• definition thmcounterdefinition: Responsibility
• remark thmcounterremark
• remark thmcounterremark
• proposition thmcounterproposition: Complexity of the positivity problem
• proposition thmcounterproposition: Complexity of the threshold and the computation problem
• definition thmcounterdefinition: Module and action guards