Synchronization expressions and languages

New constructs for synchronization termed synchronization expressions (SEs) have been developed as high-level language constructs for parallel programming languages. We introduce a new family of languages named synchronization languages which we use to give a precise semantic description for SEs. Under this description, relations such as equivalence and inclusion between SEs can be easily understood and tested. In practice, it also provides us with a systematic way for the implementation as well as the simplification of SEs in parallel programming languages. We also show that each synchronization language is closed under the following rewriting rules: (1) a_sb_s →b_sa_s, (2) a_tb_t→b_ta_t, (3) a_s b_t→b_ta_s, (4) a_ta _sb_tb_s→b_tb_sa _ta_s and also h(a_ta_sb_t b_s)→h(b_tb_sa_ta _s) for any morphism h that satisfies certain conditions which will be specified in the paper. We show that this property can be used to reduce the number of states of a finite automaton that describes a synchronization language