Authors: Patrick Gardy, Patricia Bouyer and Nicolas Markey
Paper Information
Title: | Dependences in Strategy Logic |
Authors: | Patrick Gardy, Patricia Bouyer and Nicolas Markey |
Proceedings: | SR SR18 papers |
Editors: | Nicolas Markey and Patricia Bouyer |
Keywords: | strategy logic, elementary semantics, skolemization, dependence maps, parity games |
Abstract: | ABSTRACT. Strategy Logic (SL) is a very expressive temporal logic for specifying and verifying properties of multi-agent systems: in SL, one can quantify over strategies, assign them to agents, and express LTL properties of the resulting plays. Such a powerful framework has two drawbacks: first, model checking SL has non-elementary complexity; second, the exact semantics of SL is rather intricate, and may not correspond to what is expected. In this paper, we focus on strategy dependences in SL, by tracking how existentially-quantified strategies in a formula may (or may not) depend on other strategies selected in the formula, revisiting the approach of [Mogavero et al., Reasoning about strategies: On the model-checking problem, 2014]. We explain why elementary dependences, as defined by Mogavero et al., do not exactly capture the intended concept of behavioral strategies. We address this discrepancy by introducing timeline dependences, and exhibit a large fragment of SL for which model checking can be performed in 2EXPTIME under this new semantics. |
Pages: | 14 |
Talk: | Jul 08 17:20 (Session 42Q: Strategy Logic) |
Paper: |