Responsibility in Actor-Based Systems

TL;DR

This paper reviews recent formal methods for measuring responsibility in actor-based systems, focusing on Shapley value-based notions, and demonstrates their practical application and scalability through experiments.

Contribution

It provides a unified presentation of responsibility notions based on Shapley values and explores their application to different actor types in reactive systems.

Findings

Responsibility measures help identify influential system components.

Algorithms are effective for analyzing safety property violations.

Experimental results show promising scalability and applicability.

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.