Alternating-time Temporal Logic on Finite Traces
Authors: Francesco Belardinelli, Alessio Lomuscio, Aniello Murano, Sasha Rubin
IJCAI 2018 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Theoretical | We study validities of these logics and present optimal algorithms for their modelchecking problems in the perfect recall case. Overall, we reduce the problem (G, s) |= ϕ to model checking a game with an LTLf objective ψ; in turn, this can be solved by converting ψ into a DFW accepting the models of ψ (the DFW might be doubly-exponentially larger than the formula), then taking the product of the resulting DFW with the structure G to obtain a safety game that, in turn, can be solved by using the standard fix-point algorithm linearly in the size of the game. |
| Researcher Affiliation | Academia | 1 Laboratoire IBISC, UEVE, France 2 Department of Computing, Imperial College London, UK 3 DIETI, Universit a degli Studi di Napoli, Italy |
| Pseudocode | Yes | Figure 1: Algorithm for solving games with LTLf objectives in double-exponential time. Figure 2: Recursive algorithm for model-checking ATLf that calls the Game Solving algorithm (Figure 1). Figure 3: Algorithm for model-checking G against LTLf formulas. |
| Open Source Code | No | The paper does not provide any statement or link indicating that the source code for the methodology is openly available. |
| Open Datasets | No | The paper is theoretical, focusing on logic and algorithms for model checking. It does not use empirical datasets for training or evaluation, nor does it refer to public dataset availability in that context. |
| Dataset Splits | No | The paper is theoretical and does not involve empirical experiments with data splits for validation. |
| Hardware Specification | No | The paper is theoretical and focuses on logic and algorithms; it does not describe any specific hardware used for computations or experiments. |
| Software Dependencies | No | The paper is theoretical and describes algorithms conceptually, primarily using automata theory. It does not specify any software dependencies with version numbers required for reproducibility. |
| Experiment Setup | No | The paper is theoretical and does not describe an empirical experimental setup with hyperparameters or system-level training settings. |