Published in Volume XXI, Issue 2, 2011, pages 175-198

Authors: L. Cardelli, C. Laneve


We introduce reversible structures, an algebra for massive concurrent systems, where terms retain bits of causal dependencies that allow one to reverse computation histories. We then study the implementation of (weak coherent) reversible structures in three-domains DNA strands, which is the natural model that has inspired reversible structures. We finally provide schemas for modeling significant synchronization patterns of process algebra into reversible structures and discuss the encoding of asynchronous Reversible CCS.

Full Text (PDF)


[1] G. Boudol and I. Castellani. Permutation of transitions: An event structure semantics for CCS and SCCS. In Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency, volume 354 of Lecture Notes in Computer Science, pages 411-427. Springer, 1989.

[2] L. Cardelli. Strand algebras for DNA computing. In DNA 2009, volume 5877 of Lecture Notes in Computer Science, pages 12-24, 2009.

[3] L. Cardelli. Two-domain DNA strand displacement. In Developments in Computational Models (DCM 2010), volume 25 of EPTCS, pages 33-47, 2010.

[4] L. Cardelli and C. Laneve. Reversible structures. In Proceedings of 9th Int. Conf. on Computational Methods in Systems Biology (CMSB 2011), ACM Digital Library, 2011.

[5] V. Danos and J. Krivine. Reversible communicating systems. In CONCUR 2004, volume 3170 of Lecture Notes in Computer Science, pages 292-307, 2004.

[6] V. Danos and J. Krivine. Transactions in RCCS. In CONCUR 2005, volume 3653 of Lecture Notes in Computer Science, pages 398-412. Springer, 2005

[7] C. Fournet and G. Gonthier. The reflexive cham and the join-calculus. In Proc. of the 23rd Symposium on Principles of Programming Languages (POPL ’96), pages 372-385. ACM, 1996.

[8] D. T. Gillespie. Exact stochastic simulation of coupled chemical reactions. J. Phys. Chem, 81:2340-2361, 1977.

[9] I. Lanese, C. A. Mezzina, and J.-B. Stefani. Reversing higher-order pi. In Proceedings of CONCUR 2010, volume 6269 of Lecture Notes in Computer Science, pages 478-493. Springer, 2010.

[10] C. Laneve and L. Padovani. Smooth orchestrators. In Foundations of Software Science and Computation Structures, 9th Int. Conf (FOSSACS 2006), volume 3921 of Lecture Notes in Computer Science, pages 32-46. Springer, 2006.

[11] J.-J. L´evy. An algebraic interpretation of the lambda-beta-k-calculus; and an application of a labelled lambda -calculus. Theor. Comput. Sci., 2(1):97-114, 1976.

[12] R. Milner. A Calculus of Communicating Systems, volume 92 of Lecture Notes in Computer Science. Springer, 1980.

[13] R. Milner, J. Parrow, and D. Walker. A calculus of mobile processes, i and ii. Inf. Comput., 100(1):1-77, 1992.

[14] U. Nestmann and B. C. Pierce. Decoding choice encodings. Inf. Comput., 163(1):1-59, 2000.

[15] I. Phillips and I. Ulidowski. Reversibility and models for concurrency. In Proceedings of SOS 2007, volume 192 of ENTCS, pages 93-108, 2007.

[16] I. Phillips and I. Ulidowski. Reversing algebraic process calculi. J. Log. Algebr. Program., 73(1-2):70-96, 2007.

[17] L. Qian and E. Winfree. A simple dna gate motif for synthesizing largescale circuits. In 14th International Meeting on DNA Computing, volume 5347 of Lecture Notes in Computer Science, pages 70-89. Springer, 2008.

[18] D. Y. Zhang and E. Winfree. Control of dna strand displacement kinetics using toehold exchange. Journal of the American Chemical Society, 131(47):17303-17314, 2009.


  title={Reversibility in Massive Concurrent Systems},
  author={L. Cardelli and C. Laneve},
  journal={Scientific Annals of Computer Science},
  organization={``A.I. Cuza'' University, Iasi, Romania},
  publisher={``A.I. Cuza'' University Press}