Guest Talk: Johannes Lehmann: Counterexample-based backward responsibility in transition systems using the Shapley value

Friday, August 4, 2023, 2:30pm

Location: RWTH Aachen University, Department of Computer Science - Ahornstr. 55, building E3, room 9u10

Speaker: Johannes Lehmann

 

Abstract:

Model checking tools produce a counterexample when a model does not satisfy a property. Our goal is to explain what lead to this specific execution. Because this explanation is done after the model is executed, we call it backward responsibility.

More precisely, given a transition system with a safety property and a run violating this safety property, our goal is to quantify the impact the non-deterministic choices in each state have on the result. For this, we employ the Shapley value, which is a concept from cooperative game theory.

We investigate two versions of this responsibility metric that differ in how they resolve non-determinism. We show that the one version can be computed efficiently, while the other version is computationally hard. Finally, we present an implementation that computes backward responsibility using the output of the model checker PRISM.