马尔可夫决策过程（Markov Decision Processes，MDPs）是随机控制问题的一种数学模型，它在人工智能、经济学、计算机科学等领域有着广泛的应用。马尔可夫决策过程允许系统根据当前状态随机地选择动作，并随之转移到下一个状态。其核心在于一个动作的选择仅依赖于当前状态，而与历史状态无关，这称为马尔可夫性质。
在实际应用中，人们不仅仅关心系统能否从初始状态达到目标状态，还可能对系统行为的某些方面有特定的偏好。例如，用户可能对某些特定动作有偏好，或者愿意先达到某类特定状态再达到目标。为了在MDPs中加入这种偏好，研究者们提出了基于偏好的规划问题（Preference-based Planning）。
在本文中，作者提出了马尔可夫决策过程的概率偏好规划问题。偏好规划可以被视为经典规划问题的扩展，它关注于目标达成方式的定量和定性用户定义偏好。作者基于概率线性时序逻辑（probabilistic LTL-style logic）来表示偏好，并开发了P4Solver，这是一个基于SMT求解器的规划器，它可以将问题简化为二次规划问题，并使用如Z3这样的SMT求解器进行解决。
在介绍部分，作者首先回顾了经典规划问题，指出经典规划问题主要是寻找一个动作序列，以从初始状态达到一组用户定义的目标状态。然而，在现实中，许多问题的用户可能对某些特殊动作或状态有偏好，这就促使了基于偏好的规划方法的提出，以将规划与用户偏好结合起来。
传统上，偏好规划的研究多数基于非确定性转换系统。然而，在现实中，系统动作的效果往往是不可预测的。尽管我们无法精确知道动作之后会发生什么，但某些事件发生的频率比其他事件更高或更低。这激励了研究者们将概率纳入考虑，从而产生了概率偏好规划。
在文章中，作者提出了一个新的概率偏好规划问题，并针对马尔可夫决策过程进行了阐述。在这个问题中，用户定义的偏好基于概率LTL风格的逻辑，这种逻辑能够丰富地表达用户对于系统在达到目标时行为的偏好。P4Solver通过将问题转化为二次规划问题来计算优先计划，解决了这个问题，并可以使用Z3等SMT求解器来求解。作者通过两个精选案例研究来阐述了框架。
在现实世界中，大多数系统的行为是不确定的，因此，如何在不确定性中根据概率偏好做出选择成为了一个重要的研究课题。概率偏好规划能够使规划过程更加灵活和符合实际，比如在交通规划、资源分配等领域具有重要的应用价值。
概率偏好规划的研究为MDPs带来了新的挑战和机遇。它不仅增加了规划问题的复杂性，还需要更为复杂和高效的算法来处理。概率偏好规划的核心是将用户偏好集成到规划算法中，使得最终的规划结果不仅满足问题的基本约束，同时也能满足用户的偏好需求，从而达到更好的决策效果。随着人工智能与机器学习技术的不断发展，概率偏好规划的研究将会更加深入，为解决现实世界中的复杂问题提供有力的工具和方法。
