Strategy Synthesis for First-Order Agent Programs over Finite Traces

In this work, we consider the task of synthesizing an execution strategy for an agent from a high-level description of the initial state of the world, the actions at the agent's disposal, a control program, and a temporal goal. In particular, we look at the more realistic (and more challenging) case of infinite-state systems with unbounded object domains, obtained from the usage of specification formalisms with first-order expressiveness, as well as exogenous events, triggered by the non-deterministic environment. More specifically, we use the agent programming language Golog, which is based on the situation calculus, a first-order logic formalism for reasoning about change. Here, a situation calculus action theory (perhaps incompletely) describes the initial state of the world, together with the preconditions and effects of primitive actions at the agent's disposal, while Golog programs then combine primitive actions into more complex behaviours using sequence, iteration, non-deterministic branching, and concurrency. Some of the non-deterministic choices in the program are under the control of the environment, which makes the program realization a synthesis problem. The synthesis task is to determine an execution strategy that executes the program successfully while satisfying the temporal goal, independent of the environment's choices.