We verify a simple version of the alternating bit protocol in the system ACPτ (Algebra of Communicating Processes with silent actions) augmented with Koomen's fair abstraction rule.

doi.org/10.1007/3-540-16444-8_1
International Spring School on Mathematical Methods of Specification and Synthesis of Software Systems
Centrum Wiskunde & Informatica, Amsterdam (CWI), The Netherlands

Bergstra, J., & Klop, J. W. (1986). Verification of an alternating bit protocol by means of process algebra protocol. In Lecture Notes in Computer Science/Lecture Notes in Artificial Intelligence (pp. 9–23). doi:10.1007/3-540-16444-8_1