A Logic for True Concurrency
A Logic for True Concurrency
复制标题
DOI：
10.1145/2629638
复制
发表时间：
2014-07-01
影响因子：
2.5
通讯作者：
Crafa, Silvia
中科院分区：
文献类型：
--
作者：
Baldan, Paolo;Crafa, Silvia
我们提出了一种用于真并发的逻辑，其公式对计算中的事件及其因果依赖关系进行断言。所诱导的逻辑等价是遗传历史保持双相似性，并且可以确定该逻辑的片段，它们对应于文献中其他真并发行为等价关系：步双相似性、偏序集双相似性和历史保持双相似性。标准的亨尼西 - 米尔纳逻辑，以及（交错）双相似性，也作为一个片段被恢复。我们还提出了用不动点算子对该逻辑进行扩展，从而能够描述无限计算的因果和并发性质。这项工作有助于对真并发谱系进行合理的呈现，并有助于更深入地理解所涉及的行为等价关系之间的联系。
We propose a logic for true concurrency whose formulae predicate about events in computations and their causal dependencies. The induced logical equivalence is hereditary history-preserving bisimilarity, and fragments of the logic can be identified which correspond to other true concurrent behavioural equivalences in the literature: step, pomset and history-preserving bisimilarity. Standard Hennessy-Milner logic, and thus (interleaving) bisimilarity, is also recovered as a fragment. We also propose an extension of the logic with fix-point operators, thus allowing to describe causal and concun-ency properties of infinite computations. This work contributes to a rational presentation of the true concurrent spectrum and to a deeper understanding of the relations between the involved behavioural equivalences.