Incremental LTLf Synthesis

TL;DR

This paper introduces incremental LTLf synthesis, enabling agents to adapt strategies dynamically as new goals are received, by leveraging automata-based methods and formula progression techniques.

Contribution

It formally defines the incremental synthesis problem and proposes efficient solution methods, including automata-based and formula progression approaches, with experimental evaluation.

Findings

Automata-based incremental synthesis is efficient for multiple goals.

Formula progression can generate exponentially larger formulas but automata size remains bounded.

Naive implementation of formula progression is not competitive in practice.

Abstract

In this paper, we study incremental LTLf synthesis -- a form of reactive synthesis where the goals are given incrementally while in execution. In other words, the protagonist agent is already executing a strategy for a certain goal when it receives a new goal: at this point, the agent has to abandon the current strategy and synthesize a new strategy still fulfilling the original goal, which was given at the beginning, as well as the new goal, starting from the current instant. In this paper, we formally define the problem of incremental synthesis and study its solution. We propose a solution technique that efficiently performs incremental synthesis for multiple LTLf goals by leveraging auxiliary data structures constructed during automata-based synthesis. We also consider an alternative solution technique based on LTLf formula progression. We show that, in spite of the fact that formula progression can generate formulas that are exponentially larger than the original ones, their minimal automata remain bounded in size by that of the original formula. On the other hand, we show experimentally that, if implemented naively, i.e., by actually computing the automaton of the progressed LTLf formulas from scratch every time a new goal arrives, the solution based on formula progression is not competitive.