A process algebraic view of I/O automata
Roberto Segala · DSpace@MIT (Massachusetts Institute of Technology) · 1992
The Input/Output Automata formalism of Lynch and Tuttle is a widely used framework for the specification and verification of concurrent algorithms. Unfortunately, it has never been provided with 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 quiescent preorder relation over recursion free processes with input and output. Finally, we give some example specifications and use them to show the methodology of verification based on our algebraic approach.