Planning under LTL Environment Specifications

Planning domains represent what an agent assumes or believes about the environment it acts in. In the presence of nondeterminism, additional temporal assumptions, such as fairness, are often expressed as extra conditions on the domain. Here we consider environment specifications expressed in arbitrary LTL, which generalize many forms of environment specifications, including classical specifications of nondeterministic 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 consider environment specifications as specifications of environment 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.