Responsibility and verification: importance value in temporal logics

Research output: Contribution to book/conference proceedings/anthology/reportConference contributionContributed

Contributors

Abstract

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.

Details

Original languageEnglish
Title of host publication2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)
Pages1-14
Number of pages14
Publication statusPublished - 24 Nov 2021
Peer-reviewedNo

Publication series

SeriesProceedings - Symposium on Logic in Computer Science
Volume2021-June
ISSN1043-6871

Conference

Title36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)
Abbreviated titleLICS 2021
Conference number
Duration29 June - 2 July 2021
Degree of recognitionInternational event
Locationonline
CityRom
CountryItaly

External IDs

ORCID /0000-0002-5321-9343/work/142236690
Scopus 85108134191

Keywords

DFG Classification of Subject Areas according to Review Boards

Subject groups, research areas, subject areas according to Destatis