Notice: This website is continuously updated as new conference proceedings and journal volumes are published. Consequently, the figures presented here may differ from those reported in our publications.
A brief overview of our methodology is provided on the Methods page, along with references to publications documenting our approach and links to the code and data used in each study.
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.
Complexity of Safety and coSafety Fragments of Linear Temporal Logic
Authors: Alessandro Artale, Luca Geatti, Nicola Gigante, Andrea Mazzullo, Angelo Montanari
AAAI 2023 | Venue PDF | LLM Run Details | Input Tokens: 19,068 Total number of tokens sent to the LLM as input for this paper's analysis. | Output Tokens: 4,091 Total number of tokens produced by the LLM (including reasoning/thinking tokens) for this paper's analysis.
| 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 EMAIL, EMAIL, EMAIL, EMAIL, EMAIL |
| 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. |