{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,29]],"date-time":"2025-11-29T07:41:03Z","timestamp":1764402063662,"version":"3.46.0"},"publisher-location":"Cham","reference-count":31,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031906527"},{"type":"electronic","value":"9783031906534"}],"license":[{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,5,1]],"date-time":"2025-05-01T00:00:00Z","timestamp":1746057600000},"content-version":"vor","delay-in-days":120,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    In the synthesis problem, we are given a specification, and we automatically generate a system that satisfies the specification in all environments. We introduce and study\n                    <jats:italic>synthesis with guided environments<\/jats:italic>\n                    (SGE, for short), where the system may harness the knowledge and computational power of the environment during the interaction. The underlying idea in SGE is that in many settings, in particular when the system serves or directs the environment, it is of the environment\u2019s interest that the specification is satisfied, and it would follow the guidance of the system. Thus, while the environment is\u00a0still hostile, in the sense that the system should satisfy the specification no matter how the environment assigns values to the input signals, in SGE the system assigns values to some output signals and guides the environment via\n                    <jats:italic>programs<\/jats:italic>\n                    how to assign values to other output signals. A key issue is that these assignments may depend on input signals that are hidden from the system but are known to the environment, using programs like \u201ccopy the value of the hidden input signal\n                    <jats:italic>x<\/jats:italic>\n                    to the output signal\n                    <jats:italic>y<\/jats:italic>\n                    .\u201d SGE is thus particularly useful in settings where the system has partial visibility.\n                  <\/jats:p>\n                  <jats:p>We solve the problem of SGE, show its superiority with respect to traditional synthesis, and study theoretical aspects of SGE, like the complexity (memory and domain) of programs used by the system, as well as the connection of SGE to synthesis of (possibly distributed) systems with partial visibility.<\/jats:p>","DOI":"10.1007\/978-3-031-90653-4_10","type":"book-chapter","created":{"date-parts":[[2025,5,2]],"date-time":"2025-05-02T07:43:53Z","timestamp":1746171833000},"page":"198-216","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Synthesis with Guided Environments"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-4699-6117","authenticated-orcid":false,"given":"Orna","family":"Kupferman","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9225-2325","authenticated-orcid":false,"given":"Ofer","family":"Leshkowitz","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,5,1]]},"reference":[{"key":"10_CR1","doi-asserted-by":"crossref","unstructured":"Akshay, S., Basa, E., Chakraborty, S., Fried, D.: On dependent variables in reactive synthesis. In: Proc. 30th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems. pp. 123\u2013143. Springer Nature Switzerland (2024)","DOI":"10.1007\/978-3-031-57246-3_8"},{"key":"10_CR2","doi-asserted-by":"crossref","unstructured":"Almagor, S., Kuperberg, D., Kupferman, O.: Sensing as a complexity measure. Int. J. Found. Comput. Sci. 30(6-7), 831\u2013873 (2019)","DOI":"10.1142\/S0129054119400203"},{"key":"10_CR3","doi-asserted-by":"crossref","unstructured":"Alur, R., Henzinger, T., Kupferman, O.: Alternating-time temporal logic. Journal of the ACM 49(5), 672\u2013713 (2002)","DOI":"10.1145\/585265.585270"},{"key":"10_CR4","doi-asserted-by":"crossref","unstructured":"Berthon, R., Maubert, B., Murano, A., Rubin, S., Vardi, M.: Strategy logic with imperfect information. In: Proc. 32nd ACM\/IEEE Symp. on Logic in Computer Science. pp. 1\u201312 (2017)","DOI":"10.1109\/LICS.2017.8005136"},{"key":"10_CR5","doi-asserted-by":"crossref","unstructured":"Bloem, R., Chatterjee, K., Jobstmann, B.: Graph games and reactive synthesis. In: Handbook of Model Checking., pp. 921\u2013962. Springer (2018)","DOI":"10.1007\/978-3-319-10575-8_27"},{"key":"10_CR6","doi-asserted-by":"crossref","unstructured":"Bouyer, P., Markey, N., Vester, S.: Nash equilibria in symmetric graph games with partial observation. Information and Computation 254, 238\u2013258 (2017)","DOI":"10.1016\/j.ic.2016.10.010"},{"key":"10_CR7","doi-asserted-by":"crossref","unstructured":"Chatterjee, K., Doyen, L., Henzinger, T., Raskin, J.F.: Algorithms for omega-regular games with imperfect information. Logical Methods in Computer Science 3(3) (2007)","DOI":"10.2168\/LMCS-3(3:4)2007"},{"key":"10_CR8","doi-asserted-by":"crossref","unstructured":"Chatterjee, K., Doyen, L., Nain, S., Vardi, M.: The complexity of partial-observation stochastic parity games with finite-memory strategies. In: Proc. 17th Int. Conf. on Foundations of Software Science and Computation Structures. Lecture Notes in Computer Science, vol.\u00a08412, pp. 242\u2013257. Springer (2014)","DOI":"10.1007\/978-3-642-54830-7_16"},{"key":"10_CR9","doi-asserted-by":"crossref","unstructured":"Chatterjee, K., Majumdar, R., Henzinger, T.A.: Controller synthesis with budget constraints. In: Proc 11th International Workshop on Hybrid Systems: Computation and Control. Lecture Notes in Computer Science, vol.\u00a04981, pp. 72\u201386. Springer (2008)","DOI":"10.1007\/978-3-540-78929-1_6"},{"key":"10_CR10","unstructured":"De Giacomo, G., Vardi, M.Y.: Ltl$$_f$$ and ldl$$_f$$ synthesis under partial observability. In: Proc.\u00a025th Int\u2019l Joint Conf.\u00a0on Artificial Intelligence. pp. 1044\u20131050. IJCAI\/AAAI Press (2016)"},{"key":"10_CR11","doi-asserted-by":"crossref","unstructured":"Ehlers, R.: Symbolic bounded synthesis. In: Proc. 22nd Int. Conf. on Computer Aided Verification. Lecture Notes in Computer Science, vol.\u00a06174, pp. 365\u2013379. Springer (2010)","DOI":"10.1007\/978-3-642-14295-6_33"},{"key":"10_CR12","doi-asserted-by":"crossref","unstructured":"Esparza, J., Kret\u00ednsk\u00fd, J., Sickert, S.: A unified translation of linear temporal logic to $$\\omega $$-automata. J. ACM 67(6), 33:1\u201333:61 (2020)","DOI":"10.1145\/3417995"},{"key":"10_CR13","doi-asserted-by":"crossref","unstructured":"Filiot, E., Gentilini, R., Raskin, J.F.: Rational synthesis under imperfect information. In: Proc. 33rd ACM\/IEEE Symp. on Logic in Computer Science. pp. 422\u2013431. ACM (2018)","DOI":"10.1145\/3209108.3209164"},{"key":"10_CR14","doi-asserted-by":"crossref","unstructured":"Finkbeiner, B., Metzger, N., Moses, Y.: Information flow guided synthesis with\u0103 unbounded communication. In: Proc. 36th Int. Conf. on Computer Aided Verification. pp. 64\u201386. Springer Nature Switzerland (2024)","DOI":"10.1007\/978-3-031-65633-0_4"},{"key":"10_CR15","doi-asserted-by":"crossref","unstructured":"Gutierrez, J., Perelli, G., Wooldridge, M.J.: Imperfect information in reactive modules games. Inf. Comput. 261, 650\u2013675 (2018)","DOI":"10.1016\/j.ic.2018.02.023"},{"key":"10_CR16","doi-asserted-by":"crossref","unstructured":"Krausz, A., Rieder, U.: Markov games with incomplete information. Mathematical Methods of Operations Research 46, 263\u2013279 (1997)","DOI":"10.1007\/BF01217695"},{"key":"10_CR17","doi-asserted-by":"crossref","unstructured":"Kumar, R., Shayman, M.: Formulae relating controllability, observability, and co-observability. Autom. 34(2), 211\u2013215 (1998)","DOI":"10.1016\/S0005-1098(97)00164-7"},{"key":"10_CR18","unstructured":"Kupferman, O., Leshkowitz, O.: Synthesis of privacy-preserving systems. In: Proc. 42nd Conf. on Foundations of Software Technology and Theoretical Computer Science. Leibniz International Proceedings in Informatics (LIPIcs), vol.\u00a0250, pp. 42:1\u201342:23 (2022)"},{"key":"10_CR19","unstructured":"Kupferman, O., Lustig, Y., Vardi, M., Yannakakis, M.: Temporal synthesis for bounded systems and environments. In: Proc. 28th Symp. on Theoretical Aspects of Computer Science. pp. 615\u2013626 (2011)"},{"key":"10_CR20","doi-asserted-by":"crossref","unstructured":"Kupferman, O., Vardi, M.: Synthesis with incomplete information. In: Advances in Temporal Logic. pp. 109\u2013127. Kluwer Academic Publishers (2000)","DOI":"10.1007\/978-94-015-9586-5_6"},{"key":"10_CR21","doi-asserted-by":"crossref","unstructured":"Kupferman, O., Vardi, M.: Synthesizing distributed systems. In: Proc. 16th ACM\/IEEE Symp. on Logic in Computer Science. pp. 389\u2013398 (2001)","DOI":"10.1109\/LICS.2001.932514"},{"key":"10_CR22","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal semantics of concurrent programs. Theoretical Computer Science 13, 45\u201360 (1981)","DOI":"10.1016\/0304-3975(81)90110-9"},{"key":"10_CR23","doi-asserted-by":"crossref","unstructured":"Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: Proc. 16th ACM Symp. on Principles of Programming Languages. pp. 179\u2013190 (1989)","DOI":"10.1145\/75277.75293"},{"key":"10_CR24","doi-asserted-by":"crossref","unstructured":"Pnueli, A., Rosner, R.: Distributed reactive systems are hard to synthesize. In: Proc. 31st IEEE Symp. on Foundations of Computer Science. pp. 746\u2013757 (1990)","DOI":"10.1109\/FSCS.1990.89597"},{"key":"10_CR25","doi-asserted-by":"crossref","unstructured":"Reif, J.: The complexity of two-player games of incomplete information. Journal of Computer and Systems Science 29, 274\u2013301 (1984)","DOI":"10.1016\/0022-0000(84)90034-5"},{"key":"10_CR26","unstructured":"Rosner, R.: Modular Synthesis of Reactive Systems. Ph.D. thesis, Weizmann Institute of Science (1992)"},{"key":"10_CR27","doi-asserted-by":"crossref","unstructured":"Safra, S.: On the complexity of $$\\omega $$-automata. In: Proc. 29th IEEE Symp. on Foundations of Computer Science. pp. 319\u2013327 (1988)","DOI":"10.1109\/SFCS.1988.21948"},{"key":"10_CR28","unstructured":"Schewe, S.: Synthesis of distributed systems. Ph.D. thesis, Saarland University, Saarbr\u00fccken, Germany (2008)"},{"key":"10_CR29","doi-asserted-by":"crossref","unstructured":"Schewe, S., Finkbeiner, B.: Bounded synthesis. In: 5th Int. Symp. on Automated Technology for Verification and Analysis. Lecture Notes in Computer Science, vol.\u00a04762, pp. 474\u2013488. Springer (2007)","DOI":"10.1007\/978-3-540-75596-8_33"},{"key":"10_CR30","doi-asserted-by":"crossref","unstructured":"Vardi, M., Wolper, P.: Reasoning about infinite computations. Information and Computation 115(1), 1\u201337 (1994)","DOI":"10.1006\/inco.1994.1092"},{"key":"10_CR31","doi-asserted-by":"crossref","unstructured":"Wu, Y., Raman, V., Rawlings, B., Lafortune, S., Seshia, S.: Synthesis of obfuscation policies to ensure privacy and utility. Journal of Automated Reasoning 60(1), 107\u2013131 (2018)","DOI":"10.1007\/s10817-017-9420-x"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-90653-4_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,11,29]],"date-time":"2025-11-29T07:36:32Z","timestamp":1764401792000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-90653-4_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031906527","9783031906534"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-90653-4_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"1 May 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TACAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Hamilton, ON","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Canada","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"3 May 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"8 May 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"31","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2025\/conferences\/tacas\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}