---
title: "Fair LTL Synthesis for Non-Deterministic Systems using Strong Cyclic Planners"
authors:
  - "Fabio Patrizi"
  - "Nir Lipovetzky"
  - "Hector Geffner"
doi: ""
url: "https://ijcai.org/proceedings/2013/345"
pdf: "https://ijcai.org/proceedings/2013/0345.pdf"
venue: "Proceedings of the Twenty-Third International Joint Conference on Artificial Intelligence"
year: 2013
pages: "2343-2348"
track: ""
keywords:
---

# Fair LTL Synthesis for Non-Deterministic Systems using Strong Cyclic Planners

Fabio Patrizi, Nir Lipovetzky, Hector Geffner

*Proceedings of the Twenty-Third International Joint Conference on Artificial Intelligence*, pages 2343-2348.

## Abstract

We consider the problem of planning in environments where the state is fully observable, actions have non-deterministic effects, and plans must generate infinite state trajectories for achieving a large class of LTL goals. More formally, we focus on the control synthesis problem under the assumption that the LTL formula to be realized can be mapped into a deterministic Büchi automaton. We show that by assuming that action non-determinism is fair, namely that infinite executions of a non-deterministic action in the same state yield each possible successor state an infinite number of times, the (fair) synthesis problem can be reduced to a standard strong cyclic planning task over reachability goals. Since strong cyclic planners are built on top of efficient classical planners, the transformation reduces the non-deterministic, fully observable, temporally extended planning task into the solution of classical planning problems. A number of experiments are reported showing the potential benefits of this approach to synthesis in comparison with state-of-the-art symbolic methods.