Multi-objective planning with multiple high level task specifications

We present an algorithm to solve a sequential stochastic decision making problem whereby a robot is subject to multiple objective functions and is asked to complete a number of subgoals specified using a subset of linear temporal logic. Each subgoal is associated with a desired satisfaction probability that will be met in expectation by the policy produced by the algorithm. Our method relies on the theory of constrained Markov Decision Processes and on methods coming from the realm of formal verification. The key idea is the definition of a product operation that can recursively incorporate more and more subgoals into the underlying planner. Ultimately, a policy is computed solving a linear program and we outline conditions for the existence and correctness of the solution. Our findings are validated in various simulation scenarios.