Finite-Trace and Generalized-Reactivity Specifications in Temporal Synthesis
Authors: Giuseppe De Giacomo, Antonio Di Stasio, Lucas M. Tabajara, Moshe Vardi, Shufang Zhu
IJCAI 2021 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | 6 Experimental Analysis We implemented the approach described in Section 5, which subsumes the method described in Section 3, in a tool called GFSYNTH. In this section, we first describe the implementation of GFSYNTH, and then introduce two representative benchmarks that are able to capture commonly used sensorbased robotic tasks. An empirical evaluation is shown at the end to show the performance of our approach. |
| Researcher Affiliation | Academia | 1 Sapienza University of Rome, Rome, Italy 2 Rice University, Houston, US |
| Pseudocode | No | The paper describes its methods using mathematical notation and natural language but does not include any explicit pseudocode blocks or algorithms. |
| Open Source Code | No | The paper states that its tool GFSYNTH uses code from other LTLf-synthesis tools (SYFT) and GR(1)-synthesis tools (SLUGS), but it does not explicitly state that the code for GFSYNTH itself is open-source or publicly available. |
| Open Datasets | No | The paper uses custom-defined benchmarks ("Finding Nemo" and "Workstation Resupply") and does not mention using or providing access to any publicly available or open datasets. |
| Dataset Splits | No | The paper describes custom benchmarks with a scalable parameter 'n' but does not provide specific details on dataset splits (e.g., train/validation/test percentages or counts) or cross-validation setup. |
| Hardware Specification | Yes | All tests were run on a computer cluster. Each test had exclusive access to a node with Intel(R) Xeon(R) CPU E5-2650 v2 processors running at 2.60GHz. |
| Software Dependencies | Yes | we make use of the BDD library CUDD-3.0.0 [Somenzi, 2016] to implement operations |
| Experiment Setup | No | The paper mentions system settings like "Time out was set to two hours (7200 seconds)" and describes the tools used, but it does not provide specific hyperparameter values or detailed algorithm configuration settings relevant to its synthesis approach. |