What to Do When You Can't Do It All: Temporal Logic Planning with Soft Temporal Logic Constraints

In this paper, we consider a temporal logic planning problem in which the\nobjective is to find an infinite trajectory that satisfies an optimal selection\nfrom a set of soft specifications expressed in linear temporal logic (LTL)\nwhile nevertheless satisfying a hard specification expressed in LTL. Our\nprevious work considered a similar problem in which linear dynamic logic for\nfinite traces (LDLf), rather than LTL, was used to express the soft\nconstraints. In that work, LDLf was used to impose constraints on finite\nprefixes of the infinite trajectory. By using LTL, one is able not only to\nimpose constraints on the finite prefixes of the trajectory, but also to set\n`soft' goals across the entirety of the infinite trajectory. Our algorithm\nfirst constructs a product automaton, on which the planning problem is reduced\nto computing a lasso with minimum cost. Among all such lassos, it is desirable\nto compute a shortest one. Though we prove that computing such a shortest lasso\nis computationally hard, we also introduce an efficient greedy approach to\nsynthesize short lassos nonetheless. We present two case studies describing an\nimplementation of this approach, and report results of our experiment comparing\nour greedy algorithm with an optimal baseline.\n