Inductive synthesis of recursive processes from logical properties

Shigetomo Kimura, Atsushi Togashi, Norio Shiratori

    Research output: Contribution to journalArticle

    Abstract

    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.

    Original languageEnglish
    Pages (from-to)257-284
    Number of pages28
    JournalInformation and Computation
    Volume163
    Issue number2
    DOIs
    Publication statusPublished - 2000

    Fingerprint

    Logical property
    Synthesis
    Preorder
    Output
    Enumeration
    Correctness
    Calculus
    Prototype
    Converge
    Imply

    ASJC Scopus subject areas

    • Computational Theory and Mathematics

    Cite this

    Inductive synthesis of recursive processes from logical properties. / Kimura, Shigetomo; Togashi, Atsushi; Shiratori, Norio.

    In: Information and Computation, Vol. 163, No. 2, 2000, p. 257-284.

    Research output: Contribution to journalArticle

    Kimura, Shigetomo ; Togashi, Atsushi ; Shiratori, Norio. / Inductive synthesis of recursive processes from logical properties. In: Information and Computation. 2000 ; Vol. 163, No. 2. pp. 257-284.
    @article{1f694c950b274f6ebcfd63815cda8a6a,
    title = "Inductive synthesis of recursive processes from logical properties",
    abstract = "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.",
    author = "Shigetomo Kimura and Atsushi Togashi and Norio Shiratori",
    year = "2000",
    doi = "10.1006/inco.2000.2883",
    language = "English",
    volume = "163",
    pages = "257--284",
    journal = "Information and Computation",
    issn = "0890-5401",
    publisher = "Elsevier Inc.",
    number = "2",

    }

    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 -