Two normal form theorems for CSP programs (Q1094869)

We define two normal forms for CSP programs. In the first normal form, each process contains only one I/O repetitive command and all its I/O commands appear as guards of this command. In the second normal form, all guards of this I/O repetitive command are I/O guards. We describe an inductive method that transforms any CSP program into an equivalent program in first or second normal form. The notion of equivalence is discussed. It is shown that no transformation into second normal form can preserve deadlock freedom.