{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,24]],"date-time":"2025-08-24T01:44:37Z","timestamp":1755999877664,"version":"3.40.3"},"publisher-location":"Cham","reference-count":41,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030317836"},{"type":"electronic","value":"9783030317843"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019]]},"DOI":"10.1007\/978-3-030-31784-3_2","type":"book-chapter","created":{"date-parts":[[2019,10,21]],"date-time":"2019-10-21T01:32:04Z","timestamp":1571621524000},"page":"23-47","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Lazy Abstraction-Based Controller Synthesis"],"prefix":"10.1007","author":[{"given":"Kyle","family":"Hsu","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Rupak","family":"Majumdar","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Kaushik","family":"Mallik","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Anne-Kathrin","family":"Schmuck","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2019,10,21]]},"reference":[{"doi-asserted-by":"crossref","unstructured":"Ames, A.D., et al.: First steps toward formal controller synthesis for bipedal robots. In: Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control, pp. 209\u2013218. ACM (2015)","key":"2_CR1","DOI":"10.1145\/2728606.2728611"},{"unstructured":"Gol, E.A., Lazar, M., Belta, C.: Language-guided controller synthesis for discrete-time linear systems. In: HSCC, pp. 95\u2013104. ACM (2012)","key":"2_CR2"},{"issue":"5\u20136","key":"2_CR3","doi-asserted-by":"publisher","first-page":"505","DOI":"10.1007\/s10009-007-0044-z","volume":"9","author":"D Beyer","year":"2007","unstructured":"Beyer, D., Henzinger, T.A., Jhala, R., Majumdar, R.: The software model checker blast. Int. J. Softw. Tools Technol. Transf. 9(5\u20136), 505\u2013525 (2007)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"2_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"184","DOI":"10.1007\/978-3-642-22110-1_16","volume-title":"Computer Aided Verification","author":"D Beyer","year":"2011","unstructured":"Beyer, D., Keremoglu, M.E.: CPAchecker: a tool for configurable software verification. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 184\u2013190. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_16"},{"issue":"27","key":"2_CR5","doi-asserted-by":"publisher","first-page":"285","DOI":"10.3182\/20130925-2-DE-4044.00056","volume":"46","author":"A Borri","year":"2013","unstructured":"Borri, A., Dimarogonas, D.V., Johansson, K.H., Di Benedetto, M.D., Pola, G.: Decentralized symbolic control of interconnected systems with application to vehicle platooning. IFAC Proc. Vol. 46(27), 285\u2013292 (2013)","journal-title":"IFAC Proc. Vol."},{"doi-asserted-by":"crossref","unstructured":"Bulancea, O.L., Nilsson, P., Ozay, N.: Nonuniform abstractions, refinement and controller synthesis with novel BDD encodings. arXiv preprint arXiv:1804.04280 (2018)","key":"2_CR6","DOI":"10.1016\/j.ifacol.2018.08.004"},{"doi-asserted-by":"crossref","unstructured":"C\u00e1mara, J., Girard, A., G\u00f6ssler, G.: Safety controller synthesis for switched systems using multi-scale symbolic models. In: CDC, pp. 520\u2013525 (2011)","key":"2_CR7","DOI":"10.1109\/CDC.2011.6160424"},{"doi-asserted-by":"crossref","unstructured":"C\u00e1mara, J., Girard, A., G\u00f6ssler, G.: Synthesis of switching controllers using approximately bisimilar multiscale abstractions. In: HSCC, pp. 191\u2013200 (2011)","key":"2_CR8","DOI":"10.1145\/1967701.1967730"},{"key":"2_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1007\/978-3-540-75454-1_3","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"F Cassez","year":"2007","unstructured":"Cassez, F.: Efficient on-the-fly algorithms for partially observable timed games. In: Raskin, J.-F., Thiagarajan, P.S. (eds.) FORMATS 2007. LNCS, vol. 4763, pp. 5\u201324. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-75454-1_3"},{"issue":"5","key":"2_CR10","doi-asserted-by":"publisher","first-page":"752","DOI":"10.1145\/876638.876643","volume":"50","author":"E Clarke","year":"2003","unstructured":"Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement for symbolic model checking. J. ACM 50(5), 752\u2013794 (2003)","journal-title":"J. ACM"},{"doi-asserted-by":"crossref","unstructured":"Coogan, S., Arcak, M.: Efficient finite abstraction of mixed monotone systems. In: Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control, pp. 58\u201367. ACM (2015)","key":"2_CR11","DOI":"10.1145\/2728606.2728607"},{"issue":"6","key":"2_CR12","doi-asserted-by":"publisher","first-page":"666","DOI":"10.1016\/j.ic.2009.05.007","volume":"208","author":"L Alfaro de","year":"2010","unstructured":"de Alfaro, L., Roy, P.: Solving games via three-valued abstraction refinement. Inf. Comput. 208(6), 666\u2013676 (2010)","journal-title":"Inf. Comput."},{"unstructured":"Fribourg, L., K\u00fchne, U., Soulat, R.: Constructing attractors of nonlinear dynamical systems. In: OASIcs-OpenAccess Series in Informatics, vol. 31. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik (2013)","key":"2_CR13"},{"issue":"3","key":"2_CR14","doi-asserted-by":"publisher","first-page":"303","DOI":"10.1007\/s10703-014-0211-2","volume":"45","author":"L Fribourg","year":"2014","unstructured":"Fribourg, L., K\u00fchne, U., Soulat, R.: Finite controlled invariants for sampled switched systems. Form. Methods Syst. Des. 45(3), 303\u2013329 (2014)","journal-title":"Form. Methods Syst. Des."},{"issue":"8","key":"2_CR15","first-page":"1261","volume":"51","author":"A Girard","year":"2006","unstructured":"Girard, A.: Towards a multiresolution approach to linear control. TAC 51(8), 1261\u20131270 (2006)","journal-title":"TAC"},{"issue":"6","key":"2_CR16","first-page":"1537","volume":"61","author":"A Girard","year":"2016","unstructured":"Girard, A., G\u00f6ssler, G., Mouelhi, S.: Safety controller synthesis for incrementally stable switched systems using multiscale symbolic models. TAC 61(6), 1537\u20131549 (2016)","journal-title":"TAC"},{"issue":"1","key":"2_CR17","first-page":"116","volume":"55","author":"A Girard","year":"2010","unstructured":"Girard, A., Pola, G., Tabuada, P.: Approximately bisimilar symbolic models for incrementally stable switched systems. TAC 55(1), 116\u2013126 (2010)","journal-title":"TAC"},{"doi-asserted-by":"crossref","unstructured":"Gruber, F., Kim, E.S., Arcak, M.: Sparsity-aware finite abstraction. In: 2017 IEEE 56th Annual Conference on Decision and Control (CDC), pp. 2366\u20132371. IEEE (2017)","key":"2_CR18","DOI":"10.1109\/CDC.2017.8263995"},{"issue":"3","key":"2_CR19","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1007\/s002110050241","volume":"75","author":"L Gr\u00fcne","year":"1997","unstructured":"Gr\u00fcne, L.: An adaptive grid scheme for the discrete Hamilton-Jacobi-Bellman equation. Numer. Math. 75(3), 319\u2013337 (1997)","journal-title":"Numer. Math."},{"key":"2_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"886","DOI":"10.1007\/3-540-45061-0_69","volume-title":"Automata, Languages and Programming","author":"TA Henzinger","year":"2003","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R.: Counterexample-guided control. In: Baeten, J.C.M., Lenstra, J.K., Parrow, J., Woeginger, G.J. (eds.) ICALP 2003. LNCS, vol. 2719, pp. 886\u2013902. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/3-540-45061-0_69"},{"issue":"1","key":"2_CR21","doi-asserted-by":"publisher","first-page":"58","DOI":"10.1145\/565816.503279","volume":"37","author":"TA Henzinger","year":"2002","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. ACM SIGPLAN Not. 37(1), 58\u201370 (2002)","journal-title":"ACM SIGPLAN Not."},{"key":"2_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"990","DOI":"10.1007\/978-3-642-39799-8_71","volume-title":"Computer Aided Verification","author":"F Herbreteau","year":"2013","unstructured":"Herbreteau, F., Srivathsan, B., Walukiewicz, I.: Lazy abstractions for timed automata. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 990\u20131005. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_71"},{"doi-asserted-by":"crossref","unstructured":"Hsu, K., Majumdar, R., Mallik, K., Schmuck, A.-K.: Lazy abstraction-based control for safety specifications. In: 2018 IEEE Conference on Decision and Control (CDC), pp. 4902\u20134907. IEEE (2018)","key":"2_CR23","DOI":"10.1109\/CDC.2018.8619659"},{"doi-asserted-by":"crossref","unstructured":"Hsu, K., Majumdar, R., Mallik, K., Schmuck, A.-K.: Lazy abstraction-based controller synthesis. arXiv preprint arXiv:1804.02722 (2018)","key":"2_CR24","DOI":"10.1007\/978-3-030-31784-3_2"},{"doi-asserted-by":"crossref","unstructured":"Hsu, K., Majumdar, R., Mallik, K., Schmuck, A.-K.: Multi-layered abstraction-based controller synthesis for continuous-time systems. In: HSCC, pp. 120\u2013129. ACM (2018)","key":"2_CR25","DOI":"10.1145\/3178126.3178143"},{"doi-asserted-by":"crossref","unstructured":"Khaled, M., Zamani, M.: pFaces: an acceleration ecosystem for symbolic control. In: Proceedings of the 22nd ACM International Conference on Hybrid Systems: Computation and Control, pp. 252\u2013257. ACM (2019)","key":"2_CR26","DOI":"10.1145\/3302504.3311798"},{"doi-asserted-by":"crossref","unstructured":"Li, Y., Liu, J.: ROCS: a robustly complete control synthesis tool for nonlinear dynamical systems. In: HSCC, pp. 130\u2013135. ACM (2018)","key":"2_CR27","DOI":"10.1145\/3178126.3187006"},{"key":"2_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1007\/3-540-59042-0_76","volume-title":"STACS 95","author":"O Maler","year":"1995","unstructured":"Maler, O., Pnueli, A., Sifakis, J.: On the synthesis of discrete controllers for timed systems. In: Mayr, E.W., Puech, C. (eds.) STACS 1995. LNCS, vol. 900, pp. 229\u2013242. Springer, Heidelberg (1995). https:\/\/doi.org\/10.1007\/3-540-59042-0_76"},{"issue":"6","key":"2_CR29","doi-asserted-by":"publisher","first-page":"2629","DOI":"10.1109\/TAC.2018.2869740","volume":"64","author":"K Mallik","year":"2018","unstructured":"Mallik, K., Schmuck, A.-K., Soudjani, S., Majumdar, R.: Compositional synthesis of finite-state abstractions. IEEE Trans. Autom. Control 64(6), 2629\u20132636 (2018)","journal-title":"IEEE Trans. Autom. Control"},{"key":"2_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"428","DOI":"10.1007\/978-3-540-71493-4_34","volume-title":"Hybrid Systems: Computation and Control","author":"IM Mitchell","year":"2007","unstructured":"Mitchell, I.M.: Comparing forward and backward reachability as tools for safety analysis. In: Bemporad, A., Bicchi, A., Buttazzo, G. (eds.) HSCC 2007. LNCS, vol. 4416, pp. 428\u2013443. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-71493-4_34"},{"doi-asserted-by":"crossref","unstructured":"Mouelhi, S., Girard, A., G\u00f6ssler, G.: CoSyMA: a tool for controller synthesis using multi-scale abstractions. In: HSCC, pp. 83\u201388. ACM (2013)","key":"2_CR31","DOI":"10.1145\/2461328.2461343"},{"issue":"4","key":"2_CR32","doi-asserted-by":"publisher","first-page":"1294","DOI":"10.1109\/TCST.2015.2501351","volume":"24","author":"P Nilsson","year":"2016","unstructured":"Nilsson, P., et al.: Correct-by-construction adaptive cruise control: two approaches. IEEE Trans. Contr. Sys. Techn. 24(4), 1294\u20131307 (2016)","journal-title":"IEEE Trans. Contr. Sys. Techn."},{"issue":"2","key":"2_CR33","doi-asserted-by":"publisher","first-page":"301","DOI":"10.1007\/s10626-017-0243-z","volume":"27","author":"P Nilsson","year":"2017","unstructured":"Nilsson, P., Ozay, N., Liu, J.: Augmented finite transition systems as abstractions for control synthesis. Discret. Event Dyn. Syst. 27(2), 301\u2013340 (2017)","journal-title":"Discret. Event Dyn. Syst."},{"issue":"2","key":"2_CR34","first-page":"534","volume":"57","author":"G Pola","year":"2012","unstructured":"Pola, G., Borri, A., Di Benedetto, M.D.: Integrated design of symbolic controllers for nonlinear systems. TAC 57(2), 534\u2013539 (2012)","journal-title":"TAC"},{"issue":"4","key":"2_CR35","first-page":"1781","volume":"62","author":"G Reissig","year":"2017","unstructured":"Reissig, G., Weber, A., Rungger, M.: Feedback refinement relations for the synthesis of symbolic controllers. TAC 62(4), 1781\u20131796 (2017)","journal-title":"TAC"},{"doi-asserted-by":"crossref","unstructured":"Rungger, M., Stursberg, O.: On-the-fly model abstraction for controller synthesis. In: ACC, pp. 2645\u20132650. IEEE (2012)","key":"2_CR36","DOI":"10.1109\/ACC.2012.6314891"},{"doi-asserted-by":"crossref","unstructured":"Rungger, M., Zamani, M.: SCOTS: a tool for the synthesis of symbolic controllers. In: HSCC, pp. 99\u2013104. ACM (2016)","key":"2_CR37","DOI":"10.1145\/2883817.2883834"},{"doi-asserted-by":"crossref","unstructured":"Saoud, A., Girard, A., Fribourg, L.: Contract based design of symbolic controllers for vehicle platooning. In: HSCC, pp. 277\u2013278. ACM (2018)","key":"2_CR38","DOI":"10.1145\/3178126.3187001"},{"key":"2_CR39","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4419-0224-5","volume-title":"Verification and Control of Hybrid Systems: A Symbolic Approach","author":"P Tabuada","year":"2009","unstructured":"Tabuada, P.: Verification and Control of Hybrid Systems: A Symbolic Approach. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-1-4419-0224-5"},{"unstructured":"Vizel, Y., Grumberg, O., Shoham, S.: Lazy abstraction and sat-based reachability in hardware model checking. In: FMCAD, pp. 173\u2013181. IEEE (2012)","key":"2_CR40"},{"doi-asserted-by":"crossref","unstructured":"Hussien, O., Tabuada, P.: Lazy controller synthesis using three-valued abstractions for safety and reachability specifications. In: CDC 2018, pp. 3567\u20133572 (2018)","key":"2_CR41","DOI":"10.1109\/CDC.2018.8619649"}],"container-title":["Lecture Notes in Computer Science","Automated Technology for Verification and Analysis"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-31784-3_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,10,2]],"date-time":"2022-10-02T05:50:51Z","timestamp":1664689851000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-31784-3_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030317836","9783030317843"],"references-count":41,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-31784-3_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"21 October 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ATVA","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Automated Technology for Verification and Analysis","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Taipei","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Taiwan","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28 October 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"31 October 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"17","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"atva2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/atva2019.iis.sinica.edu.tw\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Open","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":"87","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":"29","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":"33% - 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.4","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":"Between 1 and 2","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)"}}]}}