Notice: The reproducibility variables underlying each score are classified using an automated LLM-based pipeline, validated against a manually labeled dataset. LLM-based classification introduces uncertainty and potential bias; scores should be interpreted as estimates. Full accuracy metrics and methodology are described in Coakley et alK. L. Coakley, T. Snelleman, H. Hoos, and O. E. Gundersen, "The embrace of open science: An analysis of a decade of AI research and 56 800 conference papers," Under Review, 2026..
Symbolic LTLf Synthesis
Authors: Shufang Zhu, Lucas M. Tabajara, Jianwen Li, Geguang Pu, Moshe Y. Vardi
IJCAI 2017 | Venue PDF | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | We implement this symbolic synthesis method in a tool called Syft, and demonstrate by experiments on scalable benchmarks that the symbolic approach scales better than the explicit one. |
| Researcher Affiliation | Academia | Shufang Zhu East China Normal University saffiechu@gmail.com Lucas M. Tabajara Rice University EMAIL Rice University EMAIL East China Normal University EMAIL Moshe Y. Vardi Rice University EMAIL |
| Pseudocode | No | The paper describes procedural steps for the fixpoint computation but does not present them in a clearly labeled 'Pseudocode' or 'Algorithm' block. |
| Open Source Code | No | The paper mentions implementing tools called Syft and E-Syft but does not provide any concrete access information such as a repository link or an explicit statement about code availability. |
| Open Datasets | Yes | we construct our benchmarks from 20 basic cases, half of which are realizable, from the LTL literature [Jobstmann and Bloem, 2006]. For the synthesis experiments, besides the original 20 basic cases we also collected 80 instances from the LTL synthesis tool Acacia+ [Bohy et al., 2012], making 100 cases in total. |
| Dataset Splits | No | The paper describes generating 'benchmarks' and 'instances' for evaluation but does not specify explicit train/validation/test dataset splits with percentages, sample counts, or citations to predefined splits relevant for model training/evaluation. |
| Hardware Specification | Yes | The platform used in the experiments is a computer cluster consisting of 2304 processor cores in 192 Westmere nodes (12 processor cores per node) at 2.83 GHz with 4GB of RAM per core, and 6 Sandy Bridge nodes of 16 processor cores each, running at 2.2 GHz with 8GB of RAM per core. |
| Software Dependencies | Yes | Both were implemented in C++11, and Syft uses CUDD-3.0.0 as the BDD library. |
| Experiment Setup | Yes | Time out was set to 120 seconds. Given L and m (the size of the candidate variable set), we generate a formula RC(L) in the following way: (1) Randomly select L basic cases; (2) For each case φ, substitute every variable v with a random new variable v chosen from m atomic propositions. Formula lengths L range from 1 to 10, and m varies in increments of 50 from 100 to 500. |