Is there a 'process algebra' to describe ACID transactions on a database? There appears to be this beautiful algebra to help you think through the implications of Communicating Sequential Processes by Hoare. 

What I'm wondering, is there an equivalent algebra that helps you think through ACID transactions on a database, where one suceeds and another rolls back?
There is a paper by Van Beek called An Algebraic Approach to Transactional Processes which describes adding transactions to process algebra:

(a :~ 0 . a:~ a + 2) II (a:~ 1 a:~ a X 2) ((a :~ 0 . a:~ a + 2)) II ((a:~ 1 a:~ a X 2))


This paper even delves into isolation levels. 

The author describes how in Communicating Sequential Processes (CSP), if you have a write blocked on a read, you can get into a deadlock scenario. 

The author references another paper J.A. Bergstra, A. Ponse, and J.J. van Warne. Process algebra with backtracking which allows for rollback of a failed CSP operation.  

There is discussion on the nature of transactions in K.P. Eswaran, J .N. Gray, R.A. Lorie, and 1.1. Traiger. On the notions of consistency and  predicate locks in a data base system. Communications of the ACM, 19(11)

The properties of transactions are described in ] J. Gray and A. Reuter. Transaction Processing: Concepts and Techniques.

The acid properties of transactions are described in J. Gray. The transaction concept: Virtues and limitations and in T. Haerder and A. Reuter. Principles of transaction-oriented database recovery