An algebraic specification of a daisy chain arbiter

There have been few studies on formal approaches to the specification and realization of asynchronous digital circuits. The paper describes an algebraic method of specifying the abstract behavior of an asynchronous daisy chain arbiter as an example of them. In asynchronous circuits, changes of inputs cause state transitions. Thus the states after transitions are determined by the states before the transitions and the inputs after the changes, and when one component make a transition, some of the other components do not. The paper presents a representation of these relations. This algebraic method can be applied to many of the other asynchronous digital circuits