PDL满意度决策算法：基于On-the-y表的研究

"这篇论文研究了基于On-the-y表的PDL（命题动态逻辑）满意度决策算法，旨在解决PDL的可满足性问题。PDL是一种用于程序推理的逻辑系统，其公式包含布尔运算和动作模态。文章指出，虽然PDL的可满足性问题是EXPTIME完全的，但现有的决策程序在理论和实践中都存在不足。Fischer和Ladner以及Pratt提出的早期算法在实际应用中并不理想。" **命题动态逻辑（PDL）** PDL是逻辑推理中的一个重要工具，主要用于描述和分析程序的行为。它扩展了传统的布尔逻辑，引入了动作模态，如序列组合、非确定性选择、重复和测试。这些模态允许表达复杂的程序结构和控制流。 **PDL的可满足性问题** PDL的可满足性问题是判断一个给定的PDL公式是否能在某个模型下被满足，这是一个计算复杂度为EXPTIME完全的问题。这意味着存在一个最优的时间复杂度下限，但找到这样的算法在实际中极具挑战性。 **基于On-the-y表的算法** 论文提出了一种新的决策算法，该算法构建了一个有限根树，其中包含祖先循环，并且能够区分好循环和坏循环。这个算法通过表格形式进行操作，具有并行化潜力，因为它可以独立探索每个分支。然而，尽管易于实现，其最坏情况下的时间复杂度是2EXPTIME，而不是理想的EXPTIME。 **平均情况行为** 与某些在平均情况下表现良好的EXPTIME完全问题的算法不同，PDL的决策程序在理论和实践中都存在挑战。这包括算法的可靠性、完整性，以及在处理常见实例时的实际性能。 **Fischer和Ladner以及Pratt的算法** Fischer和Ladner以及Pratt提出的早期PDL决策程序虽然理论上完整，但在实际应用中并不实用，主要是因为它们构建的解析结构过于复杂，不适合大规模或复杂的问题。 **PDL决策程序的挑战** PDL满足性决策程序需要平衡理论上的正确性和实际运行效率。论文中提到的新算法试图在这两者之间找到一个折衷，通过使用On-the-y表和循环信息传递来提高效率。 **原型实现** 论文作者实现了一个原型系统TWB，该系统可以用来验证基于On-the-y表的PDL满意度算法的有效性，并为后续研究提供了基础。 **关键词** 关键词涵盖了PDL，自动推理，表演算（tableaux），以及决策过程，强调了论文涉及的核心概念和技术领域。 这篇研究聚焦于改善PDL的决策算法，特别是通过On-the-y表的方法来提高效率，同时保持理论的正确性，以应对PDL可满足性问题的复杂性。