期刊
JOURNAL OF LOGICAL AND ALGEBRAIC METHODS IN PROGRAMMING
卷 136, 期 -, 页码 -出版社
ELSEVIER SCIENCE INC
DOI: 10.1016/j.jlamp.2023.100924
关键词
Formal semantics; Process algebra; Concurrency; Reversibility
This article presents a general principle for checking the correctness of the definition of concurrency in concurrent calculi. It examines the use of reversibility in providing a criterion for assessing the correctness of concurrencies. The article introduces a syntactical definition of concurrency for CCSK and also shows the equivalence or refinement of this formalism to pre-existing definitions for reversible systems.
This article designs a general principle to check the correctness of the definition of concurrency (a.k.a. independence) of events for concurrent calculi. Concurrency relations are central in process algebras, but also two-sided: they are often defined independently on composable and on coinitial transitions, and no criteria exist to assess whether they interact correctly. This article starts by examining how reversibility can provide such a correctness of concurrencies criterion, and its implications. It then defines, for the first time, a syntactical definition of concurrency for CCSK, a reversible declension of the calculus of communicating systems. To do so, according to our criterion, requires to define concurrency relations for all types of transitions along two axes: direction (forward or backward) and concomitance (coinitial or composable). Our definition is uniform thanks to proved transition systems and satisfies our sanity checks: square properties, sideways diamonds, but also the reversible checks (reverse diamonds and causal consistency). We also prove that our formalism is either equivalent to or a refinement of pre-existing definitions of concurrency for reversible systems. We conclude by discussing additional criteria and possible future works.
作者
我是这篇论文的作者
点击您的名字以认领此论文并将其添加到您的个人资料中。
推荐
暂无数据