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.
A part of this study is supported by Grants from the Asahi Glass Foundation and Research Funds from Japanese Ministry of Education
Preview
Unable to display preview. Download preview PDF.
References
Angluin, D.: “Learning Regular Sets from Queries and Counterexamples”, Inf. and Comput, 75, pp. 87–106 (1987).
Brookes, S.D., C.A.R Hoare and A.W. Roscoe: “A Theory of Communicating Sequential Processes”, J. ACM., 31, 3, pp. 560–599 (1984).
Clocksin, W.F. and C.S. Mellish: “Programming in Prolog”, Springer-Verlag(1981).
Fantechi, A., S. Gnesi S. and G. Ristori: “Compositional Logic Semantics and LOTOS”, Protocol Specification, Testing and Verification, XL., IFIP, pp. 365–378
Graf, S. and J. Sifakis: “A Logic for the Description of Non-deterministic Programs and Their Properties”, Inf. and contr., 68, pp. 254–270 (1986)
Hennessy, M. and R. Milner: “Algebraic Laws for Nondeterminism and Concurrency”, J. ACM., 32, 1, pp. 137–161 (1985).
Hennessy, M.: “Algebraic Theory of Processes”, The MIT Press(1988).
Hindley, J.R. and J.P. Seldin: “Introduction to Combinators and λ-Calculus”, London Mathematical Society Student Texts 1, Cambridge Univ. Press(1986).
Hoare, C.A.R.: “Communicating Sequential Process”, Prentice Hall(1985).
Kimura, S., A. Togashi and S. Noguchi: “A Synthesis Algorithm of Basic Processes by Modal Formulas” (in Japanese), Trans. IEICE, J75-D-I, pp. 1048–1061 (1992).
Kimura, S., A. Togashi and N. Shiratori: “Synthesis Algorithm for Recursive Processes by μ-calculus”, preprint.
Kozen, D.: “Results on the Propositional μ-calculus”, Theoret. Comput. Sci., 27, pp. 333–354 (1983).
Manna, Z. and P. Wolper: “Synthesis of Communicating Processes from Temporal Logic Specifications”, ACM Trans. on Programming Languages and Systems, 6, 1, pp. 68–93 (1984).
Milner, R.: “Communication and Concurrency”, Prentice-Hall(1989).
Park, D.: “Concurrency and automata on infinite sequences”, Lecture Notes in Comput. Sci. 104, pp. 167–183, Springer-Verlag(1981).
Gotzhein, R.: “Specifying Communication Services With Temporal Logic”, Protocol Specification, Testing and Verification, XL, pp. 295–309 (1990).
van Glabbeek, R.J.: “The Linear Time — Branching Time Spectrum”, Lecture Notes in Comput. Sci. 458, Springer-Verlag(1990).
Shapiro, E.Y.: “Inductive Inference of Theories From Facts”, Technical Report 192, Yale Univ(1981).
Stirling, C.: “A Proof-Theoretic Characterization of Observational Equivalence”, Theoretical Computer Science, 39, pp. 27–45 (1985).
Stirling, C.: “Modal Logics For Communicating Systems”, Theoretical Computer Science, 49, pp. 311–347 (1987).
Stirling, C.: “An Introduction to Modal and Temporal Logics for CCS”, Lecture Notes in Comput. Sci. 491, Springer-Verlag, pp. 2–20 (1991).
Streett, R.S. and E.A. Emerson: “An Automata Theoretic Decision Procedure for the Propositional Mu-Calculus”, Info. and Comput. 81, Academic Press, pp. 249–264 (1989).
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1994 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kimura, S., Togashi, A., Shiratori, N. (1994). Synthesis algorithm for recursive processes by μ-calculus. In: Arikawa, S., Jantke, K.P. (eds) Algorithmic Learning Theory. AII ALT 1994 1994. Lecture Notes in Computer Science, vol 872. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-58520-6_78
Download citation
DOI: https://doi.org/10.1007/3-540-58520-6_78
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-58520-6
Online ISBN: 978-3-540-49030-2
eBook Packages: Springer Book Archive