LTL Realizability via Safety and Reachability Games
Authors: Alberto Camacho, Christian Muise, Jorge A. Baier, Sheila A. McIlraith
IJCAI 2018 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | While our contributions are intended to be largely theoretical, we conducted preliminary experiments to assess the practicality of the different techniques for LTL realizability and synthesis that we present. Preliminary results show that techniques employing Nk BW automata can complement existing techniques based on Uk CW automata, addressing realizability and synthesis problems that otherwise cannot be solved by existing tools. Moreover, they show that automated planning technology (and, in particular, FOND) can be an efficient approach to LTL realizability and synthesis. |
| Researcher Affiliation | Collaboration | Alberto Camacho , Christian Muise , Jorge A. Baier , Sheila A. Mc Ilraith Department of Computer Science, University of Toronto IBM Research, Cambridge Research Center, USA Pontificia Universidad Cat olica de Chile Chilean Center for Semantic Web Research |
| Pseudocode | Yes | Figure 1: Details of the Safe2FOND compilation for a game S = X, Y, (A, Uk CW) s with automaton A = Q, Σ, q0, δ, α. |
| Open Source Code | No | We implemented the algorithms for LTL realizability and synthesis via FOND in a tool we named Syn Kit [Camacho et al., 2018c]. - This names the tool and cites a paper about it, but does not provide a direct link or explicit statement that the code is publicly available for this paper's methodology. |
| Open Datasets | Yes | We tested the performance of our planning-based methods over a collection of benchmarks used in the sequential realizability track of the SYNTCOMP 2017 competition. |
| Dataset Splits | No | The paper mentions evaluating performance on 'a collection of benchmarks used in the sequential realizability track of the SYNTCOMP 2017 competition.' However, it does not specify how these benchmarks are split into training, validation, or test sets; it describes competition problems rather than typical dataset splits for model training. |
| Hardware Specification | Yes | Our experiments were run on an Intel Xeon E5-2430 2.2GHz processor, and each process was limited to 30 minute run times and 4GB memory usage. |
| Software Dependencies | No | We use Spot to transform LTL formulae into NBW [Duret-Lutz et al., 2016]. Reductions to automata games listed in Table 1 are solved via FOND planning with Safe2FOND and Reach2FOND compilations. We use PRP to generate strong cyclic solutions [Muise et al., 2012], and My ND to generate strong solutions [Mattm uller et al., 2010]. - The paper lists software tools (Spot, PRP, My ND) but does not provide their specific version numbers. |
| Experiment Setup | Yes | We configured Syn Kit to perform reductions to Uk CW games with k ≤ 2 and Nk BW games with k ≤ 3. |