LTLƒ Synthesis with Fairness and Stability Assumptions
Authors: Shufang Zhu, Giuseppe De Giacomo, Geguang Pu, Moshe Y. Vardi3088-3095
AAAI 2020 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | In this work we show that in interesting cases we can avoid such a detour to LTL synthesis and keep the simplicity of LTLf synthesis. Specifically, we develop a BDD-based fixpoint-based technique for handling basic forms of fairness and of stability assumptions. We show, empirically, that this technique performs much better than standard LTL synthesis. |
| Researcher Affiliation | Academia | Shufang Zhu,1 Giuseppe De Giacomo,2 Geguang Pu,1 Moshe Y. Vardi3 1Each China Normal University, 2Sapienza Universit a di Roma, 3Rice University shufangzhu.szhu@gmail.com, degiacomo@diag.uniroma1.it, ggpu@sei.ecnu.edu.cn, vardi@cs.rice.edu |
| Pseudocode | No | The paper does not contain any structured pseudocode or algorithm blocks. It describes the steps for solving fair and stable DFA games in paragraph form. |
| Open Source Code | No | The paper references an existing LTLf synthesis tool 'Syft' and states their implementation 'based on the code of Syft' and 'called FSyft and St Syft'. It provides a GitHub link for Syft: 'https://github.com/saffiepig/Syft', but it does not state that *their* specific implementations (FSyft and St Syft) are open-source or provide a link for them. |
| Open Datasets | No | The paper mentions: 'We collected 1200 formulas consisting of two classes of benchmarks: 1000 randomly conjuncted LTLf formulas over 100 basic cases, generated in the style described in (Zhu et al. 2017b), the length of which, indicating the number of conjuncts, ranges form 1 to 5. The assumption (either fairness or stability) is assigned by randomly selecting one variable from all environment variables; 200 LTLf synthesis benchmarks with assumptions generated from a scalable counter game...'. While it describes the benchmarks, it does not provide access information (link, DOI, etc.) for these specific formulas or the generated data, only referencing the style of generation. |
| Dataset Splits | No | The paper describes the benchmarks used for evaluation but does not provide specific details on how these datasets were split into training, validation, or test sets, or if such splits were even applicable given the nature of synthesis problems (where formulas are tested, not trained on). |
| Hardware Specification | Yes | All tests were ran on a computer cluster. Each test took an exclusive access to a node with Intel(R) Xeon(R) CPU E5-2650 v2 processors running at 2.60GHz. |
| Software Dependencies | Yes | Based on the LTLf synthesis tool Syft 2, we implemented our fixpoint-based techniques...The implementation makes use of the BDD library CUDD3.0.0 (Somenzi 2016). For such comparison, we employed the LTLf-to-LTL translator implemented in SPOT (Duret-Lutz et al. 2016) and chose Strix (Meyer, Sickert, and Luttenberger 2018), the winner of the synthesis competition SYNTCOMP 2019 3 over LTL synthesis track, as the baseline. |
| Experiment Setup | Yes | Time out was set to 1000 seconds. |