We propose a formalisation of the notion of transaction, using a variant of CCS, RCCS, that distinguishes reversible and irreversible actions, and incorporates a distributed backtrack mechanism. Any weakly correct implementation of a transaction in CCS, once embedded in RCCS, automatically obtains a correct one. We show examples where this method allows for a more concise implementation and a simpler proof of correctness. © Springer-Verlag Berlin Heidelberg 2005.
CITATION STYLE
Danos, V., & Krivine, J. (2005). Transactions in RCCS. In Lecture Notes in Computer Science (Vol. 3653, pp. 398–412). Springer Verlag. https://doi.org/10.1007/11539452_31
Mendeley helps you to discover research relevant for your work.