Synthesizing Good-Enough Strategies for LTLf Specifications
Authors: Yong Li, Andrea Turrini, Moshe Y. Vardi, Lijun Zhang
IJCAI 2021 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | Moreover, we conduct a comprehensive empirical evaluation on benchmarks from synthesis competitions and literature. We show that our specialized synthesis algorithm for GE-strategies outperforms the algorithms going through GE-synthesis of LTL formulas by orders of magnitude, regarding the runtime and the number of solved cases. (from Abstract) |
| Researcher Affiliation | Academia | Yong Li1 , Andrea Turrini1,2 , Moshe Y. Vardi3 and Lijun Zhang1,2 1State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences 2Institute of Intelligent Software, Guangzhou 3Department of Computer Science, Rice University |
| Pseudocode | No | The paper describes algorithms but does not present them in formal pseudocode or algorithm blocks. |
| Open Source Code | No | The paper states 'We have extended the LISA tool described in [Bansal et al., 2020] with an implementation of the synthesis algorithm described in Section 3;' but does not explicitly provide concrete access to the source code of their specific implementation. |
| Open Datasets | Yes | As benchmarks, we collected all benchmarks available on the past SYNTCOMP competitions website2, resulting in 294 benchmark files. We considered also the 1617 benchmarks used in [Bansal et al., 2020], already in the appropriate JSON format, for a total of 1911 executions. |
| Dataset Splits | No | The paper describes using a collection of benchmark files for evaluation but does not specify train, validation, or test splits for any dataset. |
| Hardware Specification | Yes | We performed our experiments on a desktop PC equipped with a 3.4 GHz Intel i7-6700 processor and 8 GB of RAM, of which 5 GB were assigned to the experiments; the operating system was Ubuntu 18.04. |
| Software Dependencies | No | The paper mentions several tools used (LISA, MONA, BOSY, LTLSYNT, SPOT) and the operating system (Ubuntu 18.04), but does not provide specific version numbers for the key software components or libraries beyond their originating papers. |
| Experiment Setup | Yes | We imposed a timeout of 10 minutes for each benchmark. We performed our experiments on a desktop PC equipped with a 3.4 GHz Intel i7-6700 processor and 8 GB of RAM, of which 5 GB were assigned to the experiments; the operating system was Ubuntu 18.04. |