Hostname: page-component-586b7cd67f-vdxz6 Total loading time: 0 Render date: 2024-11-21T23:08:07.308Z Has data issue: false hasContentIssue false
  • English
  • Français

Church's Problem Revisited

Published online by Cambridge University Press:  15 January 2014

Orna Kupferman  and
Moshe Y. Vardi
Orna Kupferman
Affiliation:
The Institute of Computer Science, Hebrew University, Jerusalem 91904, ISRAELE-mail:[email protected]
Moshe Y. Vardi
Affiliation:
Department Of Computer Science, Rice University, Houston, TEXAS 77005-1892, USAE-mail:[email protected]
Get access Rights & Permissions [Opens in a new window]

Abstract

In program synthesis, we transform a specification into a system that is guaranteed to satisfy the specification. When the system is open, then at each moment it reads input signals and writes output signals, which depend on the input signals and the history of the computation so far. The specification considers all possible input sequences. Thus, if the specification is linear, it should hold in every computation generated by the interaction, and if the specification is branching, it should hold in the tree that embodies all possible input sequences.

Often, the system cannot read all the input signals generated by its environment. For example, in a distributed setting, it might be that each process can read input signals of only part of the underlying processes. Then, we should transform a specification into a system whose output depends only on the readable parts of the input signals and the history of the computation. This is called synthesis with incomplete information. In this work we solve the problem of synthesis with incomplete information in its full generality. We consider linear and branching settings with complete and incomplete information. We claim that alternation is a suitable and helpful mechanism for coping with incomplete information. Using alternating tree automata, we show that incomplete information does not make the synthesis problem more complex, in both the linear and the branching paradigm. In particular, we prove that independently of the presence of incomplete information, the synthesis problems for CTL and CTL*. are complete for EXPTIME and 2EXPTIME, respectively.

Type
Research Article
Information
Bulletin of Symbolic Logic , Volume 5 , Issue 2 , June 1999 , pp. 245 - 263
Copyright
Copyright © Association for Symbolic Logic 1999

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

REFERENCES

