Symbolic LTLf Synthesis
Authors: Shufang Zhu, Lucas M. Tabajara, Jianwen Li, Geguang Pu, Moshe Y. Vardi
IJCAI 2017 | Venue PDF | Archive PDF | Plain Text | 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. |