Hybrid Compositional Reasoning for Reactive Synthesis from Finite-Horizon Specifications
Authors: Suguman Bansal, Yong Li, Lucas Tabajara, Moshe Vardi9766-9774
AAAI 2020 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | A comprehensive empirical evaluation on conversion and synthesis benchmarks supports the merits of our hybrid approach. The goal of the empirical analysis is to examine the performance of our hybrid approach in LTLf-to-DFA generation and LTL synthesis against existing tools and approaches. |
| Researcher Affiliation | Academia | 1Department of Computer Science, Rice University 2State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Science 3University of Chinese Academy of Sciences {suguman, lucasmt}@rice.edu, liyong@ios.ac.cn, vardi@cs.rice.edu |
| Pseudocode | Yes | A semi-formal description of the steps of the algorithm are given below. The complete description has been deferred to (Bansal et al. 2019). Step 0. (Initial) We are given input formula ϕ = n i=1 ϕi, and switch-over threshold values t1, t2 > 0. Step 1. (Decomposition) Construct the minimal DFA Di in explicit-state representation for all i {1, . . . , n}. |
| Open Source Code | No | The paper implements tools LISA and LISASYNT, but does not provide a specific repository link or explicit statement about the public release of their source code. |
| Open Datasets | Yes | We conduct our experiments on a benchmark suite curated from prior works, spanning classes of realistic and synthetic benchmarks. In total, we have 454 benchmarks split into four classes: random conjunctions (400 cases) (Zhu et al. 2017b), single counters (20 cases), double counters (10 cases) and Nim games (24 cases) (Tabajara and Vardi 2019). |
| Dataset Splits | No | The paper describes using various benchmarks, but it does not provide specific dataset split information (percentages, sample counts, or detailed splitting methodology) for training, validation, or testing. |
| Hardware Specification | Yes | All experiments were conducted on a single node of a high-performance cluster. Each node consists of four quadcore Intel-Xeon processor running at 2.6 GHz. |
| Software Dependencies | No | The paper mentions software like BUDDY and SPOT, and cites papers for them, but does not provide specific version numbers for these or other software dependencies used. |
| Experiment Setup | Yes | We set t1 = 800 and t2 = 300000 for the Nim-game class and to t1 = 800 and t2 = 2500 for all other classes. ...LTLf-to-DFA conversion experiments were run for 1 hour with 8 GB each, LTLf-synthesis experiments for 8 hours with 32 GB each. |