Strategic Reasoning with a Bounded Number of Resources: the Quest for Tractability

Autor: Francesco Belardinelli, Stéphane Demri
Přispěvatelé: Department of Computing [Imperial College London], Imperial College London, Informatique, BioInformatique, Systèmes Complexes (IBISC), Université d'Évry-Val-d'Essonne (UEVE)-Université Paris-Saclay, Laboratoire Méthodes Formelles (LMF), Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), Centre National de la Recherche Scientifique (CNRS), Francesco Belardinelli acknowledges the support of the ANR JCJC Project SVeDaS (ANR-16-CE40- 0021) and Stéphane Demri acknowledges the support of the Centre National de la Recherche Scientifique (C.N.R.S.)., ANR-16-CE40-0021,SVeDaS,Spécification et Vérification des Systèmes basés sur les Données(2016)
Jazyk: angličtina
Rok vydání: 2021
Předmět:
Linguistics and Language
Theoretical computer science
Computer science
EXPTIME
0102 computer and information sciences
02 engineering and technology
resource
01 natural sciences
Language and Linguistics
[INFO.INFO-AI]Computer Science [cs]/Artificial Intelligence [cs.AI]
[INFO.INFO-FL]Computer Science [cs]/Formal Languages and Automata Theory [cs.FL]
Artificial Intelligence
0202 electrical engineering
electronic engineering
information engineering
Temporal logic
[INFO]Computer Science [cs]
Special case
linear-time temporal operator
[INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO]
020207 software engineering
Parity game
TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES
010201 computation theory & mathematics
Turing reduction
Bounded function
Path (graph theory)
complexity
alternating-time temporal logic ATL+
Zdroj: Artificial Intelligence
Artificial Intelligence, 2021, 300, pp.103557. ⟨10.1016/j.artint.2021.103557⟩
Artificial Intelligence, Elsevier, 2021, 300, pp.103557. ⟨10.1016/j.artint.2021.103557⟩
ISSN: 0004-3702
DOI: 10.1016/j.artint.2021.103557⟩
Popis: International audience; The resource-bounded alternating-time temporal logic RB±ATL combines strategic reasoning with reasoning about resources. Its model-checking problem is known to be 2EXPTIME-complete (the same as its proper extension RB±ATL$^⁎$) and fragments have been identified to lower the complexity.In this work, we consider the variant RB±ATL+ that allows for Boolean combinations of path formulae starting with single temporal operators, but restricted to a single resource, providing an interesting trade-off between temporal expressivity and resource analysis. We show that the model-checking problem for RB±ATL+ restricted to a single agent and a single resource is $\Delta_{2}^{P}$-complete, hence the same as for the standard branching-time temporal logic CTL+. In this case reasoning about resources comes at no extra computational cost. When a fixed finite set of linear-time temporal operators is considered, the model-checking problem drops to PTIME, which includes the special case of RB±ATL restricted to a single agent and a single resource. Furthermore, we show that, with an arbitrary number of agents and a fixed number of resources, the model-checking problem for RB±ATL+ can be solved in EXPTIME using a sophisticated Turing reduction to the parity game problem for alternating vector addition systems with states (AVASS).
Databáze: OpenAIRE
Externí odkaz: