On basic rewriting rules to verify communicating machines

An approach to proving some properties of the communication of communicating machines is presented. The methodology is based on a simple algebra, using rewriting systems on communicating words and homogeneous expressions. The semicommutations and partial commutations over an alphabet of sending and receiving messages suffice to guarantee the progress properties or the communication. Basic rules of an automatic validation communicating machine are defined in an algebraic fashion, without representing the global states, transitions, and contents of channels. Only the behavior is needed as a basis for the results obtained