Kavli Affiliate: Johannes Lehmann
| First 5 Authors: Christel Baier, Rio Klatt, Sascha Klüppelholz, Johannes Lehmann,
| Summary:
As the complexity of software systems rises, methods for explaining their
behaviour are becoming ever-more important. When a system fails, it is critical
to determine which of its components are responsible for this failure. Within
the verification community, one approach uses graph games and the Shapley value
to ascribe a responsibility value to every state of a transition system. As
this is done with respect to a specific failure, it is called backward
responsibility.
This paper provides tight complexity bounds for backward responsibility for
reachability, B"uchi and parity objectives. For B"uchi objectives, a
polynomial algorithm is given to determine the set of responsible states. To
analyse systems that are too large for standard methods, the paper presents a
novel refinement algorithm that iteratively computes responsibility and
demonstrates its utility with a prototypical implementation.
| Search Query: ArXiv Query: search_query=au:”Johannes Lehmann”&id_list=&start=0&max_results=3