Responsibility and verification: Importance value in temporal logics

Corto MascleCorto Mascle, Christel BaierChristel Baier, Florian FunkeFlorian Funke, Simon JantschSimon Jantsch, Stefan KieferStefan Kiefer

DOI Link

Corto Mascle, Christel Baier, Florian Funke, Simon Jantsch, Stefan Kiefer
Responsibility and verification: Importance value in temporal logics
2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 1-14, 2021

Details
Bibtex

KurzfassungAbstract
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. We also provide tight complexity bounds in almost every case.
Forschungsgruppe:Research Group: Algebraische und logische Grundlagen der InformatikAlgebraic and Logical Foundations of Computer Science

@inproceedings{MBFJK2021,
  author    = {Corto Mascle and Christel Baier and Florian Funke and Simon
               Jantsch and Stefan Kiefer},
  title     = {Responsibility and verification: Importance value in temporal
               logics},
  booktitle = {2021 36th Annual {ACM/IEEE} Symposium on Logic in Computer
               Science (LICS)},
  year      = {2021},
  pages     = {1-14},
  doi       = {10.1109/LICS52264.2021.9470597}
}