天使进程

在系统的形式化建模中，恶魔式与天使式非确定性作为抽象机制起着基础作用。选择的天使式性质涉及在可能时避免失败的特性。作为一个概念，天使式选择最早出现在自动机理论和图灵机中，其可通过回溯实现。传统上它在精化演算（refinement calculus）中被研究，并已被证明在多种应用和精化技术中有用。最近它在关系、多关系和高阶模型中被研究。它已被用于建模用户交互、类游戏场景、定理证明策略、约束满足问题和控制系统。当考虑状态丰富的反应系统的形式化建模时，似乎很自然地应同时考虑两种类型的非确定性选择。然而，尽管在进程代数（即 Communicating Sequential Processes）背景下对天使式非确定性有若干处理，精化演算中天使式选择的对应物一直难以捉摸。在本论文中，我们在 Hoare 和 He 的 Unifying Theories of Programming 的关系设定下开发了一种语义，使得能够刻画 CSP 中的天使式非确定性。由于 CSP 进程通过设计（designs，即前置和后置条件对）在 UTP 中被赋予语义，我们首先引入一种天使设计（angelic designs）理论，以及一个同构的多关系模型，适用于刻画进程。然后我们通过强制实施 CSP 的健康条件（healthiness conditions）开发了反应式天使设计（reactive angelic designs）理论。最后，通过引入一种能够撤销事件历史的分歧（divergence）概念，我们获得了一个天使式选择避免分歧的模型。