Synthesis of algebraic processes based on process enumeration

Algebraic calculation systems for processes, e.g., Hoare's CSP [8] and Milner's CCS [13, 15], are used to describe communication processes and concurrent programs, etc., and applied to the verification problem [4-6]. On the other hand, most studies on the inductive inference have been concerned with finite automata, formal languages and their families, etc., but few have discussed algebraic processes. This is because they have nondeterministic properties, their parallel actions are difficult to handle, and their semantics are completed different from the cases of the traditional formal languages and automata. This paper presents synthesis algorithms for algebraic processes by modal formulas based on induction inference