[1] Abadi, M., Lamport, L., and Wolper, P., Realizable and unrealizable concurrent program specifications, Proceedings of the 16th international colloquium on automata, languages and programming, Lecture Notes in Computer Science, no. 372, Springer-Verlag, Berlin, 07 1989, pp. 1–17.Google Scholar
[2] Bernholtz, O., Vardi, M. Y., and Wolper, P., An automata-theoretic approach to branching-time model checking, Computer aided verification, Proceedings of the 6th international conference (Dill, D. L., editor), Lecture Notes in Computer Science, no. 818, Springer-Verlag, Berlin, 06 1994, pp. 142–155.Google Scholar
[3] Büchi, J. R. and Landweber, L. HG., Solving sequential conditions by finite-state strategies, Transactions of the American Mathematical Society, vol. 138 (1969), pp. 295–311.Google Scholar
[4] Church, A., Logic, arithmetics, and automata, Proceedings of the international congress of mathematicians, 1962, Institut Mittag-Leffler, 1963, pp. 23–35.Google Scholar
[5] Dill, D. L., Trace theory for automatic hierarchical verification of speed independent circuits, MIT Press, 1989.Google Scholar
[6] Emerson, A. E. and Sistla, A. P., Deciding full branching time logics, Information and Control, vol. 61 (1984), no. 3, pp. 175–201.Google Scholar
[7] Emerson, E. A., Temporal and modal logic, Handbook of theoretical computer science, 1990, pp. 997–1072.Google Scholar
[8] Emerson, E. A. and Clarke, E. M., Using branching time logic to synthesize synchronization skeletons, Science of Computer Programming, vol. 2 (1982), pp. 241–266.Google Scholar
[9] Emerson, E. A. and Halpern, J. Y., Decision procedures and expressiveness in the temporal logic of branching time, Journal of Computer and System Sciences, vol. 30 (1985), pp. 1–24.Google Scholar
[10] Emerson, E. A. and Halpern, J. Y., Sometimes and not never revisited: On branching versus linear time, Journal of the Association for Computing Machinery, vol. 33 (1986), no. 1, pp. 151–178.Google Scholar
[11] Emerson, E. A. and Jutla, C., The complexity of tree automata and logics of programs, Proceedings of the 29th IEEE symposium on foundations of computer science, White Plains, 10 1988, pp. 368–377.Google Scholar
[12] Gurevich, Y. and Shelah, S., Rabin's uniformization problem, this Journal, vol. 48 (1983), pp. 1105–1119.Google Scholar
[13] Harel, D. and Pnueli, A., On the development of reactive systems, Logics and models of concurrent systems (Apt, K., editor), NATO Advanced Summer Institutes, no. F-13, Springer-Verlag, 1985, pp. 477–498.Google Scholar
[14] Kumar, R. and Garg, V. K., Modeling and control of logical discrete event systems, Kluwer Academic Publishers, 1995.Google Scholar
[15] Kumar, R. and Shayman, M. A., Supervisory control of nondeterministic systems under partial observation and decentralization, Siam journal of control and optimization, 1995.Google Scholar
[16] Kupferman, O. and Vardi, M. Y., Module checking, Computer aided verification, Proceedings of the 8th international conference, Lecture Notes in Computer Science, no. 1102, Springer-Verlag, 1996, pp. 75–86.Google Scholar
[17] Kupferman, O. and Vardi, M. Y., Module checking revisited, Computer aided verification, Proceedings of the 9th international conference, Lecture Notes in Computer Science, no. 1254, Springer-Verlag, 1997, pp. 36–47.Google Scholar
[18] Kupferman, O. and Vardi, M. Y., Synthesiswith incomplete informatio, 2nd international conference on temporal logic, Kluwer Academic Publishers, Manchester, 07 1997, pp. 91–106.Google Scholar
[19] Lamport, L., Sometimes is sometimes “not never” —on the temporal logic of programs, Proceedings of the 7th ACM symposium on principles of programming languages, 01 1980, pp. 174–185.Google Scholar
[20] Manna, Z. and Waldinger, R., A deductive approach to program synthesis, Association for Computing Machinery Transactions on Programming Languages and Systems, vol. 2 (1980), no. 1, pp. 90–121.Google Scholar
[21] Muller, D. E. and Schupp, P. E., Alternating automata on infinite trees, Theoretical Computer Science, vol. 54 (1987), pp. 267–276.Google Scholar
[22] Muller, D. E. and Schupp, P. E., Simulating alternating tree automata by nondeterministic automata: new results and new proofs of theorems of Rabin, McNaughton and Safra, Theoretical Computer Science, vol. 141 (1995), pp. 69–107.Google Scholar
[23] Pnueli, A., The temporal logic of programs, Proceedings of the 18th IEEE symposium on foundation of computer science, 1977, pp. 46–57.Google Scholar
[24] Pnueli, A., The temporal semantics of concurrent programs, Theoretical Computer Science, vol. 13 (1981), pp. 45–60.Google Scholar
[25] Pnueli, A. and Rosner, R., On the synthesis of a reactive module, Proceedings of the 16th ACM symposium on principles of programming languages, Austin, 01 1989.Google Scholar
[26] Pnueli, A. and Rosner, R., On the synthesis of an asynchronous reactive module, Proceedings of the 16th international colloquium on automata, languages and programming, Lecture Notes in Computer Science, vol. 372, Springer-Verlag, 07 1989, pp. 652–671.Google Scholar
[27] Pnueli, A. and Rosner, R., Distributed reactive systems are hard to synthesize, Proceedings of the 31st IEEE symposium on foundation of computer science, 1990, pp. 746–757.Google Scholar
[28] Rabin, M.O., Weakly definable relations and special automata, Proceedings of symposia in mathematics, logic and foundations of set theory, North-Holland, 1970, pp. 1–23.Google Scholar
[29] Rosner, R., Modular synthesis of reactive systems, Ph.D. thesis , Weizmann Institute of Science, Rehovot, Israel, 1992.Google Scholar
[30] Thatcher, J.W., Tree automata: an informal survey, Currents in the theory of computing (Aho, A. V., editor), Prentice-Hall, Englewood Cliffs, 1973, pp. 143–172.Google Scholar
[31] Vardi, M. Y., An automata-theoretic approach to fair realizability and synthesis, Computer aided verification, Proceedings of the 7th international conference (Wolper, P., editor), Lecture Notes in Computer Science, no. 939, Springer-Verlag, Berlin, 1995, pp. 267–292.Google Scholar
[32] Vardi, M. Y. and Stockmeyer, L., Improved upper and lower bounds formodal logics of programs, Proceedings of the 17th acm symposium on theory of computing, 1985, pp. 240–251.Google Scholar
[33] Vardi, M. Y. and Wolper, P., Automata-theoretic techniques for modal logics of programs, Journal of Computer and System Science, vol. 32 (1986), no. 2, pp. 182–221.Google Scholar