LTLƒ Synthesis with Fairness and Stability Assumptions

In synthesis, assumptions are constraints on the environment that rule out certain environment behaviors. A key observation here is that even if we consider systems with LTL f goals on finite traces, environment assumptions need to be expressed over infinite traces, since accomplishing the agent goals may require an unbounded number of environment action. To solve synthesis with respect to finite-trace LTL f goals under infinite-trace assumptions, we could reduce the problem to LTL synthesis. Unfortunately, while synthesis in LTL f and in LTL have the same worst-case complexity (both 2EXPTIME-complete), the algorithms available for LTL synthesis are much more difficult in practice than those for LTL f synthesis. In this work we show that in interesting cases we can avoid such a detour to LTL synthesis and keep the simplicity of LTL f synthesis. Specifically, we develop a BDD-based fixpoint-based technique for handling basic forms of fairness and of stability assumptions. We show, empirically, that this technique performs much better than standard LTL synthesis. Recently synthesis under assumptions in LTL f has attracted specific interest (De Giacomo and Rubin 2018; Camacho, Bienvenu, and McIlraith 2018) . First, planning for LTL f goals can be considered as a form of LTL f synthesis under assumptions, where the assumptions are the dynamics of the environment encoded in the planning domain (Green 1969; Camacho, Bienvenu, and McIlraith 2018; Aminof et al. 2018; 2019). However, more generally, assumptions can be arbitrary constraints on the environment that can be exploited by the agent in devising a strategy to fulfill its goal.