Local Basic Strategy Logic
Valentin Goranko
Basic Strategy Logic (BSL) introduced in [1] is a minimal system of strategy logic of the type studied in [2]. BSL builds on a fixed set of agents \(\mathsf{Agt}\) and on some (usually temporalized) language for expressing agents goals, such as LTL, that defines a set of goal formulae \(\Gamma\) which are evaluated on plays in concurrent game models.
The language of BSL extends \(\Gamma\) with standard Boolean connectives and associates with each agent \(\mathsf{a} \in \mathsf{Agt}\) a strategy variable, denoted by \(\mathsf{x}_{\mathsf{a}}\). These variables range over strategies for the respective agents and can be quantified over within the formulae of BSL. Thus, BSL can be used for formalising the reasoning about strategic abilities of agents (players) and coalitions in concurrent multi-player games. It is shown in [1] that BSL is sufficiently expressive to capture many naturally defined recently studied operators and logics for strategic abilities.
In the present work I study its local version LBSL, which only involves in the language of \(\Gamma\) the Nexttime temporal operator, referring to the immediate outcomes states from playing single-round concurrent games at the states of the model. I explore and characterise the expressiveness of LBSL, study its validities, present an axiomatic system for them, and discuss the problems of its completeness and of the decidability of LBSL.
Bibliography
- V. Goranko Logics for Strategic Reasoning of Socially Interacting Rational Agents: An Overview and Perspectives. Logics, vol. 1(1), 2023. Online publication: https://www.mdpi.com/2813-0405/1/1/3.
- Fabio Mogavero, Aniello Murano, and Moshe Y. Vardi. Reasoning about strategies. In Proc. of {FSTTCS} 2010, volume 8 of LIPIcs, pages 133–144.