Partitioning Techniques in LTLf Synthesis
Authors: Lucas Martinelli Tabajara, Moshe Y. Vardi
IJCAI 2019 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | After describing how partitioning can be integrated into symbolic LTLf synthesis, we proceed to perform an experimental evaluation to point out the limitations of partitioning in this context. |
| Researcher Affiliation | Academia | Lucas Martinelli Tabajara and Moshe Y. Vardi Rice University lucasmt@rice.edu, vardi@cs.rice.edu |
| Pseudocode | No | The paper describes algorithms using symbolic notation and textual explanations (e.g., in Section 3.2), but does not contain a formally labeled "Pseudocode" or "Algorithm" block. |
| Open Source Code | Yes | Supplemental data in https://bitbucket.org/ijcai2816/ijcai-2816/ |
| Open Datasets | Yes | We initially considered benchmarks in the style of the ones used in [Zhu et al., 2017] and [Camacho et al., 2018], formed by random conjunctions of smaller base cases taken from the lilydemo LTL benchmark suite from [Jobstmann and Bloem, 2006] interpreted with LTLf semantics. |
| Dataset Splits | No | The paper uses various benchmark families for evaluation but does not describe specific training, validation, or test dataset splits. The experimental setup seems to involve running the synthesis algorithm on different problem instances rather than splitting a dataset. |
| Hardware Specification | Yes | All experiments were performed on a cluster consisting of 2304 processor cores in 192 Westmere nodes (12 processor cores per node) at 2.83 GHz with 48 GB of RAM per node (4 GB per core). |
| Software Dependencies | No | The paper mentions using the tool MONA for translation to DFAs, but does not provide specific version numbers for MONA or any other software libraries or dependencies used in the experiments. |
| Experiment Setup | Yes | We tried numerous different combinations of earlyquantification heuristics, as well as variable ordering heuristics for the BDDs. For all of them, the same general results were obtained... The best performance for both the partitioned and monolithic versions was achieved by using dynamic variable reordering for the BDDs. |