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üchi and parity objectives. For Büchi 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.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Backward Responsibility in Transition Systems Beyond Safety

  • Christel Baier,
  • Rio Klatt,
  • Sascha Klüppelholz,
  • Johannes Lehmann

摘要

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üchi and parity objectives. For Büchi 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.