Article (Scientific journals)
Multi-valued Verification of Strategic Ability
Jamroga, Wojciech; Konikowska, Beata; Kurpiewski, Damian et al.
2020In Fundamenta Informaticae, 175 (1-4), p. 207-251
Peer reviewed


Full Text
Author preprint (665.29 kB)
Request a copy

All documents in ORBilu are protected by a user license.

Send to


Abstract :
[en] Some multi-agent scenarios call for the possibility of evaluating specifications in aricher domain of truth values. Examples include runtime monitoring of a temporal property over a growing prefix of an infinite path, inconsistency analysis in distributed databases, and verification methods that use incomplete anytime algorithms, such as bounded model checking. In this paper, we present multi-valued alternating-time temporal logic(mv-ATL∗→), an expressive logic to specify strategic abilities in multi-agent systems. It is well known that, for branching-time logics, a general method for model-independent translation from multi-valued to two-valued model checking exists. We show that the method cannot be directly extended to mv-ATL∗→. We also propose two ways of overcoming the problem. Firstly, we identify constraints on formulas for which the model-independent translation can be suitably adapted. Secondly, we present a model-dependent reduction that can be applied to all formulas of mv-ATL∗→. We show that, in all cases, the complexity of verification increases only linearly when new truth values are added to the evaluation domain. We also consider several examples that show possible applications of mv-ATL∗→and motivate its use for model checking multi-agent systems.
Disciplines :
Computer science
Author, co-author :
Jamroga, Wojciech ;  University of Luxembourg > Interdisciplinary Centre for Security, Reliability and Trust (SNT) > APSIA
Konikowska, Beata
Kurpiewski, Damian
Penczek, Wojciech
External co-authors :
Language :
Title :
Multi-valued Verification of Strategic Ability
Publication date :
Journal title :
Fundamenta Informaticae
Volume :
Issue :
Pages :
Peer reviewed :
Peer reviewed
Focus Area :
Security, Reliability and Trust
FnR Project :
FNR12685695 - Socio-technical Verification Of Information Security And Trust In Voting Systems, 2018 (01/09/2019-31/08/2022) - Peter Y. A. Ryan
Available on ORBilu :
since 24 January 2021


Number of views
60 (0 by Unilu)
Number of downloads
0 (0 by Unilu)

Scopus citations®
Scopus citations®
without self-citations
WoS citations


Similar publications

Contact ORBilu