确保分布式系统的活性性质（研究议程）

为了确立分布式系统的活性性质，常常需要做出公平性假设，但在许多情况下这会导致错误的结论。本文提出一份研究议程，旨在奠定并发理论的基础，使其能够在不做公平性假设的情况下确保分布式系统的活性性质。该理论将涵盖进程代数、时序逻辑和语义模型，以及对实时性的处理。该议程还包括开发一种方法论，使得该理论能够成功应用于现实分布式系统（包括无线网络的路由协议）的规约、分析与验证。当代进程代数和时序逻辑未能区分这样的两个系统：其中一个具有关键的活性性质而另一个没有，至少在仅假设 justness（一种强进展性质）而不假设公平性的情况下如此。建立一个替代框架涉及放弃识别强互模拟系统、发明新的归纳原理、为进程代数开发新的公理基础以及为操作语义开发新的同余格式，并创造对时间和概率的新处理。即便是像公平调度器或互斥协议这样的简单系统，在缺乏公平性假设时也无法在标准进程代数（或 Petri 网）中被准确规约。因此该工作涉及研究适当的语言或模型扩展及其表达能力。