Parameterised Resource-Bounded ATL

Authors: Natasha Alechina, Stéphane Demri, Brian Logan7040-7046

AAAI 2020 | Conference PDF | Archive PDF | Plain Text | LLM Run Details

Reproducibility Variable Result LLM Response
Research Type Theoretical We give a parameter extraction algorithm and prove that the model-checking problem is 2EXPTIMEcomplete. The main contribution of our paper is to show that the maximal value given in (Jurdzinski, Lazi c, and Schmitz 2015) transfers to Par RB ATL, and to show how it can be used for nested temporal goals that include negations and a mixture of reachability and non-termination goals.
Researcher Affiliation Academia Natasha Alechina Utrecht University Utrecht, The Netherlands n.a.alechina@uu.nl Stephane Demri LSV, CNRS, ENS Paris-Saclay, University Paris-Saclay Cachan, France demri@lsv.fr Brian Logan University of Nottingham Nottingham, UK brian.logan@nottingham.ac.uk
Pseudocode Yes Algorithm 1: Computing φ0
Open Source Code No In future work we plan to implement the algorithm.
Open Datasets No The paper is theoretical and does not describe the use of any dataset for training or evaluation.
Dataset Splits No The paper is theoretical and does not describe the use of any dataset for validation.
Hardware Specification No The paper is theoretical and does not describe the hardware used for any experiments.
Software Dependencies No The paper is theoretical and does not describe specific software dependencies with version numbers for implementation or experiments.
Experiment Setup No The paper is theoretical and does not describe any experimental setup details such as hyperparameters or training configurations.