Withdraw
Loading…
Strategy Logic extended with Refinement, CGS, and Nondeterminism
Griffith, Dennis; Gunter, Elsa L.
Content Files

Loading…
Download Files
Loading…
Download Counts (All Files)
Loading…
Edit File
Loading…
Permalink
https://hdl.handle.net/2142/35276
Description
- Title
- Strategy Logic extended with Refinement, CGS, and Nondeterminism
- Author(s)
- Griffith, Dennis
- Gunter, Elsa L.
- Issue Date
- 2012-11-30
- Keyword(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.
- Type of Resource
- text
- Language
- en
- Permalink
- http://hdl.handle.net/2142/35276
Owning Collections
Manage Files
Loading…
Edit Collection Membership
Loading…
Edit Metadata
Loading…
Edit Properties
Loading…
Embargoes
Loading…