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

Freitag, 4. August 2023, 14:30 Uhr

Ort: RWTH Aachen University, Informatikzentrum - Ahornstr. 55, Erweiterungsgebäude E3, Raum 9u10

Vortragender: 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.