The Complexity of LTL on Finite Traces: Hard and Easy Fragments
Authors: Valeria Fionda, Gianluigi Greco
AAAI 2016 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | Motivated by the theoretical results we implemented a reasoner for LTLf, called LTL2SAT1, and compared it with Aalta (Li et al. 2014)... We used the same datasets used in (Li et al. 2014)... Experiments have been executed on a PC Intel Core i5 2,4 GHz, 8GB RAM. For each formula, we measured the ratio between the time required by LTL2SAT to check satisfiability and that required by Aalta. Figure 4 reports the results as percentage stacked bar charts, for each dataset. |
| Researcher Affiliation | Academia | Valeria Fionda and Gianluigi Greco De Ma CS, University of Calabria, Italy {fionda, ggreco}@mat.unical.it |
| Pseudocode | No | The paper describes formal frameworks and an encoding approach but does not include any explicitly labeled pseudocode or algorithm blocks. |
| Open Source Code | Yes | Motivated by the theoretical results we implemented a reasoner for LTLf, called LTL2SAT1... Downloadable at http://ltl2sat.wordpress.com/ |
| Open Datasets | Yes | We used the same datasets used in (Li et al. 2014) |
| Dataset Splits | No | The paper mentions using datasets for comparison but does not provide specific details on training, validation, or test splits such as percentages or sample counts. |
| Hardware Specification | Yes | Experiments have been executed on a PC Intel Core i5 2,4 GHz, 8GB RAM. |
| Software Dependencies | No | LTL2SAT rewrites the input formula into an equivalent Boolean formula and uses glucose (Audemard and Simon 2009) to compute a model. The specific version number for glucose is not provided. |
| Experiment Setup | Yes | When the optimization strategies are not applicable, the size n of the trace to be used in the SAT rewriting is initially set to 1: If no model is found, then n is doubled and the process is repeated until n exceeds the theoretical upper bound (or a 20s time-limit is reached). |