English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

In open systems verification, to formally check for reliability, one needs anappropriate formalism to model the interaction between agents and express thecorrectness of the system no matter how the environment behaves. An importantcontribution in this context is given by modal logics for strategic ability, inthe setting of multi-agent games, such as ATL, ATL\star, and the like.Recently, Chatterjee, Henzinger, and Piterman introduced Strategy Logic, whichwe denote here by CHP-SL, with the aim of getting a powerful framework forreasoning explicitly about strategies. CHP-SL is obtained by using first-orderquantifications over strategies and has been investigated in the very specificsetting of two-agents turned-based games, where a non-elementary model-checkingalgorithm has been provided. While CHP-SL is a very expressive logic, we claimthat it does not fully capture the strategic aspects of multi-agent systems. Inthis paper, we introduce and study a more general strategy logic, denoted SL,for reasoning about strategies in multi-agent concurrent games. We prove thatSL includes CHP-SL, while maintaining a decidable model-checking problem. Inparticular, the algorithm we propose is computationally not harder than thebest one known for CHP-SL. Moreover, we prove that such a problem for SL isNonElementarySpace-hard. This negative result has spurred us to investigatehere syntactic fragments of SL, strictly subsuming ATL\star, with the hope ofobtaining an elementary model-checking problem. Among the others, we study thesublogics SL[NG], SL[BG], and SL[1G]. They encompass formulas in a specialprenex normal form having, respectively, nested temporal goals, Booleancombinations of goals and, a single goal at a time. About these logics, weprove that the model-checking problem for SL[1G] is 2ExpTime-complete, thus notharder than the one for ATL\star.

Reasoning About Strategies: On the Model-Checking Problem