{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T09:03:36Z","timestamp":1770282216707,"version":"3.49.0"},"publisher-location":"New York, NY, USA","reference-count":35,"publisher":"ACM","license":[{"start":{"date-parts":[[2022,5,4]],"date-time":"2022-05-04T00:00:00Z","timestamp":1651622400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"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":["389792660? TRR 248, SCHM 3541\/1-1"],"award-info":[{"award-number":["389792660? TRR 248, SCHM 3541\/1-1"]}],"id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2022,5,4]]},"DOI":"10.1145\/3501710.3519535","type":"proceedings-article","created":{"date-parts":[[2022,4,28]],"date-time":"2022-04-28T14:28:32Z","timestamp":1651156112000},"page":"1-11","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["BOCoSy: Small but Powerful Symbolic Output-Feedback Control"],"prefix":"10.1145","author":[{"given":"Bernd","family":"Finkbeiner","sequence":"first","affiliation":[{"name":"CISPA Helmholtz Center for Information Security, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Kaushik","family":"Mallik","sequence":"additional","affiliation":[{"name":"Max-Planck Institute for Software Systems, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Noemi","family":"Passing","sequence":"additional","affiliation":[{"name":"CISPA Helmholtz Center for Information Security, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Malte","family":"Schledjewski","sequence":"additional","affiliation":[{"name":"CISPA Helmholtz Center for Information Security, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Anne-Kathrin","family":"Schmuck","sequence":"additional","affiliation":[{"name":"Max-Planck Institute for Software Systems, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2022,5,4]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1109\/LCSYS.2020.3034274"},{"key":"e_1_3_2_1_2_1","volume-title":"Principles of Model Checkit","author":"Baier Christel","unstructured":"Christel Baier and Joost-Pieter Katoen . 2008. Principles of Model Checkit . MIT Press . Christel Baier and Joost-Pieter Katoen. 2008. Principles of Model Checkit. MIT Press."},{"key":"e_1_3_2_1_4_1","volume-title":"Technical Report 11\/2","author":"Biere Armin","unstructured":"Armin Biere , Keijo Heljanko , and Siert Wieringa . 2011. AIGER 1.9 And Beyond . Technical Report 11\/2 . Institute for Formal Models and Verification, Johannes Kepler University , Altenbergerstr. 69, 4040 Linz, Austria. Armin Biere, Keijo Heljanko, and Siert Wieringa. 2011. AIGER 1.9 And Beyond. Technical Report 11\/2. Institute for Formal Models and Verification, Johannes Kepler University, Altenbergerstr. 69, 4040 Linz, Austria."},{"key":"e_1_3_2_1_5_1","volume-title":"Proceedings(Lecture Notes in Computer Science, Vol.\u00a06803)","author":"Biere Armin","year":"2011","unstructured":"Armin Biere , Florian Lonsing , and Martina Seidl . 2011 . Blocked Clause Elimination for QBF. In Automated Deduction - CADE-23 - 23rd International Conference on Automated Deduction, Wroclaw, Poland, July 31 - August 5, 2011 . Proceedings(Lecture Notes in Computer Science, Vol.\u00a06803) , Nikolaj Bj\u00f6rner and Viorica Sofronie-Stokkermans (Eds.). Springer, 101\u2013115. https:\/\/doi.org\/10.1007\/978-3-642-22438-6_10 10.1007\/978-3-642-22438-6_10 Armin Biere, Florian Lonsing, and Martina Seidl. 2011. Blocked Clause Elimination for QBF. In Automated Deduction - CADE-23 - 23rd International Conference on Automated Deduction, Wroclaw, Poland, July 31 - August 5, 2011. Proceedings(Lecture Notes in Computer Science, Vol.\u00a06803), Nikolaj Bj\u00f6rner and Viorica Sofronie-Stokkermans (Eds.). Springer, 101\u2013115. https:\/\/doi.org\/10.1007\/978-3-642-22438-6_10"},{"key":"e_1_3_2_1_6_1","volume-title":"Algorithms for Omega-Regular Games with Imperfect Information. Logical Methods in Computer Science 3, 3","author":"Chatterjee Krishnendu","year":"2007","unstructured":"Krishnendu Chatterjee , Laurent Doyen , Thomas\u00a0 A. Henzinger , and Jean-Fran\u00e7ois Raskin . 2007. Algorithms for Omega-Regular Games with Imperfect Information. Logical Methods in Computer Science 3, 3 ( 2007 ). Krishnendu Chatterjee, Laurent Doyen, Thomas\u00a0A. Henzinger, and Jean-Fran\u00e7ois Raskin. 2007. Algorithms for Omega-Regular Games with Imperfect Information. Logical Methods in Computer Science 3, 3 (2007)."},{"key":"#cr-split#-e_1_3_2_1_7_1.1","unstructured":"Rayna Dimitrova and Bernd Finkbeiner. 2008. Abstraction Refinement for Games with Incomplete Information. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science 2008(LIPIcs Vol.\u00a02) Ramesh Hariharan Madhavan Mukund and V.\u00a0Vinay (Eds.). Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik 175-186. https:\/\/doi.org\/10.4230\/LIPIcs.FSTTCS.2008.1751 10.4230\/LIPIcs.FSTTCS.2008.1751"},{"key":"#cr-split#-e_1_3_2_1_7_1.2","unstructured":"Rayna Dimitrova and Bernd Finkbeiner. 2008. Abstraction Refinement for Games with Incomplete Information. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science 2008(LIPIcs Vol.\u00a02) Ramesh Hariharan Madhavan Mukund and V.\u00a0Vinay (Eds.). Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik 175-186. https:\/\/doi.org\/10.4230\/LIPIcs.FSTTCS.2008.1751"},{"key":"e_1_3_2_1_8_1","volume-title":"Counterexample-Guided Synthesis of Observation Predicates. In FORMATS 2012(Lecture Notes in Computer Science, Vol.\u00a07595)","author":"Dimitrova Rayna","year":"2012","unstructured":"Rayna Dimitrova and Bernd Finkbeiner . 2012 . Counterexample-Guided Synthesis of Observation Predicates. In FORMATS 2012(Lecture Notes in Computer Science, Vol.\u00a07595) , Marcin Jurdzinski and Dejan Nickovic (Eds.). Springer, 107\u2013122. https:\/\/doi.org\/10.1007\/978-3-642-33365-1_9 10.1007\/978-3-642-33365-1_9 Rayna Dimitrova and Bernd Finkbeiner. 2012. Counterexample-Guided Synthesis of Observation Predicates. In FORMATS 2012(Lecture Notes in Computer Science, Vol.\u00a07595), Marcin Jurdzinski and Dejan Nickovic (Eds.). Springer, 107\u2013122. https:\/\/doi.org\/10.1007\/978-3-642-33365-1_9"},{"key":"e_1_3_2_1_9_1","volume-title":"ATVA 2016, Chiba, Japan, October 17-20, 2016, Proceedings(Lecture Notes in Computer Science, Vol.\u00a09938)","author":"Duret-Lutz Alexandre","year":"2016","unstructured":"Alexandre Duret-Lutz , Alexandre Lewkowicz , Amaury Fauchille , Thibaud Michaud , Etienne Renault , and Laurent Xu . 2016 . Spot 2.0 - A Framework for LTL and \\omega -Automata Manipulation. In Automated Technology for Verification and Analysis - 14th International Symposium , ATVA 2016, Chiba, Japan, October 17-20, 2016, Proceedings(Lecture Notes in Computer Science, Vol.\u00a09938) , Cyrille Artho, Axel Legay, and Doron Peled (Eds.). 122\u2013129. https:\/\/doi.org\/10.1007\/978-3-319-46520-3_8 10.1007\/978-3-319-46520-3_8 Alexandre Duret-Lutz, Alexandre Lewkowicz, Amaury Fauchille, Thibaud Michaud, Etienne Renault, and Laurent Xu. 2016. Spot 2.0 - A Framework for LTL and \\omega -Automata Manipulation. In Automated Technology for Verification and Analysis - 14th International Symposium, ATVA 2016, Chiba, Japan, October 17-20, 2016, Proceedings(Lecture Notes in Computer Science, Vol.\u00a09938), Cyrille Artho, Axel Legay, and Doron Peled (Eds.). 122\u2013129. https:\/\/doi.org\/10.1007\/978-3-319-46520-3_8"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"crossref","unstructured":"R\u00fcdiger Ehlers and Ufuk Topcu. 2015. Estimator-based reactive synthesis under incomplete information. In HSCC\u201915. ACM 249\u2013258. R\u00fcdiger Ehlers and Ufuk Topcu. 2015. Estimator-based reactive synthesis under incomplete information. In HSCC\u201915. ACM 249\u2013258.","DOI":"10.1145\/2728606.2728626"},{"key":"e_1_3_2_1_11_1","first-page":"3404","article-title":"Output Observability of Systems Over Finite Alphabets With Linear Internal Dynamics","volume":"63","author":"Fan Donglei","year":"2018","unstructured":"Donglei Fan and Danielle\u00a0 C Tarraf . 2018 . Output Observability of Systems Over Finite Alphabets With Linear Internal Dynamics . IEEE TAC 63 , 10 (2018), 3404 \u2013 3417 . Donglei Fan and Danielle\u00a0C Tarraf. 2018. Output Observability of Systems Over Finite Alphabets With Linear Internal Dynamics. IEEE TAC 63, 10 (2018), 3404\u20133417.","journal-title":"IEEE TAC"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54577-5_20"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63390-9_17"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.277.7"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"crossref","unstructured":"Thomas\u00a0A. Henzinger Rupak Majumdar Freddy Y.\u00a0C. Mang and Jean-Fran\u00e7ois Raskin. 2000. Abstract Interpretation of Game Properties. In SAS. 220\u2013239. Thomas\u00a0A. Henzinger Rupak Majumdar Freddy Y.\u00a0C. Mang and Jean-Fran\u00e7ois Raskin. 2000. Abstract Interpretation of Game Properties. In SAS. 220\u2013239.","DOI":"10.1007\/978-3-540-45099-3_12"},{"key":"e_1_3_2_1_16_1","volume-title":"Lazy Abstraction-Based Control for Safety Specifications. In 2018 IEEE Conference on Decision and Control (CDC). IEEE, 4902\u20134907","author":"Hsu Kyle","year":"2018","unstructured":"Kyle Hsu , Rupak Majumdar , Kaushik Mallik , and Anne-Kathrin Schmuck . 2018 . Lazy Abstraction-Based Control for Safety Specifications. In 2018 IEEE Conference on Decision and Control (CDC). IEEE, 4902\u20134907 . Kyle Hsu, Rupak Majumdar, Kaushik Mallik, and Anne-Kathrin Schmuck. 2018. Lazy Abstraction-Based Control for Safety Specifications. In 2018 IEEE Conference on Decision and Control (CDC). IEEE, 4902\u20134907."},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1109\/CDC.2018.8619649"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ifacol.2020.12.2348"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.229.10"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.artint.2016.01.004"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.23919\/ECC.2009.7074611"},{"key":"e_1_3_2_1_22_1","volume-title":"Synthesis with Incomplete Informatio","author":"Kupferman Orna","unstructured":"Orna Kupferman and Moshe\u00a0 Y. Vardi . 2000. Synthesis with Incomplete Informatio . Springer Netherlands , Dordrecht , 109\u2013127. https:\/\/doi.org\/10.1007\/978-94-015-9586-5_6 10.1007\/978-94-015-9586-5_6 Orna Kupferman and Moshe\u00a0Y. Vardi. 2000. Synthesis with Incomplete Informatio. Springer Netherlands, Dordrecht, 109\u2013127. https:\/\/doi.org\/10.1007\/978-94-015-9586-5_6"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.2005.66"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3365365.3382219"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.nahs.2018.04.001"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1013339920783"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.automatica.2019.108511"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(84)90034-5"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1109\/TAC.2016.2593947"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/2883817.2883834"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-75596-8_33"},{"key":"e_1_3_2_1_32_1","first-page":"155","article-title":"CAQE and QuAbS: Abstraction Based QBF Solvers","volume":"11","author":"Tentrup Leander","year":"2019","unstructured":"Leander Tentrup . 2019 . CAQE and QuAbS: Abstraction Based QBF Solvers . J. Satisf. Boolean Model. Comput. 11 , 1 (2019), 155 \u2013 210 . https:\/\/doi.org\/10.3233\/SAT190121 10.3233\/SAT190121 Leander Tentrup. 2019. CAQE and QuAbS: Abstraction Based QBF Solvers. J. Satisf. Boolean Model. Comput. 11, 1 (2019), 155\u2013210. https:\/\/doi.org\/10.3233\/SAT190121","journal-title":"J. Satisf. Boolean Model. Comput."},{"key":"e_1_3_2_1_33_1","volume-title":"Handbook of Theoretical Computer Science, J.\u00a0van Leeuwen (Ed.). Vol.\u00a0B","author":"Thomas W.","unstructured":"W. Thomas . 1990. Automata on infinite objects . In Handbook of Theoretical Computer Science, J.\u00a0van Leeuwen (Ed.). Vol.\u00a0B . Elsevier , 133\u2013191. W. Thomas. 1990. Automata on infinite objects. In Handbook of Theoretical Computer Science, J.\u00a0van Leeuwen (Ed.). Vol.\u00a0B. Elsevier, 133\u2013191."},{"key":"e_1_3_2_1_34_1","volume-title":"STACS\u201995(Lecture Notes in Computer Science, Vol.\u00a0900)","author":"Thomas W.","unstructured":"W. Thomas . 1995. On the Synthesis of Strategies in Infinite Games . In STACS\u201995(Lecture Notes in Computer Science, Vol.\u00a0900) . Springer-Verlag , 1\u201313. W. Thomas. 1995. On the Synthesis of Strategies in Infinite Games. In STACS\u201995(Lecture Notes in Computer Science, Vol.\u00a0900). Springer-Verlag, 1\u201313."},{"key":"e_1_3_2_1_35_1","volume-title":"Retrieved","author":"Wolf Clifford","year":"2013","unstructured":"Clifford Wolf . 2013 . Yosys Open Synthesis Suite . Retrieved March 14, 2022 from https:\/\/yosyshq.net\/yosys\/ Clifford Wolf. 2013. Yosys Open Synthesis Suite. Retrieved March 14, 2022 from https:\/\/yosyshq.net\/yosys\/"}],"event":{"name":"HSCC '22: 25th ACM International Conference on Hybrid Systems: Computation and Control","location":"Milan Italy","acronym":"HSCC '22","sponsor":["SIGBED ACM Special Interest Group on Embedded Systems"]},"container-title":["25th ACM International Conference on Hybrid Systems: Computation and Control"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3501710.3519535","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3501710.3519535","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T18:10:11Z","timestamp":1750183811000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3501710.3519535"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,5,4]]},"references-count":35,"alternative-id":["10.1145\/3501710.3519535","10.1145\/3501710"],"URL":"https:\/\/doi.org\/10.1145\/3501710.3519535","relation":{},"subject":[],"published":{"date-parts":[[2022,5,4]]},"assertion":[{"value":"2022-05-04","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}