Planning under LTL Environment Specifications

Planning domains represent what an agent assumes or be- lieves about the environment it acts in. In the presence of non- determinism, additional temporal assumptions, such as fair- ness, are often expressed as extra conditions on the domain. Here we consider environment specifications expressed in ar- bitrary LTL, which generalize many forms of environment specifications, including classical specifications of nondeter- ministic domains, fairness, and other forms of linear-time constraints on the domain itself. Existing literature typically implicitly or explicitly considers environment specifications as constraints on possible traces. In contrast, in spite of the fact that we use a linear-time formalism, we propose to con- sider environment specifications as specifications of environ- ment strategies. Planning in this framework is the problem of computing an agent strategy that achieves its goal against all environment strategies satisfying the specification. We study the mathematical and computational properties of planning in this general setting. We observe that not all LTL formulas correspond to legitimate environment specifications, and formally characterize the ones that do. Moreover, we show that our notion of planning generalizes the classical notion of Church’s synthesis, and that in spite this one can still solve it optimally using classical Church’s synthesis.