Responsibility and verification: Importance value in temporal logics

TL;DR

This paper introduces a method using Shapley values to quantify the influence of system components on satisfying specifications in model-checking, providing a new perspective on importance measurement in temporal logics.

Contribution

It applies Shapley values to verification, offering a novel approach to measure component importance and analyzing its complexity across different types of temporal logics.

Findings

Shapley values effectively quantify component importance in system verification.

Complexity bounds are established for various temporal logic types.

Methods are proposed for extending importance measures to branching temporal logics.

Abstract

We aim at measuring the influence of the nondeterministic choices of a part of a system on its ability to satisfy a specification. For this purpose, we apply the concept of Shapley values to verification as a means to evaluate how important a part of a system is. The importance of a component is measured by giving its control to an adversary, alone or along with other components, and testing whether the system can still fulfill the specification. We study this idea in the framework of model-checking with various classical types of linear-time specification, and propose several ways to transpose it to branching ones. We also provide tight complexity bounds in almost every case.