IDEALS Home University of Illinois at Urbana-Champaign logo The Alma Mater The Main Quad

Strategy Logic extended with Refinement, CGS, and Nondeterminism

Show full item record

Bookmark or cite this item: http://hdl.handle.net/2142/35276

Files in this item

File Description Format
PDF StrategyLogicExtensions.pdf (256KB) (no description provided) PDF
Title: Strategy Logic extended with Refinement, CGS, and Nondeterminism
Author(s): Griffith, Dennis; Gunter, Elsa L.
Subject(s): Formal methods concurrency temporal logics formal specification and verification
Abstract: In this paper, we introduce SLeRCN, an extension of Strategy Logic (SL). The extensions syntactic and semantic. The main syntactic extensions include lifting the restrictions in Chatterjee et al. [7] that formulae must be hierarchically closed. Semantic extensions include support for arbitrary numbers of player, concurrent game structures, and nondeterministic strategies. We show that the model checking problem decidable via tree automata, but our algorithm is nonelementary. For the restricted case of positional strategies the model checking problem is in EXPTIME. We show that ATL, SL, and Rely-Guarentee Temporal Logic (RGTL) can be embedded in SLeRCN. As a result we show that model checking for RGTL is decidable, a previously unknown result. Additionally, SLeRCN can be used to characterize the existence of Qualitative Nash Equilibria and Secure Equilibria.
Issue Date: 2012-11-30
Genre: Technical Report
Type: Text
Language: English
URI: http://hdl.handle.net/2142/35276
Publication Status: unpublished
Peer Reviewed: not peer reviewed
Date Available in IDEALS: 2012-11-30
 

This item appears in the following Collection(s)

Show full item record

Item Statistics

  • Total Downloads: 133
  • Downloads this Month: 6
  • Downloads Today: 0

Browse

My Account

Information

Access Key