The classical planning problem aims to find a sequence of permitted actions leading a system to a designed state, i.e., to achieve the system’s task. However, in many realistic cases we also have requirements on how to complete the task, indicating that some behaviors and situations are more preferred than others. In this paper, we present the probabilistic preference-based planning problem ($\mathrm{P4}$) for Markov decision processes, where the preferences are defined based on an enriched probabilistic LTL-style logic. We first recall$\mathrm{\mathrm{P4} {}Solver}$, an SMT-based planner computing the preferred plan by reducing the problem to a quadratic programming one previously developed to solve$\mathrm{P4}$. To improve computational efficiency and scalability, we then introduce a new encoding of the probabilistic preference-based planning problem as a multi-objective model checking one, and propose the corresponding planner$\mathrm{\mathrm{P4} {}Solver} _{{MO}}$. We illustrate the efficacy of both planners on some selected case studies to show that the model checking-based algorithm is considerably more efficient than the quadratic-programming-based one.

The classical planning problem can be enriched with quantitative and qualitative user-defined preferences on how the system behaves on achieving the goal. In this paper, we propose the probabilistic preference planning problem for Markov decision processes, where the preferences are based on an enriched probabilistic LTL-style logic. We develop P4Solver, an SMT-based planner computing the preferred plan by reducing the problem to quadratic programming problem, which can be solved using SMT solvers such as Z3. We illustrate the framework by applying our approach on two selected case studies.