{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,1]],"date-time":"2025-10-01T16:25:01Z","timestamp":1759335901549,"version":"3.40.3"},"publisher-location":"Cham","reference-count":32,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031572272"},{"type":"electronic","value":"9783031572289"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,4,5]],"date-time":"2024-04-05T00:00:00Z","timestamp":1712275200000},"content-version":"vor","delay-in-days":95,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"abstract":"Abstract<\/jats:title>We study automaticsynthesis<\/jats:italic>of systems that interact with their environment and maintainprivacy<\/jats:italic>against an observer to the interaction. The system and the environment interact via setsI<\/jats:italic>andO<\/jats:italic>of input and output signals. The input to the synthesis problem contains, in addition to a specification, also a list ofsecrets<\/jats:italic>, a function$$\\textsf{cost}: I \\cup O \\rightarrow {\\mathbb N}$$<\/jats:tex-math>cost<\/mml:mi>:<\/mml:mo>I<\/mml:mi>\u222a<\/mml:mo>O<\/mml:mi>\u2192<\/mml:mo>N<\/mml:mi><\/mml:mrow><\/mml:math><\/jats:alternatives><\/jats:inline-formula>, which maps each signal to the cost of hiding it, and a bound$$b \\in {\\mathbb N}$$<\/jats:tex-math>b<\/mml:mi>\u2208<\/mml:mo>N<\/mml:mi><\/mml:mrow><\/mml:math><\/jats:alternatives><\/jats:inline-formula>on the budget that the system may use for hiding of signals. The desired output is an (I<\/jats:italic>\/O<\/jats:italic>)-transducer$$\\mathcal {T}$$<\/jats:tex-math>T<\/mml:mi><\/mml:math><\/jats:alternatives><\/jats:inline-formula>and a set$$\\mathcal {H} \\subseteq I \\cup O$$<\/jats:tex-math>H<\/mml:mi>\u2286<\/mml:mo>I<\/mml:mi>\u222a<\/mml:mo>O<\/mml:mi><\/mml:mrow><\/mml:math><\/jats:alternatives><\/jats:inline-formula>of signals that respects the bound on the budget, thus$$\\sum _{s \\in \\mathcal {H}} \\textsf{cost}(s) \\le b$$<\/jats:tex-math>\u2211<\/mml:mo>s<\/mml:mi>\u2208<\/mml:mo>H<\/mml:mi><\/mml:mrow><\/mml:msub>cost<\/mml:mi>(<\/mml:mo>s<\/mml:mi>)<\/mml:mo><\/mml:mrow>\u2264<\/mml:mo>b<\/mml:mi><\/mml:mrow><\/mml:math><\/jats:alternatives><\/jats:inline-formula>, such that for every possible interaction of$$\\mathcal {T}$$<\/jats:tex-math>T<\/mml:mi><\/mml:math><\/jats:alternatives><\/jats:inline-formula>, the generated computation satisfies the specification, yet an observer from which the signals in$$\\mathcal {H}$$<\/jats:tex-math>H<\/mml:mi><\/mml:math><\/jats:alternatives><\/jats:inline-formula>are hidden, cannot evaluate the secrets.<\/jats:p>We first show that the complexity of the problem is 2EXPTIME-complete for specifications and secrets in LTL, thus it is not harder than synthesis with no privacy requirements. We then analyze the complexity of the problem more carefully, isolating the two aspects that do not exist in traditional synthesis, namely the need to hide the value of the secrets and the need to choose the set$$\\mathcal {H}$$<\/jats:tex-math>H<\/mml:mi><\/mml:math><\/jats:alternatives><\/jats:inline-formula>. We do this by studying settings in which traditional synthesis can be solved in polynomial time \u2013 when the specification formalism is deterministic automata and when the system is closed, and show that each of the two aspects involves an exponential blow-up in the complexity. We continue and studybounded synthesis with privacy<\/jats:italic>, where the input also includes a bound on the size of the synthesized transducer, as well as a variant of the problem in which the observer hasknowledge about the specification<\/jats:italic>, which can be helpful in evaluating the secrets. We study the effect of both variants on the different aspects of the problem and provide algorithms with a tight complexity.<\/jats:p>","DOI":"10.1007\/978-3-031-57228-9_13","type":"book-chapter","created":{"date-parts":[[2024,4,4]],"date-time":"2024-04-04T08:03:04Z","timestamp":1712217784000},"page":"256-277","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Synthesis with Privacy Against an Observer"],"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":[]},{"ORCID":"https:\/\/orcid.org\/0009-0009-4736-6708","authenticated-orcid":false,"given":"Naama","family":"Shamash Halevy","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,4,5]]},"reference":[{"key":"13_CR1","doi-asserted-by":"crossref","unstructured":"B.\u00a0Barak, O.\u00a0Goldreich, R.\u00a0Impagliazzo, S.\u00a0Rudich, A.\u00a0Sahai, S.P. Vadhan, and K.\u00a0Yang. On the (im)possibility of obfuscating programs. J. ACM, 59(2):6:1\u20136:48, 2012.","DOI":"10.1145\/2160158.2160159"},{"key":"13_CR2","doi-asserted-by":"crossref","unstructured":"R.\u00a0Bloem, K.\u00a0Chatterjee, and B.\u00a0Jobstmann. Graph games and reactive synthesis. In Handbook of Model Checking., pages 921\u2013962. Springer, 2018.","DOI":"10.1007\/978-3-319-10575-8_27"},{"key":"13_CR3","doi-asserted-by":"crossref","unstructured":"A.\u00a0Bohy, V.\u00a0Bruy\u00e8re, E.\u00a0Filiot, and J-F. Raskin. Synthesis from LTL specifications with mean-payoff objectives. In Proc. 19th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems, volume 7795 of Lecture Notes in Computer Science, pages 169\u2013184. Springer, 2013.","DOI":"10.1007\/978-3-642-36742-7_12"},{"key":"13_CR4","doi-asserted-by":"crossref","unstructured":"U.\u00a0Boker. Why these automata types? In Proc. 22nd Int. Conf. on Logic for Programming Artificial Intelligence and Reasoning, volume\u00a057 of EPiC Series in Computing, pages 143\u2013163, 2018.","DOI":"10.29007\/c3bj"},{"key":"13_CR5","doi-asserted-by":"crossref","unstructured":"C.S. Calude, S.\u00a0Jain, B.\u00a0Khoussainov, W.\u00a0Li, and F.\u00a0Stephan. Deciding parity games in quasipolynomial time. In Proc. 49th ACM Symp. on Theory of Computing, pages 252\u2013263, 2017.","DOI":"10.1145\/3055399.3055409"},{"key":"13_CR6","doi-asserted-by":"crossref","unstructured":"K.\u00a0Chatterjee and L.\u00a0Doyen. Energy parity games. In Proc. 37th Int. Colloq. on Automata, Languages, and Programming, pages 599\u2013610, 2010.","DOI":"10.1007\/978-3-642-14162-1_50"},{"key":"13_CR7","doi-asserted-by":"crossref","unstructured":"K.\u00a0Chatterjee, L.\u00a0Doyen, T.\u00a0A. Henzinger, and J-F. Raskin. Algorithms for $$\\omega $$-regular games with imperfect information. In Proc. 15th Annual Conf. of the European Association for Computer Science Logic, volume 4207 of Lecture Notes in Computer Science, pages 287\u2013302, 2006.","DOI":"10.1007\/11874683_19"},{"key":"13_CR8","doi-asserted-by":"crossref","unstructured":"M.R. Clarkson, B.\u00a0Finkbeiner, M.\u00a0Koleini, K.K. Micinski, M.N. Rabe, and C.\u00a0S\u00e1nchez. Temporal logics for hyperproperties. In 3rd International Conference on Principles of Security and Trust, volume 8414 of Lecture Notes in Computer Science, pages 265\u2013284. Springer, 2014.","DOI":"10.1007\/978-3-642-54792-8_15"},{"key":"13_CR9","doi-asserted-by":"crossref","unstructured":"I.\u00a0Dinur and K.\u00a0Nissim. Revealing information while preserving privacy. In Proceedings of the 22nd ACM Symposium on Principles of Database Systems, pages 202\u2013210. ACM, 2003.","DOI":"10.1145\/773153.773173"},{"key":"13_CR10","doi-asserted-by":"crossref","unstructured":"J.\u00a0Dubreil, Ph. Darondeau, and H.\u00a0Marchand. Supervisory control for opacity. IEEE Transactions on Automatic Control, 55(5):1089\u20131100, 2010.","DOI":"10.1109\/TAC.2010.2042008"},{"key":"13_CR11","doi-asserted-by":"crossref","unstructured":"C.\u00a0Dwork, F.\u00a0McSherry, K.\u00a0Nissim, and A.D. Smith. Calibrating noise to sensitivity in private data analysis. J. Priv. Confidentiality, 7(3):17\u201351, 2016.","DOI":"10.29012\/jpc.v7i3.405"},{"key":"13_CR12","doi-asserted-by":"crossref","unstructured":"R.\u00a0Ehlers. Symbolic bounded synthesis. In Proc. 22nd Int. Conf. on Computer Aided Verification, volume 6174 of Lecture Notes in Computer Science, pages 365\u2013379. Springer, 2010.","DOI":"10.1007\/978-3-642-14295-6_33"},{"key":"13_CR13","doi-asserted-by":"crossref","unstructured":"B.\u00a0Finkbeiner, C.\u00a0Hahn, P.\u00a0Lukert, M.\u00a0Stenger, and L.\u00a0Tentrup. Synthesis from hyperproperties. Acta Informatica, 57(1-2):137\u2013163, 2020.","DOI":"10.1007\/s00236-019-00358-2"},{"key":"13_CR14","doi-asserted-by":"crossref","unstructured":"D.\u00a0Fisman, O.\u00a0Kupferman, S.\u00a0Sheinvald, and M.Y. Vardi. A framework for inherent vacuity. In 4th International Haifa Verification Conference, volume 5394 of Lecture Notes in Computer Science, pages 7\u201322. Springer, 2008.","DOI":"10.1007\/978-3-642-01702-5_7"},{"key":"13_CR15","doi-asserted-by":"crossref","unstructured":"S.\u00a0Garg, C.\u00a0Gentry, S.\u00a0Halevi, M.\u00a0Raykova, A.\u00a0Sahai, and B.\u00a0Waters. Candidate indistinguishability obfuscation and functional encryption for all circuits. SIAM J. Comput., 45(3):882\u2013929, 2016.","DOI":"10.1137\/14095772X"},{"key":"13_CR16","doi-asserted-by":"crossref","unstructured":"K.\u00a0Greimel, R.\u00a0Bloem, B.\u00a0Jobstmann, and M.\u00a0Vardi. Open implication. In Proc. 35th Int. Colloq. on Automata, Languages, and Programming, volume 5126 of Lecture Notes in Computer Science, pages 361\u2013372. Springer, 2008.","DOI":"10.1007\/978-3-540-70583-3_30"},{"key":"13_CR17","doi-asserted-by":"crossref","unstructured":"T.A. Henzinger, S.C. Krishnan, O.\u00a0Kupferman, and F.Y.C. Mang. Synthesis of uninitialized systems.In Proc. 29th Int. Colloq. on Automata, Languages, and Programming, volume 2380 of Lecture Notes in Computer Science, pages 644\u2013656. Springer, 2002.","DOI":"10.1007\/3-540-45465-9_55"},{"key":"13_CR18","unstructured":"O.\u00a0Kupferman and O.\u00a0Leshkowitz. Synthesis of privacy-preserving systems. In Proc. 42nd Conf. on Foundations of Software Technology and Theoretical Computer Science, volume 250 of Leibniz International Proceedings in Informatics (LIPIcs), pages 42:1\u201342:23, 2022."},{"key":"13_CR19","unstructured":"O.\u00a0Kupferman, Y.\u00a0Lustig, M.Y. Vardi, and M.\u00a0Yannakakis. Temporal synthesis for bounded systems and environments. In Proc. 28th Symp. on Theoretical Aspects of Computer Science, pages 615\u2013626, 2011."},{"key":"13_CR20","doi-asserted-by":"crossref","unstructured":"O.\u00a0Kupferman and A.\u00a0Rosenberg. The blow-up in translating LTL to deterministic automata. In Proc. 6th Workshop on Model Checking and Artificial Intelligence, volume 6572 of Lecture Notes in Artificial Intelligence, pages 85\u201394. Springer, 2010.","DOI":"10.1007\/978-3-642-20674-0_6"},{"key":"13_CR21","doi-asserted-by":"crossref","unstructured":"O.\u00a0Kupferman and M.Y. Vardi. Synthesis with incomplete information. In Advances in Temporal Logic, pages 109\u2013127. Kluwer Academic Publishers, 2000.","DOI":"10.1007\/978-94-015-9586-5_6"},{"key":"13_CR22","doi-asserted-by":"crossref","unstructured":"O.\u00a0Kupferman and M.Y. Vardi. From linear time to branching time. ACM Transactions on Computational Logic, 6(2):273\u2013294, 2005.","DOI":"10.1145\/1055686.1055689"},{"key":"13_CR23","doi-asserted-by":"crossref","unstructured":"N.\u00a0Piterman. From nondeterministic B\u00fcchi and Streett automata to deterministic parity automata. In Proc. 21st IEEE Symp. on Logic in Computer Science, pages 255\u2013264. IEEE press, 2006.","DOI":"10.1109\/LICS.2006.28"},{"key":"13_CR24","doi-asserted-by":"crossref","unstructured":"A.\u00a0Pnueli. The temporal semantics of concurrent programs. Theoretical Computer Science, 13:45\u201360, 1981.","DOI":"10.1016\/0304-3975(81)90110-9"},{"key":"13_CR25","doi-asserted-by":"crossref","unstructured":"A.\u00a0Pnueli and R.\u00a0Rosner. On the synthesis of a reactive module. In Proc. 16th ACM Symp. on Principles of Programming Languages, pages 179\u2013190, 1989.","DOI":"10.1145\/75277.75293"},{"key":"13_CR26","doi-asserted-by":"crossref","unstructured":"M.O. Rabin. Automata on infinite objects and Church\u2019s problem. Amer. Mathematical Society, 1972.","DOI":"10.1090\/cbms\/013"},{"key":"13_CR27","doi-asserted-by":"crossref","unstructured":"J.H. Reif. 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":"13_CR28","unstructured":"R.\u00a0Rosner. Modular Synthesis of Reactive Systems. PhD thesis, Weizmann Institute of Science, 1992."},{"key":"13_CR29","doi-asserted-by":"crossref","unstructured":"S.\u00a0Safra. On the complexity of $$\\omega $$-automata. In Proc. 29th IEEE Symp. on Foundations of Computer Science, pages 319\u2013327, 1988.","DOI":"10.1109\/SFCS.1988.21948"},{"key":"13_CR30","doi-asserted-by":"crossref","unstructured":"S.\u00a0Schewe and B.\u00a0Finkbeiner. Bounded synthesis. In 5th Int. Symp. on Automated Technology for Verification and Analysis, volume 4762 of Lecture Notes in Computer Science, pages 474\u2013488. Springer, 2007.","DOI":"10.1007\/978-3-540-75596-8_33"},{"key":"13_CR31","doi-asserted-by":"crossref","unstructured":"M.Y. Vardi and P.\u00a0Wolper. Reasoning about infinite computations. Information and Computation, 115(1):1\u201337, 1994.","DOI":"10.1006\/inco.1994.1092"},{"key":"13_CR32","doi-asserted-by":"crossref","unstructured":"Y.\u00a0Wu, V.\u00a0Raman, B.C. Rawlings, S.\u00a0Lafortune, and S.A. Seshia. 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","Foundations of Software Science and Computation Structures"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-57228-9_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,11,15]],"date-time":"2024-11-15T17:20:59Z","timestamp":1731691259000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-57228-9_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031572272","9783031572289"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-57228-9_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"5 April 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FoSSaCS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Foundations of Software Science and Computation Structures","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg City","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 April 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 April 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fossacs2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2024\/conferences\/fossacs\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"79","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"24","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"30% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"9","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}