Satisfiability in Strategy Logic Can Be Easier than Model Checking
Authors: Erman Acar, Massimo Benerecetti, Fabio Mogavero2638-2645
AAAI 2019 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Theoretical | In this paper, we investigate the connection between the two problems for a non-trivial fragment of Strategy Logic (SL, for short). SL extends LTL with first-order quantifications over strategies, thus allowing to explicitly reason about the strategic abilities of agents in a multi-agent system. Satisfiability for the full logic is known to be highly undecidable, while model-checking is non-elementary. The SL fragment we consider is obtained by preventing strategic quantifications within the scope of temporal operators. The resulting logic is quite powerful, still allowing to express important game-theoretic properties of multi-agent systems, such as existence of Nash and immune equilibria, as well as to formalize the rational synthesis problem. We show that satisfiability for such a fragment is PSPACE-COMPLETE, while its model-checking complexity is 2EXPTIME-HARD. The result is obtained by means of an elegant encoding of the problem into the satisfiability of conjunctive-binding first-order logic, a recently discovered decidable fragment of first-order logic. |
| Researcher Affiliation | Academia | 1Vrije Universiteit Amsterdam, The Netherlands 2Universit a di Napoli Federico II , Italy |
| Pseudocode | Yes | Algorithm 1: FSL[CG] Satisfiability Procedure. signature sat: FSL[CG] B function sat(ϕ) |
| Open Source Code | No | The paper is theoretical and focuses on logical complexity and proofs; it does not mention releasing source code. |
| Open Datasets | No | The paper is theoretical and does not involve empirical datasets or training data. |
| Dataset Splits | No | The paper is theoretical and does not involve empirical data requiring validation splits. |
| Hardware Specification | No | The paper is theoretical and does not describe empirical experiments, thus no hardware specifications are provided. |
| Software Dependencies | No | The paper is theoretical and does not describe empirical experiments, thus no software dependencies with version numbers are provided. |
| Experiment Setup | No | The paper is theoretical and does not describe empirical experiments or specific hyperparameter/training settings. |