Synthesis for LTL and LDL on Finite Traces
Authors: Giuseppe De Giacomo, Moshe Vardi
IJCAI 2015 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Theoretical | We characterize the problem computationally as 2EXPTIME-complete and present a sound and complete synthesis technique based on DFA (reachability) games. The presented technique is double exponential in general but optimal, since it can be shown that the problem itself is 2EXPTIME-complete. Moreover, considering the cost of each of the steps above, we get the following worst-case computational complexity upper bound. Theorem 5. Realizability in LDLf/LTLf can be solved in 2EXPTIME, and synthesis (i.e., returning a winning strategy) can be done in time double exponential. A matching lower-bound can be shown by reduction from EXPSPACE alternating Turing machines. Theorem 6. Realizability (and synthesis) in LDLf/LTLf is 2EXPTIME-hard. |
| Researcher Affiliation | Academia | Giuseppe De Giacomo Sapienza Universit a di Roma Roma, Italy degiacomo@dis.uniroma1.it Moshe Y. Vardi Rice University, Houston, TX, USA vardi@cs.rice.edu |
| Pseudocode | Yes | algorithm LDLf 2NFA input LTLf formula ϕ output NFA Aϕ = (2P, S, {s0}, ϱ, {sf}) s0 {"ϕ"} single initial state sf single final state S {s0, sf}, ϱ while (S or ϱ change) do if (q S and q |= V ("ψ" q) δ("ψ", Π)) then S S {q } update set of states ϱ ϱ {(q, Π, q )} update transition relation |
| Open Source Code | No | The paper does not provide any specific links to source code repositories, nor does it explicitly state that the code for the methodology described is released or made available. |
| Open Datasets | No | The paper is theoretical and does not involve empirical evaluation on datasets. Therefore, no information about publicly available or open datasets is provided. |
| Dataset Splits | No | The paper is theoretical and does not involve empirical evaluation on datasets. Therefore, no specific dataset split information (training, validation) is provided. |
| Hardware Specification | No | The paper is theoretical and does not describe any empirical experiments, thus no hardware specifications for running experiments are provided. |
| Software Dependencies | No | The paper is theoretical and focuses on logical specifications and synthesis techniques. It does not provide specific software dependencies with version numbers that would be needed to replicate an implementation of the described techniques. |
| Experiment Setup | No | The paper is theoretical and does not describe any empirical experiments, thus no details regarding experimental setup, such as hyperparameters or training settings, are provided. |