Complexity of Safety and coSafety Fragments of Linear Temporal Logic
Authors: Alessandro Artale, Luca Geatti, Nicola Gigante, Andrea Mazzullo, Angelo Montanari
AAAI 2023 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Theoretical | In this paper, we study the complexity of the problems of satisfiability, validity, and realizability over infinite and finite traces for the safety and cosafety fragments of LTL. As for satisfiability and validity over infinite traces, we prove that the majority of the fragments have the same complexity as full LTL, that is, they are PSPACE-complete. The picture is radically different for realizability: we find fragments with the same expressive power whose complexity varies from 2EXPTIME-complete (as full LTL) to EXPTIME-complete. Notably, for all cosafety fragments, the complexity of the three problems does not change passing from infinite to finite traces, while for all safety fragments the complexity of satisfiability (resp., realizability) over finite traces drops to NP-complete (resp., ΠP 2 -complete). |
| Researcher Affiliation | Academia | 1Free University of Bozen-Bolzano 2 University of Udine artale@inf.unibz.it, luca.geatti@uniud.it, gigante@inf.unibz.it, mazzullo@inf.unibz.it, angelo.montanari@uniud.it |
| Pseudocode | No | The paper does not include any sections or figures labeled "Pseudocode" or "Algorithm", nor does it present structured code-like steps. |
| Open Source Code | No | The paper does not contain any statement or link indicating that the source code for the described methodology is publicly available. |
| Open Datasets | No | This paper is theoretical and does not involve experiments with datasets, therefore no public dataset information or access details are provided. |
| Dataset Splits | No | This paper is theoretical and does not involve experiments with datasets, therefore no training/validation/test splits are mentioned. |
| Hardware Specification | No | This paper is theoretical and does not describe experiments that would require specific hardware, thus no hardware specifications are mentioned. |
| Software Dependencies | No | This paper is theoretical and does not describe experiments, therefore no specific software dependencies with version numbers are listed. |
| Experiment Setup | No | This paper is theoretical and does not describe experimental setups, hyperparameters, or training configurations. |