Computing Unsatisfiable Cores for LTLf Specifications
Authors: Marco Roveri, Claudio Di Ciccio, Chiara Di Francescomarino, Chiara Ghidini
JAIR 2024 | Venue PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | We implement those algorithms extending the respective implementations and carry out an experimental evaluation on a set of reference benchmarks, restricting to the unsatisfiable specifications. The results put in evidence that the different algorithms and tools exhibit complementary features determining their efficiency and efficacy. |
| Researcher Affiliation | Academia | Marco Roveri EMAIL University of Trento, Via Sommarive, 9, 38123 Trento, Italy Claudio Di Ciccio EMAIL Utrecht University, Princetonplein 5, 3584 CC Utrecht, Netherlands Chiara Di Francescomarino EMAIL University of Trento, Via Sommarive, 9, 38123 Trento, Italy Chiara Ghidini EMAIL Free University of Bozen-Bolzano, Piazza Domenicani 3, 39100 Bolzano, Italy, and Fondazione Bruno Kessler, Via Sommarive, 18, 38123 Trento, Italy |
| Pseudocode | Yes | Algorithm NA1 BDD-based LTLf UC extraction with the approach of Clarke et al. (1997) ... Algorithm NA2 SAT BMC-based LTLf UC extraction with the approach of Biere et al. (2006) ... Algorithm NA3 TR LTLf UC Extraction with the approach of Schuppan (2016) ... Algorithm NA4 SAT LTLf UC Extraction with the approach of Li et al. (2020) |
| Open Source Code | Yes | The source code for the extended version of Nu SMV with these implementations is available at https://github.com/roveri-marco/ltlfuc. ... The source code for our extended version of aaltaf is available at https:// github.com/roveri-marco/aaltaf-uc. ... All the material to reproduce the experiments reported hereinafter is available at https://github.com/roveri-marco/ltlfuc/archive/refs/tags/jair-release -v1.0.zip. |
| Open Datasets | Yes | For the experimental evaluation, we considered all the unsatisfiable problems reported in the work of Li et al. (2020), for a total of 1377 problems. ... a set of reference benchmarks taken from (Li et al., 2020) |
| Dataset Splits | No | The paper focuses on satisfiability checking for LTLf specifications and uses a set of reference benchmarks. There is no mention of traditional dataset splits (e.g., training, validation, test) as would be common in machine learning tasks. |
| Hardware Specification | Yes | We ran all experiments on an Ubuntu 18.04.5 LTS machine, 8-Core Intel Xeon at 2.2 GHz, equipped with 64 GB of RAM. |
| Software Dependencies | No | We realise Algorithms NA1 and NA2 as extensions of the Nu SMV model checker (Cimatti et al., 2002) ... For our experiments, we use the latest version of trp++. ... Finally, we implement Algorithm NA4 within an extended version of the aaltaf tool (Li et al., 2020). The paper mentions specific tools but does not provide their version numbers (e.g., 'latest version of trp++' is not a specific version). |
| Experiment Setup | Yes | We set a memory occupation limit of 4 GB, and a CPU usage limit of 60 min. Additionally, we considered k = 50 as the maximum depth for Nu SMV-S, and we ran Nu SMV-B with the BDD dynamic variable reordering mode active (Felt et al., 1993) to dynamically reduce the size of the BDDs and thus save space over time. |