On the synthesis of a reactive module

ABSTRACT

We consider the synthesis of a reactive module with input x and output y, which is specified by the linear temporal formula @@@@(x, y). We show that there exists a program satisfying @@@@ iff the branching time formula (∀x) (∃y) A@@@@(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 for constructing the program whenever it exists. The algorithm is based on a new procedure for checking the emptiness of Rabin automata on infinite trees in time exponential in the number of pairs, but only polynomial in the number of states. This leads to a synthesis algorithm whose complexity is double exponential in the length of the given specification.

REFERENCES

• Bac80: J. Bacon, Substance and first-order quantification over individual-concepts, J. Symb. Logic 45, 1980, pp. 193-203.
• BL69: J.R. B Schi and L.H. Landweber, Solving sequential conditions by finite-state strategies, Trans. Amer. Math. Soc. 138, 1969, pp. 295-311.
• CE81: Edmund M. Clarke , E. Allen Emerson, Design and Synthesis of Synchronization Skeletons Using Branching-Time Temporal Logic, Logic of Programs, Workshop, p.52-71, May 01, 1981
• CES86: E. M. Clarke , E. A. Emerson , A. P. Sistla, Automatic verification of finite-state concurrent systems using temporal logic specifications, ACM Transactions on Programming Languages and Systems (TOPLAS), v.8 n.2, p.244-263, April 1986 [doi>10.1145/5397.5399]
• Chu63: A. Church, Logic, arithmetic and automata, Pro~. 196~ I~zt. Congr. Math., Upsala, 1963, pp. 23-25.
• Con85: R.L. Constable, Constructive mathematics as a programming logic I: some principles of theory, Ann. Discrete Math. 24, 1985, pp. 21-38.
• EH86: E. Allen Emerson , Joseph Y. Halpern, “Sometimes” and “not never” revisited: on branching versus linear time temporal logic, Journal of the ACM (JACM), v.33 n.1, p.151-178, Jan. 1986 [doi>10.1145/4904.4999]
• EJ88: E.A. Emerson and C.S. Jutla, The complexity of tree automata and logic of programs, Proc. ~9~h IEEE Syrup. Found. Comp. Sci., 1988.
• Elg61: C.C. Elgot, Decision problems of finite automata design and related arithmetics, Tra~s. Amer. Math. Soc. 98, 1961, pp. 21- 52.
• Eme85: E. Allen Emerson, Automata, Tableaux and Temporal Logics (Extended Abstract), Proceedings of the Conference on Logic of Programs, p.79-88, June 17-19, 1985
• ES84: E.A. Emerson and A.P. Sistl~, Deciding full branching time logic, Inf. and Coat. 61, 1984, pp. 175-201.
• GH82: Yuri Gurevich , Leo Harrington, Trees, automata, and games, Proceedings of the fourteenth annual ACM symposium on Theory of computing, p.60-65, May 05-07, 1982, San Francisco, California, United States [doi>10.1145/800070.802177]
• GPSS80: Dov Gabbay , Amir Pnueli , Saharon Shelah , Jonathan Stavi, On the temporal analysis of fairness, Proceedings of the 7th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.163-173, January 28-30, 1980, Las Vegas, Nevada [doi>10.1145/567446.567462]
• Har87: David Harel, Statecharts: A visual formalism for complex systems, Science of Computer Programming, v.8 n.3, p.231-274, June 1, 1987 [doi>10.1016/0167-6423(87)90035-9]
• HP85: D. Harel , A. Pnueli, On the development of reactive systems, Logics and models of concurrent systems, Springer-Verlag New York, Inc., New York, NY, 1989
• HR72: R. Hossley and C. Rackoff, The emptiness problem for automata on infinite trees, Proc. 13th IEEE Syrup. Switching and Automata Theory, 1972, pp. 121-124.
• HT87: T. Hafer , W. Thomas, Computation tree logic CTL* and path quantifiers in the monadic theory of the binary tree, 14th International Colloquium on Automata, languages and programming, p.269-279, July 1987, Karlsruhe, Germany
• MP82: Z. Manna and A. Pnueli, Verification of concurrent programs: the temporal framework, The Correctneas Problem in Computer Scier~ee (R.S. Boyer and J.S. Moore, eds.), Academic Press, London, 1982, pp. 215-273.
• MS85: David E. Muller , Paul E. Schupp, Alternating automata on infinite objects, determinacy and Rabin's theorem, Automata on Infinite Words, Ecole de Printemps d'Informatique Théorique,, p.100-107, May 14-18, 1984
• MW80: Zohar Manna , Richard Waldinger, A Deductive Approach to Program Synthesis, ACM Transactions on Programming Languages and Systems (TOPLAS), v.2 n.1, p.90-121, Jan. 1980 [doi>10.1145/357084.357090]
• MW84: Zohar Manna , Pierre Wolper, Synthesis of Communicating Processes from Temporal Logic Specifications, ACM Transactions on Programming Languages and Systems (TOPLAS), v.6 n.1, p.68-93, Jan. 1984 [doi>10.1145/357233.357237]
• Pnu77: A. Pnueli, The temporal logic of programs, Proc. 18th IEEE Syrup. Found. Comp. Sci., 1977, pp. 46-57.
• Pnu85: A. Pnueli, In transition from global to modular temporal reasoning about programs, Logics and models of concurrent systems, Springer-Verlag New York, Inc., New York, NY, 1989
• Pnu86: A Pnueli, Applications of temporal logic to the specification and verification of reactive systems: a survey of current trends, Current trends in concurrency. Overviews and tutorials, Springer-Verlag New York, Inc., New York, NY, 1986
• Rab69: M.O. Rabin, Decidability of second order theories and automata on infinite trees, Tra~s. A mer. Math. Soc. 141, 1969, pp. 1- 35.
• Rab72: Michael Oser Rabin, Automata on Infinite Objects and Church's Problem, American Mathematical Society, Boston, MA, 1972
• Saf88: S. Safra, On the complexity of wautomata, Proc. 29th IEEE Syrup. Found. Comp. Sci.~ 1988.
• SC85: A. P. Sistla , E. M. Clarke, The complexity of propositional linear temporal logics, Journal of the ACM (JACM), v.32 n.3, p.733-749, July 1985 [doi>10.1145/3828.3837]
• Tho: W. Thomas, Automata on infinite objects, Handbook o/ Theoretical Computer Science, North-Holland. To appear.
• VS85: M Y Vardi , L Stockmeyer, Improved upper and lower bounds for modal logics of programs, Proceedings of the seventeenth annual ACM symposium on Theory of computing, p.240-251, May 06-08, 1985, Providence, Rhode Island, United States [doi>10.1145/22145.22173]
• VW86: Moshe Y Vardi , Pierre Wolper, Automata-Theoretic techniques for modal logics of programs, Journal of Computer and System Sciences, v.32 n.2, p.183-221, April 1986 [doi>10.1016/0022-0000(86)90026-7]
• WL69: R.:f. Waldlnger and R.C.T. Lee, PROW: a step towrds automatic program writing, Proc. First Int. Joint Conf. on Artificial Inteligenc~, 1969, pp. 241-252.

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Mechanical theorem proving

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES

  F. Theory of Computation
  F.1 COMPUTATION BY ABSTRACT DEVICES
      F.1.1 Models of Computation
          Subjects: Automata (e.g., finite, push-down, resource-bounded)
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
          Subjects: Logics of programs
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES

General Terms:
Algorithms, Design, Languages, Theory