Skip to main content
SpringerLink
Log in

On the synthesis of an asynchronous reactive module

  • Conference paper
  • First Online:
Book cover Automata, Languages and Programming (ICALP 1989)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 372))

Included in the following conference series:

Abstract

We consider the synthesis of a reactive asynchronous module which communicates with its environment via the shared input variable x and the shared output variable y, assuming that the module is specified by the linear temporal formula ϕ(x,y). We derive from ϕ(x,y) another linear formula χ(r,w,x,y), with the additional scheduling variables r,w, and show that there exists a program satisfying ϕ iff the branching time formula (∀r,w,x)(∃y)Aχ(r,w,x,y) is valid over all tree models. For the restricted case that all variables range over finite domains, the validity problem is decidable, and we present an algorithm, of doubly exponential time and space complexity, for constructing a program that implements the specification whenever it is implementable. In addition, we provide some matching lower bounds.

The work of this author was partially supported by the Israel ministry of science and development, the national council for research and development.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. P.C. Attie and E.A. Emerson, Synthesis of concurrent systems with many similar sequential processes, Proc. 16th ACM Symp. Princ. of Prog. Lang., 1989, pp. 191–201.

    Google Scholar 

  2. M. Abadi, L. Lamport, and P. Wolper, Realizable and unrealizable concurrent program specifications, Proc. 16th Int. Colloq. Aut. Lang. Prog., 1989. To appear in the LNCS-series, Springer.

    Google Scholar 

  3. J. Bacon, Substance and first-order quantification over individual-concepts, J. Symb. Logic 45, 1980, pp. 193–203.

    Google Scholar 

  4. H. Barringer, The use of temporal logic in the compositional specification of concurrent systems, Temporal Logics and Their Applications (A. Galton, ed.), Academic Press, London, 1987, pp. 53–90.

    Google Scholar 

  5. H. Barringer, R. Kuiper, and A Pnueli, Now you may compose temporal logic specifications, Proc. 16th ACM Symp. Theory of Comp., 1984, pp. 51–63.

    Google Scholar 

  6. H. Barringer, R. Kuiper, and A Pnueli, A really abstract concurrent model and its temporal logic, Proc. 13th ACM Symp. Princ. of Prog. Lang., 1986, pp. 173–183.

    Google Scholar 

  7. J.R. Büchi and L.H. Landweber, Solving sequential conditions by finite-state strategies, Trans. Amer. Math. Soc. 138, 1969, pp. 295–311.

    Google Scholar 

  8. E.M. Clarke, E.A. Emerson, and A.P. Sistla, Automatic verification of finite state concurrent systems using temporal logic specifications, ACM Trans. Prog. Lang. Sys. 8, 1986, pp. 244–263.

    Article  Google Scholar 

  9. A.K. Chandra, D.C. Kozen, and L.J. Stockmeyer, Alternation, J. ACM 28, 1981, pp. 114–133.

    Article  Google Scholar 

  10. R.L. Constable, Constructive mathematics as a programming logic I: Some principles of theory, Ann. Discrete Math. 24, 1985, pp. 21–38.

    Google Scholar 

  11. D.L. Dill, Trace Theory for Automatic Hierarchical Verification of Speed-Independent Circuits, Ph.D. thesis, CMU, 1988. Available as Technical Report CMU-CS-88-119.

    Google Scholar 

  12. E.A. Emerson and E.M. Clarke, Using branching time temporal logic to synthesize synchronization skeletons, Sci. Comp. Prog. 2, 1982, pp. 241–266.

    Article  Google Scholar 

  13. E.A. Emerson and J.Y. Halpern, 'sometimes’ and ‘not never’ revisited: On branching time versus linear time, J. ACM 33, 1986, pp. 151–178.

    Article  Google Scholar 

  14. E.A. Emerson and C.S. Jutla, The complexity of tree automata and logic of programs, Proc. 29th IEEE Symp. Found. of Comp. Sci., 1988, pp. 328–337.

    Google Scholar 

  15. E.A. Emerson and C.S. Jutla, On simultaneously determinizing and complementing w-automata, Proc. 4th IEEE Symp. Logic in Comp. Sci., 1989. To appear.

    Google Scholar 

  16. E.A. Emerson and A.P. Sistla, Deciding full branching time logic, Inf. and Cont. 61, 1984, pp. 175–201.

    Article  Google Scholar 

  17. M.J. Fischer and R.E. Ladner, Propositional dynamic logic of regular programs, J. Comp. Sys. Sci. 18, 1979, pp. 194–211.

    Article  Google Scholar 

  18. R. Hossley and C. Rackoff, The emptiness problem for automata on infinite trees, Proc. 13th IEEE Symp. Switching and Automata Theory, 1972, pp. 121–124.

    Google Scholar 

  19. T. Hafer and W. Thomas, Computation tree logic CTL* and path quantifiers in the monadic theory of the binary tree, Proc. 14th Int. Colloq. Aut. Lang. Prog., Lec. Notes in Comp. Sci. 267, Springer, 1987, pp. 269–279.

    Google Scholar 

  20. L. Lamport, What good is temporal logic, Proc. IFIP Congress (R.E.A. Mason, ed.), North-Holland, 1983, pp. 657–668.

    Google Scholar 

  21. L. Lamport, Personal Communication, 1986.

    Google Scholar 

  22. Z. Manna and R.J. Waldinger, A deductive approach to program synthesis, ACM Trans. Prog. Lang. Sys. 2, 1980, pp. 90–121.

    Article  Google Scholar 

  23. Z. Manna and P. Wolper, Synthesis of communicating processes from temporal logic specifications, ACM Trans. Prog. Lang. Sys. 6, 1984, pp. 68–93.

    Article  Google Scholar 

  24. A. Pnueli and R. Rosner, A framework for the synthesis of reactive modules, Proc. Intl. Conf. on Concurrency: Concurrency88 (F.H. Vogt, ed.), Lec. Notes in Comp. Sci. 335, Springer, 1988, pp. 4–17.

    Google Scholar 

  25. A. Pnueli and R. Rosner, On the synthesis of a reactive module, Proc. 16th ACM Symp. Princ. of Prog. Lang., 1989, pp. 179–190.

    Google Scholar 

  26. M.O. Rabin, Automata on Infinite Objects and Churc's Problem, Volume 13 of Regional Conference Series in Mathematics, Amer. Math. Soc., 1972.

    Google Scholar 

  27. S. Safra, On the complexity of ω-automata, Proc. 29th IEEE Symp. Found. of Comp. Sci., 1988, pp. 319–327. An extended version to appear in J. Comp. Sys. Sci.

    Google Scholar 

  28. A.P. Sistla, M.Y. Vardi, and P. Wolper, The complementation problem for Büchi autamata with application to temporal logic, Theor. Comp. Sci. 49, 1987, pp. 217–237.

    Article  Google Scholar 

  29. M.Y. Vardi and L.J. Stockmeyer, Improved upper and lower bounds for modal logics of programs, Proc. 17th ACM Symp. Theory of Comp., 1985, pp. 240–251.

    Google Scholar 

  30. M.Y. Vardi and P. Wolper, Automata theoretic techniques for modal logics of programs, J. Comp. Sys. Sci. 32, 1986, pp. 183–221.

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, The Weizmann Institute of Science, 76100, Rehovot, Israel

    Amir Pnueli & Roni Rosner

Authors
  1. Amir Pnueli
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Roni Rosner
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Giorgio Ausiello Mariangiola Dezani-Ciancaglini Simonetta Ronchi Della Rocca

Rights and permissions

Reprints and permissions

Copyright information

© 1989 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Pnueli, A., Rosner, R. (1989). On the synthesis of an asynchronous reactive module. In: Ausiello, G., Dezani-Ciancaglini, M., Della Rocca, S.R. (eds) Automata, Languages and Programming. ICALP 1989. Lecture Notes in Computer Science, vol 372. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0035790

Download citation

  • DOI: https://doi.org/10.1007/BFb0035790

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-51371-1

  • Online ISBN: 978-3-540-46201-9

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation