Reversible Truly Concurrent Process Algebra
Yong Wang
TL;DR
This paper introduces RCTC, a reversible extension of the truly concurrent process algebra CTC, with properties supporting various bisimulation equivalences, enabling more flexible modeling of reversible concurrent systems.
Contribution
It presents the first reversible truly concurrent process algebra RCTC with comprehensive bisimulation properties and laws, expanding the theoretical framework for reversible concurrent computation.
Findings
RCTC satisfies monoid and static laws
Includes a new expansion law for strongly forward-reverse bisimulations
Establishes congruence properties for both strongly and weakly bisimulations
Abstract
We design a reversible version of truly concurrent process algebra CTC which is called RCTC. It has good properties modulo several kinds of strongly forward-reverse truly concurrent bisimulations and weakly forward-reverse truly concurrent bisimulations. These properties include monoid laws, static laws, new expansion law for strongly forward-reverse truly concurrent bisimulations, \tau laws for weakly forward-reverse truly concurrent bisimulations, and congruences for strongly and weakly forward-reverse truly concurrent bisimulations.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsFormal Methods in Verification · Logic, programming, and type systems · Computability, Logic, AI Algorithms