LTLf Synthesis on First-Order Action Theories
<|reference_start|>LTLf Synthesis on First-Order Action Theories: Golog is an expressive high-level agent language that includes nondeterministic operators which allow to leave some of the decisions to be made only at execution time. This so-called program realization is typically implemented by means of search, or in an incremental online fashion. In this paper, we consider the more realistic case where parts of the non-determinism are under the control of the environment. Program realization then becomes a synthesis problem, where a successful realization executes the program and satisfies the temporal goal for all possible environment actions. We consider Golog programs in combination with an expressive class of first-order action theories that allow for an unbounded number of objects and non-local effects, together with a temporal goal specified in a first-order extension of LTLf. We solve the synthesis problem by constructing a game arena that captures all possible executions of the program while tracking the satisfaction of the temporal goal and then solving the resulting two-player game. We evaluate the approach in two domains, showing the general feasibility of the approach.<|reference_end|>
@article{hofmann2024ltlf,
    title={LTLf Synthesis on First-Order Action Theories},
    author={Till Hofmann, Jens Cla{ss}en},
    journal={arXiv preprint arXiv:2410.00726},
    year={2024},
    archivePrefix={arXiv},
    eprint={2410.00726},
    primaryClass={cs.AI cs.LO}
}