An Axiomatization for the Terminal Cycle

Milner proposed an axiomatization for the Kleene star in basic process algebra, in the presence of deadlock and empty process, modulo bisimulation equivalence. In this paper, Milner's axioms are adapted to the terminal cycle x ! , which executes x infinitely many times in a row, and it is shown that this axiomatization is complete for the terminal cycle in basic process algebra with deadlock and empty process modulo bisimulation. 1 Introduction Kleene [15] defined a binary operator x y in the context of finite automata, which denotes the iterate of x and y. Intuitively, the expression x y can choose to execute either x, after which it evolves into x y again, or y, after which it terminates. A feature of the Kleene star is that on the one hand it can express recursion, while on the other hand it can be captured in equational laws. Hence, one does not need metaprinciples such as the Recursive Specification Principle from Bergstra and Klop [10]. Kleene formulated several equa..