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.

International Spring School on Mathematical Methods of Specification and Synthesis of Software Systems
Centrum Wiskunde & Informatica, Amsterdam, The Netherlands

Bergstra, J.A, & 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