A Process Algebraic View of I/O Automata

Appears: Theoretical Computer Science, 138:391-423, 1995.

Abstract: Input/Output Automata are a widely used formalism for the specification and verification of concurrent algorithms. Unfortunately, they lack an algebraic characterization, a formalization which has been fundamental for the success of theories like CSP, CCS and ACP. We present a many-sorted algebra for I/O Automata that takes into account notions such as interface, input enabling, and local control. It is sufficiently expressive for representing all finitely branching transition systems, hence all I/O automata with a finitely branching transition relation. Our presentation includes a complete axiomatization of the external trace preorder relation over recursion free processes with input and output.

Download the full paper from the publisher.

Download a preliminary version of the paper.