论文标题
具有全球变量的过程代数
A process algebra with global variables
论文作者
论文摘要
在标准过程代数中，并行组件不具有共同的状态并通过同步进行通信。这种交流的优点是它有助于构图推理。但是，对于在共享存储器上运行的并行组件运行的模型和分析系统，但是，通信 - 同步范式有时不方便。在本文中，我们研究了一个具有全球变量概念的过程代数。我们还提出了轩尼诗 - 米尔纳逻辑的扩展，以测试和设置全局变量的值，并证明了公式在扩展逻辑中的有效性和无数据逻辑性的有效性与没有集合逻辑的扩展逻辑中的公式的有效性之间的有效性，而没有集合的算法和基于州的Bisimrility。我们还将提出从具有全球变量的过程代数转换为MCRL2片段的翻译，该变量保留了公式在扩展的Hennessy-Milner逻辑中的有效性。
In standard process algebra, parallel components do not share a common state and communicate through synchronisation. The advantage of this type of communication is that it facilitates compositional reasoning. For modelling and analysing systems in which parallel components operate on shared memory, however, the communication-through-synchronisation paradigm is sometimes less convenient. In this paper we study a process algebra with a notion of global variable. We also propose an extension of Hennessy-Milner logic with predicates to test and set the values of the global variables, and prove correspondence results between validity of formulas in the extended logic and stateless bisimilarity and between validity of formulas in the extended logic without the set operator and state-based bisimilarity. We shall also present a translation from the process algebra with global variables to a fragment of mCRL2 that preserves the validity of formulas in the extended Hennessy-Milner logic.
