First-Order LTLf Synthesis with Lookback (Extended Version)

TL;DR

This paper introduces a reactive synthesis method for LTLf with first-order constraints and lookback, expanding expressiveness but facing high complexity and undecidability issues, while providing soundness and completeness under certain bounds.

Contribution

It presents the first reactive synthesis procedure for LTLf with lookback, enabling cross-instant variable comparison and identifying new decidable fragments.

Findings

The approach is sound and complete with bounded strategy length.

It re-proves known decidability results for certain fragments.

It identifies new decidable classes within LTLfMT.

Abstract

Reactive synthesis addresses the problem of generating a controller for a temporal specification in an adversarial environment; it was typically studied for LTL. Driven by applications ranging from AI to business process management, LTL modulo first order-theories over finite traces (LTLfMT) has recently gained traction, where propositional variables in properties are replaced by first-order constraints. Though reactive synthesis for LTLf with some first-order features has been addressed, existing work in this direction strongly restricts or excludes the possibility to compare variables across instants, a limitation that severely restricts expressiveness and applicability. In this work we present a reactive synthesis procedure for LTLfMT, where properties support "lookback" to model cross-instant comparison of variables. Our procedure works for full LTLfMT with lookback, subsuming the fragments of LTLfMT for which realizability was studied earlier. However, the setting with cross-instant comparison is inherently highly complex, as realizability is undecidable even over decidable background theories. Hence termination of our approach is in general not guaranteed. Nevertheless, we prove its soundness, and show that it is complete if a bound on the strategy length exists. Finally, we show that our approach constitutes a decision procedure for several relevant fragments of LTLfMT, at once re-proving known decidability results and identifying new decidable classes.