TY - JOUR

T1 - Inductive synthesis of recursive processes from logical properties

AU - Kimura, Shigetomo

AU - Togashi, Atsushi

AU - Shiratori, Norio

PY - 2000

Y1 - 2000

N2 - This paper proposes an inductive synthesis algorithm for a recursive process. To synthesize a process, facts, which must be satisfied by the target process, are given to the algorithm one by one since such facts are infinitely many in general. When n facts are input to the algorithm, it outputs a process which satisfies the given n facts. And this generating process is repeated infinitely many times. To represent facts of a process, we adopt a subcalculus of μ-calculus. First, we introduce a new preorder ≤d on recursive processes based on the subcalculus to discuss its properties. p ≤ d q means that p |= f implies q |= f, for all formulae f in the subcalculus. Then, its discriminative power and relationship with other preorders are also discussed. Finally, 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 could know it) by a given enumeration of facts, in the limit. A prototype system based on the algorithm is stated as well.

AB - This paper proposes an inductive synthesis algorithm for a recursive process. To synthesize a process, facts, which must be satisfied by the target process, are given to the algorithm one by one since such facts are infinitely many in general. When n facts are input to the algorithm, it outputs a process which satisfies the given n facts. And this generating process is repeated infinitely many times. To represent facts of a process, we adopt a subcalculus of μ-calculus. First, we introduce a new preorder ≤d on recursive processes based on the subcalculus to discuss its properties. p ≤ d q means that p |= f implies q |= f, for all formulae f in the subcalculus. Then, its discriminative power and relationship with other preorders are also discussed. Finally, 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 could know it) by a given enumeration of facts, in the limit. A prototype system based on the algorithm is stated as well.

UR - http://www.scopus.com/inward/record.url?scp=0034672930&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=0034672930&partnerID=8YFLogxK

U2 - 10.1006/inco.2000.2883

DO - 10.1006/inco.2000.2883

M3 - Article

AN - SCOPUS:0034672930

VL - 163

SP - 257

EP - 284

JO - Information and Computation

JF - Information and Computation

SN - 0890-5401

IS - 2

ER -