First-Order LTLf Synthesis with Lookback (Extended Version)

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.