{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,13]],"date-time":"2026-05-13T14:02:58Z","timestamp":1778680978899,"version":"3.51.4"},"reference-count":48,"publisher":"Springer Science and Business Media LLC","issue":"1-2","license":[{"start":{"date-parts":[[2019,9,13]],"date-time":"2019-09-13T00:00:00Z","timestamp":1568332800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2019,9,13]],"date-time":"2019-09-13T00:00:00Z","timestamp":1568332800000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"name":"European Research Council","award":["725144"],"award-info":[{"award-number":["725144"]}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Acta Informatica"],"published-print":{"date-parts":[[2020,4]]},"DOI":"10.1007\/s00236-019-00341-x","type":"journal-article","created":{"date-parts":[[2019,9,13]],"date-time":"2019-09-13T19:10:41Z","timestamp":1568401841000},"page":"245-269","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Safety synthesis for incrementally stable switched systems using discretization-free multi-resolution abstractions"],"prefix":"10.1007","volume":"57","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-4075-9041","authenticated-orcid":false,"given":"Antoine","family":"Girard","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gregor","family":"G\u00f6ssler","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2019,9,13]]},"reference":[{"issue":"7","key":"341_CR1","doi-asserted-by":"publisher","first-page":"971","DOI":"10.1109\/5.871304","volume":"88","author":"R Alur","year":"2000","unstructured":"Alur, R., Henzinger, T.A., Lafferriere, G., Pappas, G.J.: Discrete abstractions of hybrid systems. Proc. IEEE 88(7), 971\u2013984 (2000)","journal-title":"Proc. IEEE"},{"issue":"3","key":"341_CR2","doi-asserted-by":"publisher","first-page":"410","DOI":"10.1109\/9.989067","volume":"47","author":"D Angeli","year":"2002","unstructured":"Angeli, D.: A Lyapunov approach to incremental stability properties. IEEE Trans. Autom. Control 47(3), 410\u2013421 (2002)","journal-title":"IEEE Trans. Autom. Control"},{"issue":"8","key":"341_CR3","doi-asserted-by":"publisher","first-page":"2163","DOI":"10.1016\/j.automatica.2007.12.012","volume":"44","author":"EM Aylward","year":"2008","unstructured":"Aylward, E.M., Parrilo, P.A., Slotine, J.J.E.: Stability and robustness analysis of nonlinear systems via contraction metrics and SOS programming. Automatica 44(8), 2163\u20132170 (2008)","journal-title":"Automatica"},{"key":"341_CR4","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-50763-7","volume-title":"Formal Methods for Discrete-Time Dynamical Systems","author":"C Belta","year":"2017","unstructured":"Belta, C., Yordanov, B., Aydin Gol, E.: Formal Methods for Discrete-Time Dynamical Systems, vol. 89. Springer, Berlin (2017)"},{"issue":"16","key":"341_CR5","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1016\/j.ifacol.2018.08.004","volume":"51","author":"OL Bulancea","year":"2018","unstructured":"Bulancea, O.L., Nilsson, P., Ozay, N.: Nonuniform abstractions, refinement and controller synthesis with novel BDD encodings. IFAC-PapersOnLine 51(16), 19\u201324 (2018)","journal-title":"IFAC-PapersOnLine"},{"issue":"4","key":"341_CR6","doi-asserted-by":"publisher","first-page":"501","DOI":"10.1109\/9.664153","volume":"43","author":"PE Caines","year":"1998","unstructured":"Caines, P.E., Wei, Y.J.: Hierarchical hybrid control systems: a lattice theoretic formulation. IEEE Trans. Autom. Control 43(4), 501\u2013508 (1998)","journal-title":"IEEE Trans. Autom. Control"},{"key":"341_CR7","doi-asserted-by":"crossref","unstructured":"C\u00e1mara, J., Girard, A., G\u00f6ssler, G.: Synthesis of switching controllers using approximately bisimilar multiscale abstractions. In: Hybrid Systems: Computation and Control, pp. 191\u2013200 (2011)","DOI":"10.1145\/1967701.1967730"},{"issue":"24","key":"341_CR8","doi-asserted-by":"publisher","first-page":"197","DOI":"10.3182\/20120912-3-BG-2031.00040","volume":"45","author":"C Canudas De Wit","year":"2012","unstructured":"Canudas De Wit, C., Ojeda, L.L., Kibangou, A.Y.: Graph constrained-CTM observer design for the Grenoble south ring. IFAC Proc. Vol. 45(24), 197\u2013202 (2012)","journal-title":"IFAC Proc. Vol."},{"key":"341_CR9","doi-asserted-by":"publisher","first-page":"254","DOI":"10.1016\/j.nahs.2016.04.005","volume":"23","author":"S Coogan","year":"2017","unstructured":"Coogan, S., Arcak, M.: Finite abstraction of mixed monotone systems with discrete and continuous inputs. Nonlinear Anal. Hybrid Syst. 23, 254\u2013271 (2017)","journal-title":"Nonlinear Anal. Hybrid Syst."},{"key":"341_CR10","doi-asserted-by":"crossref","unstructured":"Dallal, E., Tabuada, P.: On compositional symbolic controller synthesis inspired by small-gain theorems. In: IEEE Conference on Decision and Control, pp. 6133\u20136138 (2015)","DOI":"10.1109\/CDC.2015.7403184"},{"key":"341_CR11","doi-asserted-by":"crossref","unstructured":"Girard, A.: Approximately bisimilar abstractions of incrementally stable finite or infinite dimensional systems. In: IEEE Conference on Decision and Control, pp. 824\u2013829 (2014)","DOI":"10.1109\/CDC.2014.7039483"},{"issue":"6","key":"341_CR12","doi-asserted-by":"publisher","first-page":"1537","DOI":"10.1109\/TAC.2015.2478131","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. IEEE Trans. Autom. Control 61(6), 1537\u20131549 (2016)","journal-title":"IEEE Trans. Autom. Control"},{"issue":"5","key":"341_CR13","doi-asserted-by":"publisher","first-page":"782","DOI":"10.1109\/TAC.2007.895849","volume":"52","author":"A Girard","year":"2007","unstructured":"Girard, A., Pappas, G.: Approximation metrics for discrete and continuous systems. IEEE Trans. Autom. Control 52(5), 782\u2013798 (2007)","journal-title":"IEEE Trans. Autom. Control"},{"issue":"1","key":"341_CR14","doi-asserted-by":"publisher","first-page":"116","DOI":"10.1109\/TAC.2009.2034922","volume":"55","author":"A Girard","year":"2010","unstructured":"Girard, A., Pola, G., Tabuada, P.: Approximately bisimilar symbolic models for incrementally stable switched systems. IEEE Trans. Autom. Control 55(1), 116\u2013126 (2010)","journal-title":"IEEE Trans. Autom. Control"},{"key":"341_CR15","doi-asserted-by":"crossref","unstructured":"Gruber, F., Kim, E.S., Arcak, M.: Sparsity-aware finite abstraction. In: IEEE Conference on Decision and Control, pp. 2366\u20132371 (2017)","DOI":"10.1109\/CDC.2017.8263995"},{"key":"341_CR16","doi-asserted-by":"crossref","unstructured":"Hsu, K., Majumdar, R., Mallik, K., Schmuck, A.K.: Lazy abstraction-based control for safety specifications. arXiv preprint \narXiv:1804.02666\n\n (2018)","DOI":"10.1109\/CDC.2018.8619659"},{"key":"341_CR17","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: International Conference on Hybrid Systems: Computation and Control, pp. 120\u2013129 (2018)","DOI":"10.1145\/3178126.3178143"},{"issue":"2","key":"341_CR18","doi-asserted-by":"publisher","first-page":"227","DOI":"10.1109\/LCSYS.2017.2713461","volume":"1","author":"O Hussien","year":"2017","unstructured":"Hussien, O., Ames, A., Tabuada, P.: Abstracting partially feedback linearizable systems compositionally. IEEE Control Syst. Lett. 1(2), 227\u2013232 (2017)","journal-title":"IEEE Control Syst. Lett."},{"key":"341_CR19","doi-asserted-by":"crossref","unstructured":"Kim, E.S., Arcak, M., Seshia, S.A.: Compositional controller synthesis for vehicular traffic networks. In: IEEE Conference on Decision and Control, pp. 6165\u20136171 (2015)","DOI":"10.1109\/CDC.2015.7403189"},{"key":"341_CR20","doi-asserted-by":"crossref","unstructured":"Kim, E.S., Arcak, M., Zamani, M.: Constructing control system abstractions from modular components. In: International Conference on Hybrid Systems: Computation and Control, pp. 137\u2013146 (2018)","DOI":"10.1145\/3178126.3178144"},{"issue":"7","key":"341_CR21","doi-asserted-by":"publisher","first-page":"1026","DOI":"10.1109\/5.871307","volume":"88","author":"XD Koutsoukos","year":"2000","unstructured":"Koutsoukos, X.D., Antsaklis, P.J., Stiver, J.A., Lemmon, M.D.: Supervisory control of hybrid systems. Proc. IEEE 88(7), 1026\u20131049 (2000)","journal-title":"Proc. IEEE"},{"key":"341_CR22","doi-asserted-by":"crossref","unstructured":"Le\u00a0Corronc, E., Girard, A., G\u00f6ssler, G.: Mode sequences as symbolic states in abstractions of incrementally stable switched systems. In: IEEE Conference on Decision and Control, pp. 3225\u20133230 (2013)","DOI":"10.1109\/CDC.2013.6760375"},{"key":"341_CR23","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.nahs.2016.02.002","volume":"22","author":"J Liu","year":"2016","unstructured":"Liu, J., Ozay, N.: Finite abstractions with robustness margins for temporal logic-based control synthesis. Nonlinear Anal. Hybrid Syst. 22, 1\u201315 (2016)","journal-title":"Nonlinear Anal. Hybrid Syst."},{"issue":"3","key":"341_CR24","doi-asserted-by":"publisher","first-page":"417","DOI":"10.1016\/0005-1098(94)90119-8","volume":"30","author":"J Lunze","year":"1994","unstructured":"Lunze, J.: Qualitative modelling of linear dynamical systems with quantized state measurements. Automatica 30(3), 417\u2013431 (1994)","journal-title":"Automatica"},{"issue":"1","key":"341_CR25","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1109\/TAC.2014.2325635","volume":"60","author":"J Maidens","year":"2014","unstructured":"Maidens, J., Arcak, M.: Reachability analysis of nonlinear systems using matrix measures. IEEE Trans. Autom. Control 60(1), 265\u2013270 (2014)","journal-title":"IEEE Trans. Autom. Control"},{"key":"341_CR26","unstructured":"Majumdar, R., Mallik, K., Schmuck, A.K.: Compositional synthesis of finite state abstractions. arXiv preprint \narXiv:1612.08515\n\n (2016)"},{"issue":"2","key":"341_CR27","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1016\/S1367-5788(02)00030-5","volume":"26","author":"O Maler","year":"2002","unstructured":"Maler, O.: Control from computer science. Annu. Rev. Control 26(2), 175\u2013187 (2002)","journal-title":"Annu. Rev. Control"},{"issue":"6","key":"341_CR28","doi-asserted-by":"publisher","first-page":"1835","DOI":"10.1109\/TAC.2017.2753039","volume":"63","author":"PJ Meyer","year":"2018","unstructured":"Meyer, P.J., Girard, A., Witrant, E.: Compositional abstraction and safety synthesis using overlapping symbolic models. IEEE Trans. Autom. Control 63(6), 1835\u20131841 (2018)","journal-title":"IEEE Trans. Autom. Control"},{"key":"341_CR29","first-page":"364","volume-title":"Lecture Notes in Computer Science","author":"Nir Piterman","year":"2005","unstructured":"Piterman, N., Pnueli, A., Sa\u2019ar, Y.: Synthesis of reactive (1) designs. In: International Workshop on Verification, Model Checking, and Abstract Interpretation, pp. 364\u2013380 (2006)"},{"key":"341_CR30","doi-asserted-by":"crossref","unstructured":"Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: Symposium on Principles of Programming Languages, pp. 179\u2013190. ACM (1989)","DOI":"10.1145\/75277.75293"},{"issue":"2","key":"341_CR31","doi-asserted-by":"publisher","first-page":"534","DOI":"10.1109\/TAC.2011.2164740","volume":"57","author":"G Pola","year":"2012","unstructured":"Pola, G., Borri, A., Di Benedetto, M.: Integrated design of symbolic controllers for nonlinear systems. IEEE Trans. Autom. Control 57(2), 534\u2013539 (2012)","journal-title":"IEEE Trans. Autom. Control"},{"issue":"11","key":"341_CR32","doi-asserted-by":"publisher","first-page":"3663","DOI":"10.1109\/TAC.2016.2528046","volume":"61","author":"G Pola","year":"2016","unstructured":"Pola, G., Pepe, P., Di Benedetto, M.D.: Symbolic models for networks of control systems. IEEE Trans. Autom. Control 61(11), 3663\u20133668 (2016)","journal-title":"IEEE Trans. Autom. Control"},{"issue":"9","key":"341_CR33","doi-asserted-by":"publisher","first-page":"2803","DOI":"10.1109\/TAC.2017.2775962","volume":"63","author":"G Pola","year":"2018","unstructured":"Pola, G., Pepe, P., Di Benedetto, M.D.: Decentralized supervisory control of networks of nonlinear control systems. IEEE Trans. Autom. Control 63(9), 2803\u20132817 (2018)","journal-title":"IEEE Trans. Autom. Control"},{"issue":"4","key":"341_CR34","doi-asserted-by":"publisher","first-page":"569","DOI":"10.1109\/9.664160","volume":"43","author":"J Raisch","year":"1998","unstructured":"Raisch, J., O\u2019Young, S.D.: Discrete approximation and supervisory control of continuous systems. IEEE Trans. Autom. Control 43(4), 569\u2013573 (1998)","journal-title":"IEEE Trans. Autom. Control"},{"issue":"1","key":"341_CR35","doi-asserted-by":"publisher","first-page":"206","DOI":"10.1137\/0325013","volume":"25","author":"P Ramadge","year":"1987","unstructured":"Ramadge, P., Wonham, W.: Supervisory control of a class of discrete event processes. SIAM J. Control Optim. 25(1), 206\u2013230 (1987)","journal-title":"SIAM J. Control Optim."},{"issue":"11","key":"341_CR36","doi-asserted-by":"publisher","first-page":"2583","DOI":"10.1109\/TAC.2011.2118950","volume":"56","author":"G Rei\u00dfig","year":"2011","unstructured":"Rei\u00dfig, G.: Computing abstractions of nonlinear systems. IEEE Trans. Autom. Control 56(11), 2583\u20132598 (2011)","journal-title":"IEEE Trans. Autom. Control"},{"issue":"4","key":"341_CR37","doi-asserted-by":"publisher","first-page":"1781","DOI":"10.1109\/TAC.2016.2593947","volume":"62","author":"G Reissig","year":"2017","unstructured":"Reissig, G., Weber, A., Rungger, M.: Feedback refinement relations for the synthesis of symbolic controllers. IEEE Trans. Autom. Control 62(4), 1781\u20131796 (2017)","journal-title":"IEEE Trans. Autom. Control"},{"key":"341_CR38","doi-asserted-by":"crossref","unstructured":"Rungger, M., Mazo, M., Tabuada, P.: Scaling up controller synthesis for linear systems and safety specifications. In: IEEE Conference on Decision and Control, pp. 7638\u20137643 (2012)","DOI":"10.1109\/CDC.2012.6426081"},{"key":"341_CR39","doi-asserted-by":"crossref","unstructured":"Rungger, M., Stursberg, O.: On-the-fly model abstraction for controller synthesis. In: American Control Conference, pp. 2645\u20132650 (2012)","DOI":"10.1109\/ACC.2012.6314891"},{"key":"341_CR40","doi-asserted-by":"crossref","unstructured":"Saoud, A., Girard, A., Fribourg, L.: Contract based design of symbolic controllers for interconnected multiperiodic sampled-data systems. In: IEEE Conference on Decision and Control, pp. 1\u20139 (2018)","DOI":"10.1109\/CDC.2018.8619099"},{"key":"341_CR41","doi-asserted-by":"publisher","first-page":"551","DOI":"10.1016\/j.automatica.2019.06.021","volume":"107","author":"A Swikir","year":"2019","unstructured":"Swikir, A., Zamani, M.: Compositional synthesis of finite abstractions for networks of systems: a small-gain approach. Automatica 107, 551\u2013561 (2019)","journal-title":"Automatica"},{"key":"341_CR42","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4419-0224-5","volume-title":"Verification and Control of Hybrid Systems\u2014A Symbolic Approach","author":"P Tabuada","year":"2009","unstructured":"Tabuada, P.: Verification and Control of Hybrid Systems\u2014A Symbolic Approach. Springer, Berlin (2009)"},{"issue":"12","key":"341_CR43","doi-asserted-by":"publisher","first-page":"1862","DOI":"10.1109\/TAC.2006.886494","volume":"51","author":"P Tabuada","year":"2006","unstructured":"Tabuada, P., Pappas, G.: Linear time logic control of discrete-time linear systems. IEEE Trans. Autom. Control 51(12), 1862\u20131877 (2006)","journal-title":"IEEE Trans. Autom. Control"},{"key":"341_CR44","doi-asserted-by":"publisher","first-page":"351","DOI":"10.1007\/978-3-642-00602-9_25","volume-title":"Hybrid Systems: Computation and Control","author":"Yuichi Tazaki","year":"2009","unstructured":"Tazaki, Y., Imura, J.: Discrete-state abstractions of nonlinear systems using multi-resolution quantizer. In: Hybrid Systems: Computation and Control, vol. 5469, pp. 351\u2013365 (2009)"},{"issue":"12","key":"341_CR45","doi-asserted-by":"publisher","first-page":"2834","DOI":"10.1109\/TAC.2010.2072530","volume":"55","author":"B Yordanov","year":"2010","unstructured":"Yordanov, B., Belta, C.: Formal analysis of discrete-time piecewise affine systems. IEEE Trans. Autom. Control 55(12), 2834\u20132840 (2010)","journal-title":"IEEE Trans. Autom. Control"},{"key":"341_CR46","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/j.automatica.2015.03.004","volume":"55","author":"M Zamani","year":"2015","unstructured":"Zamani, M., Abate, A., Girard, A.: Symbolic models for stochastic switched systems: a discretization and a discretization-free approach. Automatica 55, 183\u2013196 (2015)","journal-title":"Automatica"},{"issue":"7","key":"341_CR47","doi-asserted-by":"publisher","first-page":"1804","DOI":"10.1109\/TAC.2011.2176409","volume":"57","author":"M Zamani","year":"2012","unstructured":"Zamani, M., Pola, G., Mazo, M., Tabuada, P.: Symbolic models for nonlinear control systems without stability assumptions. IEEE Trans. Autom. Control 57(7), 1804\u20131809 (2012)","journal-title":"IEEE Trans. Autom. Control"},{"issue":"9","key":"341_CR48","doi-asserted-by":"publisher","first-page":"2184","DOI":"10.1109\/TAC.2011.2158135","volume":"56","author":"M Zamani","year":"2011","unstructured":"Zamani, M., Tabuada, P.: Backstepping design for incremental stability. IEEE Trans. Autom. Control 56(9), 2184\u20132189 (2011)","journal-title":"IEEE Trans. Autom. Control"}],"container-title":["Acta Informatica"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-019-00341-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00236-019-00341-x\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-019-00341-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,9,11]],"date-time":"2020-09-11T23:09:30Z","timestamp":1599865770000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s00236-019-00341-x"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,9,13]]},"references-count":48,"journal-issue":{"issue":"1-2","published-print":{"date-parts":[[2020,4]]}},"alternative-id":["341"],"URL":"https:\/\/doi.org\/10.1007\/s00236-019-00341-x","relation":{},"ISSN":["0001-5903","1432-0525"],"issn-type":[{"value":"0001-5903","type":"print"},{"value":"1432-0525","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,9,13]]},"assertion":[{"value":"20 December 2018","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"3 September 2019","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"13 September 2019","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}