LTLf Synthesis Under Environment Specifications for Reachability and Safety Properties

TL;DR

This paper develops optimal algorithms for synthesizing strategies under environment specifications for reachability and safety properties in LTLf, covering new cases and providing a comprehensive framework.

Contribution

It introduces novel synthesis algorithms for various combinations of properties and specifications, expanding the existing theoretical landscape.

Findings

Algorithms are proven correct and optimal in complexity

Some cases are newly studied, others extend prior work

Provides a complete landscape of synthesis methods

Abstract

In this paper, we study LTLf synthesis under environment specifications for arbitrary reachability and safety properties. We consider both kinds of properties for both agent tasks and environment specifications, providing a complete landscape of synthesis algorithms. For each case, we devise a specific algorithm (optimal wrt complexity of the problem) and prove its correctness. The algorithms combine common building blocks in different ways. While some cases are already studied in literature others are studied here for the first time.