Independence and causality in the reversible Concurrent setting
File(s)
Accepted version
Author(s)
Aubert, Clément
Phillips, Iain
Ulidowski, Irek
Type
Conference Paper
Abstract
Among the formalisms that can be used to reason about concurrent systems, process calculi stand out both for their simple syntax and close connection to reversibility. They also offer approaches to study relations such as dependence, concurrency or causality between transitions,
useful in exploring e.g., causes of bugs or how to multi-thread executions. This paper offers two main contributions: first, we provide separate definitions of a dependence relation and an independence relation, and prove their complementarity on connected transitions instead of postulating it, as is usually done. We also prove that those relations, as well as the notions of event, concurrency, causality and conflict, are unique for any reversible system respecting basic sanity axioms. Second, we prove that the operational definitions of core independence and causality coincide with their characterisations using a pre-existing syntactic mechanism in reversible process calculi, namely communication keys.
useful in exploring e.g., causes of bugs or how to multi-thread executions. This paper offers two main contributions: first, we provide separate definitions of a dependence relation and an independence relation, and prove their complementarity on connected transitions instead of postulating it, as is usually done. We also prove that those relations, as well as the notions of event, concurrency, causality and conflict, are unique for any reversible system respecting basic sanity axioms. Second, we prove that the operational definitions of core independence and causality coincide with their characterisations using a pre-existing syntactic mechanism in reversible process calculi, namely communication keys.
Date Issued
2025-06-22
Date Acceptance
2025-04-11
Citation
Lecture Notes in Computer Science, 2025, 15716
ISBN
978-3-031-97062-7
ISSN
1611-3349
Publisher
Springer
Journal / Book Title
Lecture Notes in Computer Science
Volume
15716
Copyright Statement
Copyright © 2025 The Author(s), under exclusive license to Springer Nature Switzerland AG. This is the author’s accepted manuscript made available under a CC-BY licence in accordance with Imperial’s Research Publications Open Access policy (www.imperial.ac.uk/oa-policy)
License URL
Source
Seventeenth International Conference on Reversible Computation (RC 2025)
Publication Status
Published
Start Date
2025-07-03
Finish Date
2025-07-04
Coverage Spatial
Odense, Denmark
Date Publish Online
2025-06-22