On the consistency of Koomen's Fair Abstraction Rule

AbstractWe construct a graph model for ACPτ, the algebra of communicating processes with silent steps, in which Koomen's Fair Abstraction Rule (KFAR) holds, and also versions of the Approximation Induction Principle (AIP) and the Recursive Definition & Specification Principles (RDP&RSP). We use this model to prove that in ACPT (but not in ACP!) each computably recursively definable process is finitely recursively definable