Inductive synthesis of recursive processes from logical properties

This paper proposes an inductive synthesis algorithm for a recursive proces s. To synthesize a process, facts, which must be satisfied by the target pr ocess, are given to the algorithm one by one since such facts are infinitel y many in general. When n facts are input to the algorithm, it outputs a pr ocess which satisfies the given n facts. And this generating process is rep eated infinitely many times. To represent facts of a process, we adopt a su bcalculus of mu -calculus. First, we introduce a new preorder less than or equal to (d) on recursive processes based on the subcalculus to discuss its properties. P less than or equal to (d) q means that p satisfies f implies q satisfies f, for all formulae f in the subcalculus. Then, its discrimina tive power and relationship with other preorders are also discussed. Finall y, we present the synthesis algorithm. The correctness of the algorithm can be stated that the output sequence of processes by the algorithm converges to a process, which cannot be distinguished from the intended one (if we c ould know it) by a given enumeration of facts, in the limit. A prototype sy stem based on the algorithm is stated as well. (C) 2000 Academic Press.