M. Benevides and L. Schechter, A Propositional Dynamic Logic for CCS Programs, WoLLIC'08, pp.83-97, 2008.
DOI : 10.1007/978-3-540-69937-8_9

M. Bravetti and G. Zavattaro, On the expressive power of process interruption and compensation, Mathematical Structures in Computer Science, vol.4960, issue.03, pp.565-599, 2009.
DOI : 10.1007/s10270-006-0012-1

J. Broersen, Modal Action Logics for Reasoning about Reactive Systems, 2003.

J. Broersen, R. Wieringa, and J. Meyer, A fixed-point characterization of a deontic logic of regular action, Fundamenta Informaticae, vol.48, issue.2-3, pp.107-128, 2001.

R. Bruni, H. Melgratti, and U. Montanari, Nested Commits For Mobile Calculi: Extending Join, IFIP TCS'04, pp.563-576, 2004.
DOI : 10.1007/1-4020-8141-3_43
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.120.6285

R. Bruni, H. Melgratti, and U. Montanari, Theoretical foundations for compensations in flow composition languages, POPL'05, pp.209-220, 2005.
DOI : 10.1145/1047659.1040323
URL : http://basics.sjtu.edu.cn/~yuehg/popl/theoretical foundations for compensations in flow composition languages (2005).pdf

M. Butler and C. Ferreira, A Process Compensation Language, IFM'00, pp.61-76, 2000.
DOI : 10.1007/3-540-40911-4_5

M. Butler, C. Hoare, and C. Ferreira, A Trace Semantics for Long-Running Transactions, 25 Years of CSP, pp.133-150, 2004.
DOI : 10.1007/11423348_8
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.100.3195

L. Caires, C. Ferreira, and H. Vieira, A Process Calculus Analysis of Compensations, TGC'08, pp.87-103, 2009.
DOI : 10.1007/978-3-540-78739-6_21

P. Castro and T. Maibaum, Deontic action logic, atomic boolean algebras and fault-tolerance, Journal of Applied Logic, vol.7, issue.4, pp.441-466, 2009.
DOI : 10.1016/j.jal.2009.02.001
URL : http://doi.org/10.1016/j.jal.2009.02.001

V. Danos and J. Krivine, Reversible Communicating Systems, CONCUR'04, pp.292-307, 2004.
DOI : 10.1007/BFb0012800
URL : https://hal.archives-ouvertes.fr/hal-00784051

E. De-vries, V. Koutavas, and M. Hennessy, Communicating Transactions -(Extended Abstract ), CONCUR'10, pp.569-583, 2010.

C. Eisentraut and D. Spieler, Fault, Compensation and Termination in WS-BPEL??2.0 ??? A Comparative Analysis, WS-FM'08, pp.107-126, 2009.
DOI : 10.1007/11526841_24

D. Harel, D. Kozen, and J. Tiuryn, Dynamic logic, Handbook of Philosophical Logic, pp.497-604, 1984.

M. P. Herlihy and J. M. Wing, Linearizability: a correctness condition for concurrent objects, ACM Transactions on Programming Languages and Systems, vol.12, issue.3, pp.463-492, 1990.
DOI : 10.1145/78969.78972
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.142.5315

I. Lanese, C. Mezzina, and J. Stefani, Reversing Higher-Order Pi, CONCUR'10, pp.478-493, 2010.
DOI : 10.1007/978-3-642-15375-4_33

R. Lucchi and M. Mazzara, A pi-calculus based semantics for WS-BPEL, The Journal of Logic and Algebraic Programming, vol.70, issue.1, pp.96-118, 2007.
DOI : 10.1016/j.jlap.2006.05.007
URL : http://doi.org/10.1016/j.jlap.2006.05.007

M. Mazzara and I. Lanese, Towards a Unifying Theory for Web Services Composition, WS-FM, pp.257-272, 2006.
DOI : 10.1007/11841197_17
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.110.3155

J. Meyer, A different approach to deontic logic: deontic logic viewed as a variant of dynamic logic., Notre Dame Journal of Formal Logic, vol.29, issue.1, pp.109-136, 1988.
DOI : 10.1305/ndjfl/1093637776

C. H. Papadimitriou, The serializability of concurrent database updates, Journal of the ACM, vol.26, issue.4, pp.631-653, 1979.
DOI : 10.1145/322154.322158

D. Peleg, Concurrent dynamic logic, Journal of the ACM, vol.34, issue.2, pp.450-479, 1987.
DOI : 10.1145/23005.23008

R. Van-der-meyden, The dynamic logic of permission, Journal of Logic and Computation, vol.6, issue.3, pp.465-479, 1996.
DOI : 10.1093/logcom/6.3.465

C. Vaz and C. Ferreira, Towards Compensation Correctness in Interactive Systems, WS- FM'09, pp.161-177, 2010.
DOI : 10.1007/978-3-642-14458-5_10

C. Vaz, C. Ferreira, and A. Ravara, Dynamic Recovering of Long Running Transactions, TGC'08, pp.201-215, 2009.
DOI : 10.1007/11948148_27
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.413.3548

A. Lemma, Let s, s , s ? State(V ) The following equality holds: s\ X s ? s \ X s = s\ X s