scholarly journals Extended Graded Modalities in Strategy Logic

2016 ◽  
Vol 218 ◽  
pp. 1-14 ◽  
Author(s):  
Benjamin Aminof ◽  
Vadim Malvone ◽  
Aniello Murano ◽  
Sasha Rubin
Keyword(s):  
Strategy Logic ◽  
Graded Modalities

scholarly journals Graded modalities in Strategy Logic

2018 ◽  
Vol 261 ◽  
pp. 634-649 ◽  
Author(s):  
Benjamin Aminof ◽  
Vadim Malvone ◽  
Aniello Murano ◽  
Sasha Rubin
Keyword(s):  
Strategy Logic ◽  
Graded Modalities

Graded modalities. I

Studia Logica ◽  
1985 ◽  
Vol 44 (2) ◽  
pp. 197-221 ◽  
Author(s):  
M. Fattorosi-Barnaba ◽  
F. De Caro
Keyword(s):  
Graded Modalities

scholarly journals Representation and Reasoning about Strategic Abilities with ω-Regular Properties

Mathematics ◽  
2021 ◽  
Vol 9 (23) ◽  
pp. 3052
Author(s):  
Liping Xiong ◽  
Sumei Guo
Keyword(s):  
Temporal Logic ◽  
Linear Time ◽  
Dynamic Logic ◽  
Research Area ◽  
Regular Expressions ◽  
Multi Agent Systems ◽  
Practical Applications ◽  
Multi Agent ◽  
Strategy Logic ◽  
Active Research

Specification and verification of coalitional strategic abilities have been an active research area in multi-agent systems, artificial intelligence, and game theory. Recently, many strategic logics, e.g., Strategy Logic (SL) and alternating-time temporal logic (ATL*), have been proposed based on classical temporal logics, e.g., linear-time temporal logic (LTL) and computational tree logic (CTL*), respectively. However, these logics cannot express general ω-regular properties, the need for which are considered compelling from practical applications, especially in industry. To remedy this problem, in this paper, based on linear dynamic logic (LDL), proposed by Moshe Y. Vardi, we propose LDL-based Strategy Logic (LDL-SL). Interpreted on concurrent game structures, LDL-SL extends SL, which contains existential/universal quantification operators about regular expressions. Here we adopt a branching-time version. This logic can express general ω-regular properties and describe more programmed constraints about individual/group strategies. Then we study three types of fragments (i.e., one-goal, ATL-like, star-free) of LDL-SL. Furthermore, we show that prevalent strategic logics based on LTL/CTL*, such as SL/ATL*, are exactly equivalent with those corresponding star-free strategic logics, where only star-free regular expressions are considered. Moreover, results show that reasoning complexity about the model-checking problems for these new logics, including one-goal and ATL-like fragments, is not harder than those of corresponding SL or ATL*.

scholarly journals Dependences in Strategy Logic

2020 ◽  
Vol 64 (3) ◽  
pp. 467-507
Author(s):  
Patrick Gardy ◽  
Patricia Bouyer ◽  
Nicolas Markey
Keyword(s):  
Strategy Logic

Graded modalities. III (the completeness and compactness of S40)

Studia Logica ◽  
1988 ◽  
Vol 47 (2) ◽  
pp. 99-110 ◽  
Author(s):  
M. Fattorosi-Barnaba ◽  
C. Cerrato
Keyword(s):  
Graded Modalities

scholarly journals Strategy logic with imperfect information

2017 ◽  
Author(s):  
Raphael Berthon ◽  
Bastien Maubert ◽  
Aniello Murano ◽  
Sasha Rubin ◽  
Moshe Y. Vardi
Keyword(s):  
Imperfect Information ◽  
Strategy Logic

Graded modalities, II (canonical models)

Studia Logica ◽  
1988 ◽  
Vol 47 (1) ◽  
pp. 1-10 ◽  
Author(s):  
Francesco De Caro
Keyword(s):  
Canonical Models ◽  
Graded Modalities

scholarly journals Probabilistic Strategy Logic

2019 ◽  
Author(s):  
Benjamin Aminof ◽  
Marta Kwiatkowska ◽  
Bastien Maubert ◽  
Aniello Murano ◽  
Sasha Rubin
Keyword(s):  
Model Checking ◽  
Nash Equilibria ◽  
Stochastic Systems ◽  
Solution Concepts ◽  
Imperfect Recall ◽  
Double Exponential ◽  
Temporal Operator ◽  
Standard Solution ◽  
Strategy Logic ◽  
Exponential Space

We introduce Probabilistic Strategy Logic, an extension of Strategy Logic for stochastic systems. The logic has probabilistic terms that allow it to express many standard solution concepts, such as Nash equilibria in randomised strategies, as well as constraints on probabilities, such as independence. We study the model-checking problem for agents with perfect- and imperfect-recall. The former is undecidable, while the latter is decidable in space exponential in the system and triple-exponential in the formula. We identify a natural fragment of the logic, in which every temporal operator is immediately preceded by a probabilistic operator, and show that it is decidable in space exponential in the system and the formula, and double-exponential in the nesting depth of the probabilistic terms. Taking a fixed nesting depth, this gives a fragment that still captures many standard solution concepts, and is decidable in exponential space.

Sign in / Sign up

Export Citation Format

Share Document