{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,1]],"date-time":"2026-06-01T18:29:07Z","timestamp":1780338547571,"version":"3.54.1"},"reference-count":43,"publisher":"Springer Science and Business Media LLC","issue":"1-2","license":[{"start":{"date-parts":[[2019,12,7]],"date-time":"2019-12-07T00:00:00Z","timestamp":1575676800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2019,12,7]],"date-time":"2019-12-07T00:00:00Z","timestamp":1575676800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","award":["683300"],"award-info":[{"award-number":["683300"]}],"id":[{"id":"10.13039\/501100000781","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001659","name":"Deutsche Forschungsgemeinschaft","doi-asserted-by":"publisher","award":["TRR 248, 389792660"],"award-info":[{"award-number":["TRR 248, 389792660"]}],"id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001659","name":"Deutsche Forschungsgemeinschaft","doi-asserted-by":"publisher","award":["SFB 1223"],"award-info":[{"award-number":["SFB 1223"]}],"id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Acta Informatica"],"published-print":{"date-parts":[[2020,4]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We study the reactive synthesis problem for hyperproperties given as formulas of the temporal logic HyperLTL. Hyperproperties generalize trace properties, i.e., sets of traces, to <jats:italic>sets of sets<\/jats:italic> of traces. Typical examples are information-flow policies like noninterference, which stipulate that no sensitive data must leak into the public domain. Such properties cannot be expressed in standard linear or branching-time temporal logics like LTL, CTL, or <jats:inline-formula><jats:alternatives><jats:tex-math>$$\\hbox {CTL}^*$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\"><mml:msup><mml:mtext>CTL<\/mml:mtext><mml:mo>\u2217<\/mml:mo><\/mml:msup><\/mml:math><\/jats:alternatives><\/jats:inline-formula>. Furthermore, HyperLTL subsumes many classical extensions of the LTL realizability problem, including realizability under incomplete information, distributed synthesis, and fault-tolerant synthesis. We show that, while the synthesis problem is undecidable for full HyperLTL, it remains decidable for the <jats:inline-formula><jats:alternatives><jats:tex-math>$$\\exists ^*$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\"><mml:msup><mml:mo>\u2203<\/mml:mo><mml:mo>\u2217<\/mml:mo><\/mml:msup><\/mml:math><\/jats:alternatives><\/jats:inline-formula>, <jats:inline-formula><jats:alternatives><jats:tex-math>$$\\exists ^*\\forall ^1$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\"><mml:mrow><mml:msup><mml:mo>\u2203<\/mml:mo><mml:mo>\u2217<\/mml:mo><\/mml:msup><mml:msup><mml:mo>\u2200<\/mml:mo><mml:mn>1<\/mml:mn><\/mml:msup><\/mml:mrow><\/mml:math><\/jats:alternatives><\/jats:inline-formula>, and the <jats:inline-formula><jats:alternatives><jats:tex-math>$${{ linear }}\\;\\forall ^*$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\"><mml:mrow><mml:mrow><mml:mi>linear<\/mml:mi><\/mml:mrow><mml:mspace\/><mml:msup><mml:mo>\u2200<\/mml:mo><mml:mo>\u2217<\/mml:mo><\/mml:msup><\/mml:mrow><\/mml:math><\/jats:alternatives><\/jats:inline-formula> fragments. Beyond these fragments, the synthesis problem immediately becomes undecidable. For universal HyperLTL, we present a semi-decision procedure that constructs implementations and counterexamples up to a given bound. We report encouraging experimental results obtained with a prototype implementation on example specifications with hyperproperties like symmetric responses, secrecy, and information flow.\n<\/jats:p>","DOI":"10.1007\/s00236-019-00358-2","type":"journal-article","created":{"date-parts":[[2019,12,7]],"date-time":"2019-12-07T16:02:37Z","timestamp":1575734557000},"page":"137-163","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":19,"title":["Synthesis from hyperproperties"],"prefix":"10.1007","volume":"57","author":[{"given":"Bernd","family":"Finkbeiner","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Christopher","family":"Hahn","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Philip","family":"Lukert","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Marvin","family":"Stenger","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6150-2982","authenticated-orcid":false,"given":"Leander","family":"Tentrup","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2019,12,7]]},"reference":[{"key":"358_CR1","doi-asserted-by":"publisher","unstructured":"Agrawal, S., Bonakdarpour, B.: Runtime verification of k-safety hyperproperties in HyperLTL. In: Proceedings of CSF, pp. 239\u2013252. IEEE Computer Society (2016). https:\/\/doi.org\/10.1109\/CSF.2016.24","DOI":"10.1109\/CSF.2016.24"},{"key":"358_CR2","doi-asserted-by":"publisher","unstructured":"Bonakdarpour, B., Finkbeiner, B.: The complexity of monitoring hyperproperties. In: Proceedings of CSF, pp. 162\u2013174. IEEE Computer Society (2018). https:\/\/doi.org\/10.1109\/CSF.2018.00019","DOI":"10.1109\/CSF.2018.00019"},{"key":"358_CR3","doi-asserted-by":"publisher","first-page":"8","DOI":"10.1007\/978-3-030-03421-4_2","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation. Verification","author":"Borzoo Bonakdarpour","year":"2018","unstructured":"Bonakdarpour, B., S\u00e1nchez, C., Schneider, G.: Monitoring hyperproperties by combining static analysis and runtime verification. In: Proceedings of ISoLA. LNCS, vol. 11245, pp. 8\u201327. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-030-03421-4_2"},{"key":"358_CR4","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1007\/978-3-662-54580-5_5","volume":"10206","author":"N Brett","year":"2017","unstructured":"Brett, N., Siddique, U., Bonakdarpour, B.: Rewriting-based runtime verification for alternation-free hyperltl. Proce. TACAS. LNCS 10206, 77\u201393 (2017). https:\/\/doi.org\/10.1007\/978-3-662-54580-5_5","journal-title":"Proce. TACAS. LNCS"},{"key":"358_CR5","doi-asserted-by":"publisher","unstructured":"Brewer, E.A.: Towards robust distributed systems (abstract). In: Proceedings of PODC, p.\u00a07. ACM (2000). https:\/\/doi.org\/10.1145\/343477.343502","DOI":"10.1145\/343477.343502"},{"issue":"10","key":"358_CR6","doi-asserted-by":"publisher","first-page":"1030","DOI":"10.1145\/4372.4373","volume":"28","author":"D Chaum","year":"1985","unstructured":"Chaum, D.: Security without identification: transaction systems to make big brother obsolete. Commun. ACM 28(10), 1030\u20131044 (1985). https:\/\/doi.org\/10.1145\/4372.4373","journal-title":"Commun. ACM"},{"key":"358_CR7","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1016\/j.entcs.2004.01.018","volume":"112","author":"D Clark","year":"2005","unstructured":"Clark, D., Hunt, S., Malacaria, P.: Quantified interference for a while language. Electron. Notes Theor. Comput. Sci. 112, 149\u2013166 (2005). https:\/\/doi.org\/10.1016\/j.entcs.2004.01.018","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"358_CR8","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1007\/978-3-642-54792-8_15","volume-title":"Lecture Notes in Computer Science","author":"Michael R. Clarkson","year":"2014","unstructured":"Clarkson, M.R., Finkbeiner, B., Koleini, M., Micinski, K.K., Rabe, M.N., S\u00e1nchez, C.: Temporal logics for hyperproperties. In: Proceedings of POST. LNCS, vol.\u00a08414, pp. 265\u2013284. Springer (2014). https:\/\/doi.org\/10.1007\/978-3-642-54792-8_15"},{"issue":"6","key":"358_CR9","doi-asserted-by":"publisher","first-page":"1157","DOI":"10.3233\/JCS-2009-0393","volume":"18","author":"MR Clarkson","year":"2010","unstructured":"Clarkson, M.R., Schneider, F.B.: Hyperproperties. J. Comput. Secur. 18(6), 1157\u20131210 (2010). https:\/\/doi.org\/10.3233\/JCS-2009-0393","journal-title":"J. Comput. Secur."},{"key":"358_CR10","doi-asserted-by":"publisher","unstructured":"Coenen, N., Finkbeiner, B., Hahn, C., Hofmann, J.: The hierarchy of hyperlogics. In: Proceedings of LICS, pp. 1\u201313. IEEE (2019). https:\/\/doi.org\/10.1109\/LICS.2019.8785713","DOI":"10.1109\/LICS.2019.8785713"},{"key":"358_CR11","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1007\/978-3-030-25540-4_7","volume-title":"Computer Aided Verification","author":"Norine Coenen","year":"2019","unstructured":"Coenen, N., Finkbeiner, B., S\u00e1nchez, C., Tentrup, L.: Verifying hyperliveness. In: Proceedings of CAV. LNCS, vol. 11561, pp. 121\u2013139. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-25540-4_7"},{"key":"358_CR12","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Leonardo de Moura","year":"2008","unstructured":"de\u00a0Moura, L.M., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Proceedings of TACAS. LNCS, vol.\u00a04963, pp. 337\u2013340. Springer (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"358_CR13","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1007\/978-3-642-04761-9_24","volume-title":"Automated Technology for Verification and Analysis","author":"Rayna Dimitrova","year":"2009","unstructured":"Dimitrova, R., Finkbeiner, B.: Synthesis of fault-tolerant distributed systems. In: Proceedings of ATVA. LNCS, vol.\u00a05799, pp. 321\u2013336. Springer (2009). https:\/\/doi.org\/10.1007\/978-3-642-04761-9_24"},{"key":"358_CR14","doi-asserted-by":"publisher","first-page":"169","DOI":"10.1007\/978-3-642-27940-9_12","volume-title":"Lecture Notes in Computer Science","author":"Rayna Dimitrova","year":"2012","unstructured":"Dimitrova, R., Finkbeiner, B., Kov\u00e1cs, M., Rabe, M.N., Seidl, H.: Model checking information flow in reactive systems. In: Proceedings of VMCAI. LNCS, vol.\u00a07148, pp. 169\u2013185. Springer (2012). https:\/\/doi.org\/10.1007\/978-3-642-27940-9_12"},{"key":"358_CR15","doi-asserted-by":"publisher","unstructured":"Ehlers, R., Finkbeiner, B.: Symmetric synthesis. In: Proceedings of IARCS. LIPIcs, vol.\u00a093, pp. 26:1\u201326:13. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik (2017). https:\/\/doi.org\/10.4230\/LIPIcs.FSTTCS.2017.26","DOI":"10.4230\/LIPIcs.FSTTCS.2017.26"},{"key":"358_CR16","doi-asserted-by":"publisher","first-page":"354","DOI":"10.1007\/978-3-662-54577-5\\_20","volume":"10205","author":"P Faymonville","year":"2017","unstructured":"Faymonville, P., Finkbeiner, B., Rabe, M.N., Tentrup, L.: Encodings of bounded synthesis. Proc. TACAS. LNCS 10205, 354\u2013370 (2017). https:\/\/doi.org\/10.1007\/978-3-662-54577-5_20","journal-title":"Proc. TACAS. LNCS"},{"key":"358_CR17","doi-asserted-by":"publisher","unstructured":"Faymonville, P., Finkbeiner, B., Tentrup, L.: BoSy: An experimentation framework for bounded synthesis. In: Proceedings of CAV. LNCS, vol. 10427, pp. 325\u2013332. Springer (2017). https:\/\/doi.org\/10.1007\/978-3-319-63390-9_17","DOI":"10.1007\/978-3-319-63390-9_17"},{"key":"358_CR18","doi-asserted-by":"publisher","unstructured":"Finkbeiner, B., Hahn, C.: Deciding hyperproperties. In: Proceedings of CONCUR. LIPIcs, vol.\u00a059, pp. 13:1\u201313:14. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik (2016). https:\/\/doi.org\/10.4230\/LIPIcs.CONCUR.2016.13","DOI":"10.4230\/LIPIcs.CONCUR.2016.13"},{"key":"358_CR19","doi-asserted-by":"publisher","first-page":"521","DOI":"10.1007\/978-3-030-01090-4_31","volume-title":"Automated Technology for Verification and Analysis","author":"Bernd Finkbeiner","year":"2018","unstructured":"Finkbeiner, B., Hahn, C., Hans, T.: MGHyper: Checking satisfiability of HyperLTL formulas beyond the $$\\exists ^* \\forall ^*$$ fragment. In: Proceedings of ATVA. LNCS, vol. 11138, pp. 521\u2013527. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-030-01090-4_31"},{"key":"358_CR20","doi-asserted-by":"publisher","first-page":"289","DOI":"10.1007\/978-3-319-96145-3_16","volume-title":"Computer Aided Verification","author":"Bernd Finkbeiner","year":"2018","unstructured":"Finkbeiner, B., Hahn, C., Lukert, P., Stenger, M., Tentrup, L.: Synthesizing reactive systems from hyperproperties. In: Proceedings of CAV. LNCS, vol. 10981, pp. 289\u2013306. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-96145-3_16"},{"key":"358_CR21","doi-asserted-by":"publisher","first-page":"564","DOI":"10.1007\/978-3-319-63390-9_29","volume-title":"Computer Aided Verification","author":"Bernd Finkbeiner","year":"2017","unstructured":"Finkbeiner, B., Hahn, C., Stenger, M.: Eahyper: Satisfiability, implication, and equivalence checking of hyperproperties. In: Proceedings of CAV. LNCS, vol. 10427, pp. 564\u2013570. Springer (2017). https:\/\/doi.org\/10.1007\/978-3-319-63390-9_29"},{"key":"358_CR22","doi-asserted-by":"publisher","first-page":"190","DOI":"10.1007\/978-3-319-67531-2_12","volume-title":"Runtime Verification","author":"Bernd Finkbeiner","year":"2017","unstructured":"Finkbeiner, B., Hahn, C., Stenger, M., Tentrup, L.: Monitoring hyperproperties. In: Proceedings of RV. LNCS, vol. 10548, pp. 190\u2013207. Springer (2017). https:\/\/doi.org\/10.1007\/978-3-319-67531-2_12"},{"key":"358_CR23","doi-asserted-by":"publisher","first-page":"194","DOI":"10.1007\/978-3-319-89963-3_11","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Bernd Finkbeiner","year":"2018","unstructured":"Finkbeiner, B., Hahn, C., Stenger, M., Tentrup, L.: RVHyper: A runtime verification tool for temporal hyperproperties. In: Proceedings of TACAS. LNCS, vol. 10806, pp. 194\u2013200. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-89963-3_11"},{"key":"358_CR24","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-019-00334-z","author":"B Finkbeiner","year":"2019","unstructured":"Finkbeiner, B., Hahn, C., Stenger, M., Tentrup, L.: Monitoring hyperproperties. Formal Methods Syst. Des. (2019). https:\/\/doi.org\/10.1007\/s10703-019-00334-z","journal-title":"Formal Methods Syst. Des."},{"key":"358_CR25","doi-asserted-by":"publisher","first-page":"144","DOI":"10.1007\/978-3-319-96145-3_8","volume-title":"Computer Aided Verification","author":"Bernd Finkbeiner","year":"2018","unstructured":"Finkbeiner, B., Hahn, C., Torfah, H.: Model checking quantitative hyperproperties. In: Proceedings of CAV. LNCS, vol. 10981, pp. 144\u2013163. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-96145-3_8"},{"key":"358_CR26","doi-asserted-by":"publisher","first-page":"30","DOI":"10.1007\/978-3-319-21690-4_3","volume-title":"Computer Aided Verification","author":"Bernd Finkbeiner","year":"2015","unstructured":"Finkbeiner, B., Rabe, M.N., S\u00e1nchez, C.: Algorithms for model checking HyperLTL and HyperCTL*. In: Proceedings of CAV. LNCS, vol.\u00a09206, pp. 30\u201348. Springer (2015). https:\/\/doi.org\/10.1007\/978-3-319-21690-4_3"},{"key":"358_CR27","doi-asserted-by":"publisher","unstructured":"Finkbeiner, B., Schewe, S.: Uniform distributed synthesis. In: Proceedings of LICS, pp. 321\u2013330. IEEE Computer Society (2005). https:\/\/doi.org\/10.1109\/LICS.2005.53","DOI":"10.1109\/LICS.2005.53"},{"issue":"5\u20136","key":"358_CR28","doi-asserted-by":"publisher","first-page":"519","DOI":"10.1007\/s10009-012-0228-z","volume":"15","author":"B Finkbeiner","year":"2013","unstructured":"Finkbeiner, B., Schewe, S.: Bounded synthesis. STTT 15(5\u20136), 519\u2013539 (2013). https:\/\/doi.org\/10.1007\/s10009-012-0228-z","journal-title":"STTT"},{"key":"358_CR29","doi-asserted-by":"publisher","first-page":"78","DOI":"10.1007\/978-3-642-54862-8_6","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Bernd Finkbeiner","year":"2014","unstructured":"Finkbeiner, B., Tentrup, L.: Detecting unrealizable specifications of distributed systems. In: Proceedings of TACAS. LNCS, vol.\u00a08413, pp. 78\u201392. Springer (2014). https:\/\/doi.org\/10.1007\/978-3-642-54862-8_6"},{"key":"358_CR30","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-11(3:12)2015","author":"B Finkbeiner","year":"2015","unstructured":"Finkbeiner, B., Tentrup, L.: Detecting unrealizability of distributed fault-tolerant systems. Log. Methods Comput. Sci. (2015). https:\/\/doi.org\/10.2168\/LMCS-11(3:12)2015","journal-title":"Log. Methods Comput. Sci."},{"key":"358_CR31","doi-asserted-by":"publisher","unstructured":"Finkbeiner, B., Zimmermann, M.: The first-order logic of hyperproperties. In: Proceedings of STACS. LIPIcs, vol.\u00a066, pp. 30:1\u201330:14. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik (2017). https:\/\/doi.org\/10.4230\/LIPIcs.STACS.2017.30","DOI":"10.4230\/LIPIcs.STACS.2017.30"},{"key":"358_CR32","doi-asserted-by":"publisher","unstructured":"Goguen, J.A., Meseguer, J.: Security policies and security models. In: Proceedings of S&P, pp. 11\u201320. IEEE Computer Society (1982). https:\/\/doi.org\/10.1109\/SP.1982.10014","DOI":"10.1109\/SP.1982.10014"},{"key":"358_CR33","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1007\/978-3-030-32079-9_5","volume-title":"Runtime Verification","author":"Christopher Hahn","year":"2019","unstructured":"Hahn, C.: Algorithms for monitoring hyperproperties. In: Proceedings of RV. LNCS, vol. 11757, pp. 70\u201390. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-32079-9_5"},{"key":"358_CR34","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1007\/978-3-030-17465-1_7","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Christopher Hahn","year":"2019","unstructured":"Hahn, C., Stenger, M., Tentrup, L.: Constraint-based monitoring of hyperproperties. In: Proceedings of TACAS. LNCS, vol. 11428, pp. 115\u2013131. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-17465-1_7"},{"key":"358_CR35","unstructured":"Kupferman, O., Vardi, M.Y.: Synthesis with incomplete information. In: ICTL (1997)"},{"key":"358_CR36","doi-asserted-by":"publisher","unstructured":"Kupferman, O., Vardi, M.Y.: Safraless decision procedures. In: Proceedings of FOCS, pp. 531\u2013542. IEEE Computer Society (2005). https:\/\/doi.org\/10.1109\/SFCS.2005.66","DOI":"10.1109\/SFCS.2005.66"},{"key":"358_CR37","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-4222-2","volume-title":"Temporal Verification of Reactive Systems-Safety","author":"Z Manna","year":"1995","unstructured":"Manna, Z., Pnueli, A.: Temporal Verification of Reactive Systems-Safety. Springer, Berlin (1995)"},{"issue":"1","key":"358_CR38","doi-asserted-by":"publisher","first-page":"37","DOI":"10.3233\/JCS-1992-1103","volume":"1","author":"J McLean","year":"1992","unstructured":"McLean, J.: Proving noninterference and functional correctness using traces. J. Comput. Secur. 1(1), 37\u201358 (1992). https:\/\/doi.org\/10.3233\/JCS-1992-1103","journal-title":"J. Comput. Secur."},{"key":"358_CR39","doi-asserted-by":"publisher","unstructured":"Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: Proceedings of POPL, pp. 179\u2013190. ACM Press (1989). https:\/\/doi.org\/10.1145\/75277.75293","DOI":"10.1145\/75277.75293"},{"key":"358_CR40","doi-asserted-by":"publisher","unstructured":"Pnueli, A., Rosner, R.: Distributed reactive systems are hard to synthesize. In: Proceedings of FOCS. pp. 746\u2013757. IEEE Computer Society (1990). https:\/\/doi.org\/10.1109\/FSCS.1990.89597","DOI":"10.1109\/FSCS.1990.89597"},{"issue":"4","key":"358_CR41","doi-asserted-by":"publisher","first-page":"264","DOI":"10.1090\/S0002-9904-1946-08555-9","volume":"52","author":"EL Post","year":"1946","unstructured":"Post, E.L.: A variant of a recursively unsolvable problem. Bull. Am. Math. Soc. 52(4), 264\u2013268 (1946)","journal-title":"Bull. Am. Math. Soc."},{"key":"358_CR42","doi-asserted-by":"publisher","unstructured":"Schewe, S., Finkbeiner, B.: Synthesis of asynchronous systems. In: Proceedings of LOPSTR. LNCS, vol.\u00a04407, pp. 127\u2013142. Springer (2006). https:\/\/doi.org\/10.1007\/978-3-540-71410-1_10","DOI":"10.1007\/978-3-540-71410-1_10"},{"issue":"3","key":"358_CR43","doi-asserted-by":"publisher","first-page":"733","DOI":"10.1145\/3828.3837","volume":"32","author":"AP Sistla","year":"1985","unstructured":"Sistla, A.P., Clarke, E.M.: The complexity of propositional linear temporal logics. J. ACM 32(3), 733\u2013749 (1985). https:\/\/doi.org\/10.1145\/3828.3837","journal-title":"J. ACM"}],"container-title":["Acta Informatica"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-019-00358-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00236-019-00358-2\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-019-00358-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,12,6]],"date-time":"2020-12-06T00:39:19Z","timestamp":1607215159000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s00236-019-00358-2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,12,7]]},"references-count":43,"journal-issue":{"issue":"1-2","published-print":{"date-parts":[[2020,4]]}},"alternative-id":["358"],"URL":"https:\/\/doi.org\/10.1007\/s00236-019-00358-2","relation":{},"ISSN":["0001-5903","1432-0525"],"issn-type":[{"value":"0001-5903","type":"print"},{"value":"1432-0525","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,12,7]]},"assertion":[{"value":"15 January 2019","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"22 November 2019","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"7 December 2019","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}