ML Anthology

Synthesis Algorithm for Recursive Process by Μ-Calculus (Extended Abstract)

Shigetomo Kimura, Atsushi Togashi, Norio Shiratori
ALT 1994 pp. 379-394
doi:10.1007/3-540-58520-6_78 /alt/1994/kimura1994alt-synthesis/

Abstract

This paper proposes an inductive synthesis algorithm for a recursive process from the enumeration of facts, which must be satisfied by the target process. We adopt a subcalculus of μ -calculus to represent facts of a process. First, a new preorder ≤_ d on recursive processes is introduced in such a way that p ≤_d q means that p ⊨ f implies q ⊨ f , for all formulae f in the subcalculus. Then, we present the synthesis algorithm. The correctness of the algorithm consists in that it only produces processes that satisfy the given facts. By adding more and more facts, the algorithm will eventually produce the target process. It will be shown that the algorithm is complete for the subcalculus.

PDF ALT Semantic Scholar

Cite

Text

Kimura et al. "Synthesis Algorithm for Recursive Process by Μ-Calculus (Extended Abstract)." International Conference on Algorithmic Learning Theory, 1994. doi:10.1007/3-540-58520-6_78

Markdown

[Kimura et al. "Synthesis Algorithm for Recursive Process by Μ-Calculus (Extended Abstract)." International Conference on Algorithmic Learning Theory, 1994.](https://mlanthology.org/alt/1994/kimura1994alt-synthesis/) doi:10.1007/3-540-58520-6_78

BibTeX

@inproceedings{kimura1994alt-synthesis,
  title     = {{Synthesis Algorithm for Recursive Process by Μ-Calculus (Extended Abstract)}},
  author    = {Kimura, Shigetomo and Togashi, Atsushi and Shiratori, Norio},
  booktitle = {International Conference on Algorithmic Learning Theory},
  year      = {1994},
  pages     = {379-394},
  doi       = {10.1007/3-540-58520-6_78},
  url       = {https://mlanthology.org/alt/1994/kimura1994alt-synthesis/}
}