Reasoning about Quality and Fuzziness of Strategic Behaviors

Temporal logics are extensively used for the specification of on-going behaviors of computer systems. Two significant developments in this area are the extension of traditional temporal logics with modalities that enable the specification of on-going strategic behaviors in multi-agent systems, and t...

Full description

Saved in:
Bibliographic Details
Published in:ACM transactions on computational logic 2023-07, Vol.24 (3), p.1-38, Article 21
Main Authors: Bouyer, Patricia, Kupferman, Orna, Markey, Nicolas, Maubert, Bastien, Murano, Aniello, Perelli, Giuseppe
Format: Article
Language:English
Subjects:
Automata over infinite objects
Computer Science
Logic and verification
Modal and temporal logics
Theory of computation
Tree languages
Verification by model checking
Citations: Items that this one cites
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:Temporal logics are extensively used for the specification of on-going behaviors of computer systems. Two significant developments in this area are the extension of traditional temporal logics with modalities that enable the specification of on-going strategic behaviors in multi-agent systems, and the transition of temporal logics to a quantitative setting, where different satisfaction values enable the specifier to formalize concepts such as certainty or quality. In the first class, SL (Strategy Logic) is one of the most natural and expressive logics describing strategic behaviors. In the second class, a notable logic is LTL[ℱ] , which extends LTL with quality operators.In this work, we introduce and study SL[ℱ] , which enables the specification of quantitative strategic behaviors. The satisfaction value of an SL[ℱ] formula is a real value in [0,1], reflecting “how much” or “how well” the strategic on-going objectives of the underlying agents are satisfied. We demonstrate the applications of SL[ℱ] in quantitative reasoning about multi-agent systems, showing how it can express and measure concepts like stability in multi-agent systems, and how it generalizes some fuzzy temporal logics. We also provide a model-checking algorithm for SL[ℱ] , based on a quantitative extension of Quantified CTL⋆ . Our algorithm provides the first decidability result for a quantitative extension of Strategy Logic. In addition, it can be used for synthesizing strategies that maximize the quality of the systems’ behavior.
ISSN:1529-3785
1557-945X
DOI:10.1145/3582498