Notice: The reproducibility variables underlying each score are classified using an automated LLM-based pipeline, validated against a manually labeled dataset. LLM-based classification introduces uncertainty and potential bias; scores should be interpreted as estimates. Full accuracy metrics and methodology are described in Coakley et alK. L. Coakley, T. Snelleman, H. Hoos, and O. E. Gundersen, "The embrace of open science: An analysis of a decade of AI research and 56 800 conference papers," Under Review, 2026..
Satisfiability in Strategy Logic Can Be Easier than Model Checking
Authors: Erman Acar, Massimo Benerecetti, Fabio Mogavero2638-2645
AAAI 2019 | Venue PDF | 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. |