Linear Temporal Logic Modulo Theories over Finite Traces
Authors: Luca Geatti, Alessandro Gianola, Nicola Gigante
IJCAI 2022 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | The algorithm is implemented in the BLACK satisfiability checking tool, and an experimental evaluation shows the feasibility of the approach on novel benchmarks. |
| Researcher Affiliation | Academia | Luca Geatti , Alessandro Gianola , Nicola Gigante Free University of Bozen-Bolzano, Italy {geatti,gianola,gigante}@inf.unibz.it |
| Pseudocode | Yes | Algorithm 1 BLACK s main procedure for LTLf MT |
| Open Source Code | Yes | The source code and all the tests and benchmarks are available in BLACK s Git Hub repository, merged into version 0.7 of the tool. |
| Open Datasets | No | The paper mentions 'crafted benchmarks' and 'scalable patterns' but does not provide specific access information (links, DOIs, formal citations) to a publicly available or open dataset. |
| Dataset Splits | No | The paper does not explicitly specify training, validation, or test dataset split percentages or sample counts. |
| Hardware Specification | No | The paper states, 'The tests were run on commodity hardware,' which is not a specific hardware description required for reproducibility. |
| Software Dependencies | No | The paper mentions 'setting BLACK to use the Z3 backend [de Moura and Bjørner, 2008],' but it does not specify a version number for the Z3 solver or any other software dependency. |
| Experiment Setup | Yes | The tests were run on commodity hardware, setting BLACK to use the Z3 backend [de Moura and Bjørner, 2008]. The table shows... a qualitative plot of running times from N = 1 up to the maximum value of N which runs under the 5 minutes timeout. |