{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,5]],"date-time":"2026-03-05T23:51:59Z","timestamp":1772754719314,"version":"3.50.1"},"reference-count":33,"publisher":"Cambridge University Press (CUP)","issue":"2","license":[{"start":{"date-parts":[[2014,1,15]],"date-time":"2014-01-15T00:00:00Z","timestamp":1389744000000},"content-version":"unspecified","delay-in-days":5342,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Bull. symb. log."],"published-print":{"date-parts":[[1999,6]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>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.<\/jats:p><jats:p>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 <jats:italic>synthesis with incomplete information<\/jats:italic>. 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 <jats:italic>alternation<\/jats:italic> is a suitable and helpful mechanism for coping with incomplete information. Using <jats:italic>alternating tree automata<\/jats:italic>, 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.<\/jats:p>","DOI":"10.2307\/421091","type":"journal-article","created":{"date-parts":[[2006,5,7]],"date-time":"2006-05-07T07:12:41Z","timestamp":1146985961000},"page":"245-263","source":"Crossref","is-referenced-by-count":49,"title":["Church's Problem Revisited"],"prefix":"10.1017","volume":"5","author":[{"given":"Orna","family":"Kupferman","sequence":"first","affiliation":[]},{"given":"Moshe Y.","family":"Vardi","sequence":"additional","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2014,1,15]]},"reference":[{"key":"S1079898600007034_ref021","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(87)90133-2"},{"key":"S1079898600007034_ref002","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-58179-0_50"},{"key":"S1079898600007034_ref009","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(85)90001-7"},{"key":"S1079898600007034_ref032","first-page":"240","volume-title":"Proceedings of the 17th acm symposium on theory of computing","author":"Vardi","year":"1985"},{"key":"S1079898600007034_ref007","first-page":"997","volume-title":"Handbook of theoretical computer science","author":"Emerson","year":"1990"},{"key":"S1079898600007034_ref029","unstructured":"Rosner R. , Modular synthesis of reactive systems, Ph.D. thesis , Weizmann Institute of Science, Rehovot, Israel, 1992."},{"key":"S1079898600007034_ref030","first-page":"143","volume-title":"Currents in the theory of computing","author":"Thatcher","year":"1973"},{"key":"S1079898600007034_ref004","first-page":"23","volume-title":"Proceedings of the international congress of mathematicians, 1962","author":"Church","year":"1963"},{"key":"S1079898600007034_ref010","doi-asserted-by":"publisher","DOI":"10.1145\/4904.4999"},{"key":"S1079898600007034_ref003","doi-asserted-by":"publisher","DOI":"10.1090\/S0002-9947-1969-0280205-0"},{"key":"S1079898600007034_ref031","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-60045-0_56"},{"key":"S1079898600007034_ref023","first-page":"46","volume-title":"Proceedings of the 18th IEEE symposium on foundation of computer science","author":"Pnueli","year":"1977"},{"key":"S1079898600007034_ref027","first-page":"746","volume-title":"Proceedings of the 31st IEEE symposium on foundation of computer science","author":"Pnueli","year":"1990"},{"key":"S1079898600007034_ref020","doi-asserted-by":"publisher","DOI":"10.1145\/357084.357090"},{"key":"S1079898600007034_ref014","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4615-2217-1"},{"key":"S1079898600007034_ref015","volume-title":"Siam journal of control and optimization","author":"Kumar","year":"1995"},{"key":"S1079898600007034_ref018","first-page":"91","volume-title":"2nd international conference on temporal logic","author":"Kupferman","year":"1997"},{"key":"S1079898600007034_ref028","first-page":"1","volume-title":"Proceedings of symposia in mathematics, logic and foundations of set theory","author":"Rabin","year":"1970"},{"key":"S1079898600007034_ref026","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0035790"},{"key":"S1079898600007034_ref033","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(86)90026-7"},{"key":"S1079898600007034_ref012","first-page":"1105","volume":"48","author":"Gurevich","year":"1983","journal-title":"Rabin's uniformization problem"},{"key":"S1079898600007034_ref016","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-61474-5_59"},{"key":"S1079898600007034_ref019","first-page":"174","volume-title":"Proceedings of the 7th ACM symposium on principles of programming languages","author":"Lamport","year":"1980"},{"key":"S1079898600007034_ref022","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)00214-4"},{"key":"S1079898600007034_ref025","volume-title":"Proceedings of the 16th ACM symposium on principles of programming languages","author":"Pnueli","year":"1989"},{"key":"S1079898600007034_ref005","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/6874.001.0001","volume-title":"Trace theory for automatic hierarchical verification of speed independent circuits","author":"Dill","year":"1989"},{"key":"S1079898600007034_ref011","first-page":"368","volume-title":"Proceedings of the 29th IEEE symposium on foundations of computer science","author":"Emerson","year":"1988"},{"key":"S1079898600007034_ref017","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-63166-6_7"},{"key":"S1079898600007034_ref001","first-page":"1","volume-title":"Proceedings of the 16th international colloquium on automata, languages and programming","author":"Abadi","year":"1989"},{"key":"S1079898600007034_ref013","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-82453-1_17"},{"key":"S1079898600007034_ref024","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(81)90110-9"},{"key":"S1079898600007034_ref008","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(83)90017-5"},{"key":"S1079898600007034_ref006","doi-asserted-by":"publisher","DOI":"10.1016\/S0019-9958(84)80047-9"}],"container-title":["Bulletin of Symbolic Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S1079898600007034","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,9]],"date-time":"2019-05-09T21:13:34Z","timestamp":1557436414000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S1079898600007034\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999,6]]},"references-count":33,"journal-issue":{"issue":"2","published-print":{"date-parts":[[1999,6]]}},"alternative-id":["S1079898600007034"],"URL":"https:\/\/doi.org\/10.2307\/421091","relation":{},"ISSN":["1079-8986","1943-5894"],"issn-type":[{"value":"1079-8986","type":"print"},{"value":"1943-5894","type":"electronic"}],"subject":[],"published":{"date-parts":[[1999,6]]}}}