优先级CSP扩展：符号化操作语义与优先级影响

"这篇论文探讨了优先级CSP（Concurrent Sequential Processes）的扩展和符号化，以及其语义学。作者A.W.罗斯科来自牛津大学计算机科学系，他在之前的工作中定义了一种类似CSP的操作语义，但存在一些限制，如自动提升τ动作、不允许克隆进程以及没有否定前提的规则。现在，他证明了这些限制在优先级运算符被引入的情况下仍然适用，取消了对否定前提的限制，从而扩展了CSP的表达能力。优先级的概念（Pri≤）允许对过程执行事件进行偏序，确保只有在没有更高优先级事件时，过程P才能执行事件x。这种扩展对描述实时系统等具有重要意义，因为可以更精确地控制事件的发生顺序。然而，Pri≤并不是经典CSP的一部分，因为它需要负前提，而这在大多数CSP模型中无法实现语义。" 本文详细研究了CSP的理论基础，特别是在操作语义方面。CSP是一种形式化方法，用于描述并发系统的行为，通常使用迹T和故障-发散N这样的模型来指定其语义。在SOS（结构化操作语义）框架下，CSP有一个清晰的操作语义描述。罗斯科先前的类CSP定义不允许规则中含有否定前提，这限制了某些复杂行为的表示。他的最新工作引入了优先级运算符Pri≤，这是一种用于控制并发事件执行顺序的方法，它通过限制不可见的τ动作来实现，使得只有在没有更高优先级事件阻塞时，事件才能发生。 在优先级CSP中，Pri≤的引入提供了一种无需构建特殊语义模型或 LTS（Labelled Transition System，标记状态转换系统）类型的方式来增强CSP的表达性，这对于实时系统分析特别有用。然而，由于Pri≤需要负前提，这在标准CSP中是不允许的，因此它在很多CSP模型中无法直接应用。罗斯科的工作展示了如何在保持原有操作语义性质的同时，扩展CSP以支持优先级控制，这对于理解和验证复杂的并发系统至关重要。 这篇论文深入讨论了CSP的理论扩展，特别是关于优先级控制的语义学，对于理解并发系统的行为模型和验证方法有着重要的理论贡献，并为后续研究提供了基础。