Responsibility and verification: Importance value in temporal logics

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. In the case of branching specifications, we are lead to a notion of tree games and study some tree language classes such that tree games with those languages as objectives are determined. This is joint work with Christel Baier, Florian Funke, Simon Jantsch, Stefan Kiefer and Karoliina Lehtinen. A paper was published at LICS 2021, but the talk will go further. A full version is available on Arxiv: https: //arxiv. org/abs/2102. 06655.

Authors

• Corto Mascle

Keywords

No keywords are indexed for this paper.