LTLf Synthesis on First-Order Agent Programs in Nondeterministic Environments
Authors: Till Hofmann, Jens Claßen
AAAI 2025 | Venue PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | Experimental results demonstrate this approach s feasibility in domains with unbounded objects and non-local effects. ... Section 5 Experiments ... Table 1: Evaluation Results for the Dish Robot Domain ... Table 2: Evaluation Results for the Warehouse Domain |
| Researcher Affiliation | Academia | Till Hofmann1, Jens Claßen2 1Department of Computer Science, RWTH Aachen University 2Institute for People and Technology, Roskilde University EMAIL, EMAIL |
| Pseudocode | Yes | Algorithm 1: Computing a strategy from AΦ G ... Algorithm 2: The program for the dishwasher robot ... Algorithm 3: The program for the warehouse robot |
| Open Source Code | Yes | We implemented the method (Claßen and Hofmann 2025) in the Prolog-based Golog interpreter vergo (Claßen 2018), that, different from other implementations, uses full FOL as base logic, where an embedded theorem prover (Schulz, Cruanes, and Vukmirovic 2019) is used for reasoning tasks such as deciding entailment and consistency. The system contains optimizations for handling FO expressions, in particular an FO variant of binary decision diagrams. ... vergo 0.1.1. https://doi.org/10.5281/zenodo.14690219. |
| Open Datasets | No | The paper describes two custom-defined domains, 'Dishwasher Robot' and 'Warehouse Robot', with their initial situations and axioms. However, it does not provide concrete access information (e.g., link, DOI, citation) for these specific domain definitions to be publicly available as open datasets. |
| Dataset Splits | No | The paper evaluates a synthesis method on custom-defined domains by varying parameters like the number of rooms, dishes, or boxes. It does not involve machine learning models or traditional datasets that require explicit training, validation, or test splits. |
| Hardware Specification | Yes | All experiments were conducted on an Intel Core i5-7300U @2.60GHz with 8GB of RAM, running Debian 12 with WSL2 under Windows 10, using SWI-Prolog 9.0.4 and version 3.2 of the E theorem prover. |
| Software Dependencies | Yes | All experiments were conducted on an Intel Core i5-7300U @2.60GHz with 8GB of RAM, running Debian 12 with WSL2 under Windows 10, using SWI-Prolog 9.0.4 and version 3.2 of the E theorem prover. |
| Experiment Setup | Yes | We evaluated the method on two domains, a dishwasher robot and a warehouse robot, that we will be described in detail below. ... Initial situation: ... Precondition axioms: ... Successor state axioms: ... Program: ... Specification: F G x, y. Dirty Dish(x, y) ... The construction is done in an incremental fashion, where only the relevant and reachable parts are actually materialized. This is achieved by keeping the types as general as possible, and only including additional formulas once they are needed. More specifically, the method works by iterating the following steps, until no more changes occur: Initialize: Create initial states (τ, , A, δ), where types τ are constructed only from formulas in D0 and literals L(P) of propositional assignments over A. Split: If there is a state (τ, E, A, ρ) that does not entail a truth value for some required condition ψ (the transition condition for an action α, the termination condition φ(ρ), the condition κ of an effect, or a literal l L(P) of a propositional assignment over A), then create two copies of all states and transitions, where one includes ψ and the other includes ψ into τ, discarding states with inconsistent τ. Expand: If a state s = (τ, E, A, ρ) admits an action α, create the successor state s and the transition s α s . |