{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,19]],"date-time":"2026-01-19T14:31:03Z","timestamp":1768833063895,"version":"3.49.0"},"reference-count":39,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2017,3,31]],"date-time":"2017-03-31T00:00:00Z","timestamp":1490918400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2017,3,31]],"date-time":"2017-03-31T00:00:00Z","timestamp":1490918400000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CNS-1239037"],"award-info":[{"award-number":["CNS-1239037"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CNS-1446298"],"award-info":[{"award-number":["CNS-1446298"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["ECCS-1553873"],"award-info":[{"award-number":["ECCS-1553873"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000185","name":"Defense Advanced Research Projects Agency","doi-asserted-by":"publisher","award":["N66001-14-1-4045"],"award-info":[{"award-number":["N66001-14-1-4045"]}],"id":[{"id":"10.13039\/100000185","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Discrete Event Dyn Syst"],"published-print":{"date-parts":[[2017,6]]},"DOI":"10.1007\/s10626-017-0243-z","type":"journal-article","created":{"date-parts":[[2017,3,31]],"date-time":"2017-03-31T17:10:36Z","timestamp":1490980236000},"page":"301-340","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":36,"title":["Augmented finite transition systems as abstractions for control synthesis"],"prefix":"10.1007","volume":"27","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-8748-6936","authenticated-orcid":false,"given":"Petter","family":"Nilsson","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Necmiye","family":"Ozay","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jun","family":"Liu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,3,31]]},"reference":[{"key":"243_CR1","unstructured":"Ahmadi AA, Majumdar A (2014) DSOS and SDSOS optimization: LP and SOCP-based alternatives to sum of squares optimization. In: Proceedings of the IEEE conference on decision and control, pp 394\u2013401"},{"key":"243_CR2","doi-asserted-by":"crossref","unstructured":"Ahmadi AA, Parrilo PA (2014) Towards scalable algorithms with formal guarantees for Lyapunov analysis of control systems via algebraic optimization","DOI":"10.1109\/CDC.2014.7039734"},{"key":"243_CR3","unstructured":"Baier C., Katoen J. (2008) Principles of model checking, MIT press"},{"issue":"Special Issue","key":"243_CR4","doi-asserted-by":"publisher","first-page":"215","DOI":"10.1109\/TAC.2007.911330","volume":"53","author":"G Batt","year":"2008","unstructured":"Batt G., Belta C., Weiss R. (2008) Temporal logic analysis of gene networks under parameter uncertainty. IEEE Trans Automatic Control 53(Special Issue):215\u2013229","journal-title":"IEEE Trans Automatic Control"},{"issue":"11","key":"243_CR5","doi-asserted-by":"publisher","first-page":"1749","DOI":"10.1109\/TAC.2006.884957","volume":"51","author":"C Belta","year":"2006","unstructured":"Belta C., Habets L. (2006) Controlling a class of nonlinear systems on rectangles. IEEE Trans Automatic Control 51(11):1749\u20131759","journal-title":"IEEE Trans Automatic Control"},{"key":"243_CR6","doi-asserted-by":"publisher","first-page":"911","DOI":"10.1016\/j.jcss.2011.08.007","volume":"78","author":"R Bloem","year":"2012","unstructured":"Bloem R, Jobstmann B, Piterman N, Pnueli A, Saar Y (2012) Synthesis of reactive (1) designs. J Comput System Sci 78:911\u2013938","journal-title":"J Comput System Sci"},{"key":"243_CR7","doi-asserted-by":"crossref","unstructured":"C\u00e1mara J, Girard A, G\u00f6ssler G (2011) Synthesis of switching controllers using approximately bisimilar multiscale abstractions. In: Proceeding of HSCC, pp 191\u2013200","DOI":"10.1145\/1967701.1967730"},{"key":"243_CR8","unstructured":"Church A (1962) Logic, arithmetic and automata. In: Proceedings of the international congress of mathematicians, pp 23\u201335"},{"key":"243_CR9","unstructured":"Clarke FH, Ledyaev YS, Stern RJ, Wolenski PR (1998) Nonsmooth analysis and control theory. Springer"},{"key":"243_CR10","doi-asserted-by":"crossref","unstructured":"Coogan S, Arcak M (2015) Efficient finite abstraction of mixed monotone systems. In: Proceedings of HSCC, pp 58\u201367","DOI":"10.1145\/2728606.2728607"},{"issue":"2","key":"243_CR11","doi-asserted-by":"publisher","first-page":"266","DOI":"10.1016\/0022-247X(76)90110-4","volume":"53","author":"A Feuer","year":"1976","unstructured":"Feuer A, Heymann M (1976) \u03a9-invariance in control systems with bounded controls. J Math Anal Appl 53(2):266\u2013276","journal-title":"J Math Anal Appl"},{"key":"243_CR12","doi-asserted-by":"crossref","unstructured":"Filippidis I, Dathathri S, Livingston SC, Ozay N, Murray RM (2016) Control design for hybrid systems with TuLiP: The temporal logic planning toolbox. In: Proceedings of MSC","DOI":"10.1109\/CCA.2016.7587949"},{"key":"243_CR13","doi-asserted-by":"publisher","first-page":"1046","DOI":"10.1109\/TAC.2011.2168874","volume":"57","author":"A Girard","year":"2012","unstructured":"Girard A, Martin S (2012) Control synthesis for constrained nonlinear systems using hybridization and robust controllers on simplices. IEEE Trans Automatic Control 57:1046\u20131051","journal-title":"IEEE Trans Automatic Control"},{"issue":"1","key":"243_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 (2010) Approximately bisimilar symbolic models for incrementally stable switched systems. IEEE Trans Automatic Control 55 (1):116\u2013126","journal-title":"IEEE Trans Automatic Control"},{"key":"243_CR15","doi-asserted-by":"crossref","unstructured":"Gol E, Ding X, Lazar M, Belta C (2012) Finite bisimulations for switched linear systems. In: Proceedings of IEEE CDC, pp 7632\u20137637","DOI":"10.1109\/CDC.2012.6426654"},{"key":"243_CR16","doi-asserted-by":"crossref","unstructured":"Gr\u00e4del E, Thomas W, Wilke T (eds.) (2002) Automata, Logics, and Infinite Games: A Guide to Current Research, Lecture Notes in Computer Science, vol. 2500. Springer","DOI":"10.1007\/3-540-36387-4"},{"issue":"7","key":"243_CR17","doi-asserted-by":"publisher","first-page":"565","DOI":"10.1016\/j.apenergy.2007.08.001","volume":"85","author":"M Gwerder","year":"2008","unstructured":"Gwerder M, Lehmann B, T\u00f6dtli J, Dorer V, Renggli F (2008) Control of thermally-activated building systems (tabs). Appl Energy 85(7):565\u2013581. doi: 10.1016\/j.apenergy.2007.08.001","journal-title":"Appl Energy"},{"key":"243_CR18","doi-asserted-by":"crossref","unstructured":"Habets L., Collins P., van Schuppen J. (2006) Reachability and control synthesis for piecewise-affine hybrid systems on simplices. IEEE Trans Automatic Control 51 (6):938\u2013948","DOI":"10.1109\/TAC.2006.876952"},{"issue":"1","key":"243_CR19","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1016\/S0167-6911(01)00164-5","volume":"45","author":"ZP Jiang","year":"2002","unstructured":"Jiang ZP, Wang Y (2002) A converse Lyapunov theorem for discrete-time systems with disturbances. Syst Control Lett 45(1):49\u201358","journal-title":"Syst Control Lett"},{"issue":"1","key":"243_CR20","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1006\/inco.2000.3000","volume":"163","author":"Y Kesten","year":"2000","unstructured":"Kesten Y, Pnueli A (2000) Verification by augmented finitary abstraction. Inf Comput 163(1):203\u2013243","journal-title":"Inf Comput"},{"issue":"1","key":"243_CR21","doi-asserted-by":"publisher","first-page":"124","DOI":"10.1137\/S0363012993259981","volume":"34","author":"Y Lin","year":"1996","unstructured":"Lin Y, Sontag ED, Wang Y (1996) A smooth converse Lyapunov theorem for robust stability. SIAM J Control Optimization 34(1):124\u2013160","journal-title":"SIAM J Control Optimization"},{"key":"243_CR22","doi-asserted-by":"crossref","unstructured":"Liu J, Ozay N, Topcu U, Murray R (2013) Synthesis of reactive switching protocols from temporal logic specifications. IEEE Trans Automatic Control","DOI":"10.1109\/TAC.2013.2246095"},{"key":"243_CR23","doi-asserted-by":"crossref","unstructured":"L\u00f6fberg J (2004) Yalmip: a toolbox for modeling and optimization in matlab. In: Proceeding of IEEE CACSD, pp 284\u2013289","DOI":"10.1109\/CACSD.2004.1393890"},{"key":"243_CR24","doi-asserted-by":"crossref","unstructured":"Mattila R, Mo Y, Murray RM (2015) An iterative abstraction algorithm for reactive correct-by-construction controller synthesis. In: Proceedings of IEEE CDC, pp 6147\u2013+6152","DOI":"10.1109\/CDC.2015.7403186"},{"key":"243_CR25","doi-asserted-by":"crossref","unstructured":"Nilsson P, Ozay N (2014) Incremental synthesis of switching protocols via abstraction refinement. In: Proceedings of CDC, pp 6246\u20136253","DOI":"10.1109\/CDC.2014.7040368"},{"key":"243_CR26","doi-asserted-by":"crossref","unstructured":"Ozay N, Liu J, Prabhakar P, Murray R (2013) Computing augmented finite transition systems to synthesize switching protocols for polynomial switched systems. American Control Conference","DOI":"10.1109\/ACC.2013.6580816"},{"issue":"2","key":"243_CR27","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1007\/s10107-003-0387-5","volume":"96","author":"P Parrilo","year":"2003","unstructured":"Parrilo P (2003) Semidefinite programming relaxations for semialgebraic problems. Math Program 96(2):293\u2013320","journal-title":"Math Program"},{"key":"243_CR28","doi-asserted-by":"crossref","unstructured":"Piterman N, Pnueli A (2006) Faster solutions of rabin and streett games. In: Proceedings of IEEE LICS, pp 275\u2013284","DOI":"10.1109\/LICS.2006.23"},{"key":"243_CR29","unstructured":"Piterman N, Pnueli A, Sa\u2019ar Y (2006) Synthesis of reactive (1) designs. In: Proceedings of VMCAI, pp 364\u2013380"},{"key":"243_CR30","doi-asserted-by":"crossref","unstructured":"Pnueli A, Rosner R (1989) On the synthesis of an asynchronous reactive module. In: Proceedings of ICALP, pp 652\u2013671","DOI":"10.1007\/BFb0035790"},{"key":"243_CR31","doi-asserted-by":"crossref","unstructured":"Roman\u00ed J, de Gracia A, Cabeza LF (2016) Simulation and control of thermally activated building systems (TABS). Energy & Buildings 127:22\u201342","DOI":"10.1016\/j.enbuild.2016.05.057"},{"issue":"3","key":"243_CR32","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1080\/19401493.2012.680497","volume":"6","author":"M Sourbron","year":"2013","unstructured":"Sourbron M, Verhelst C, Helsen L (2013) Building models for model predictive control of office buildings with concrete core activation. J Build Perform Simul 6(3):175\u2013198","journal-title":"J Build Perform Simul"},{"key":"243_CR33","doi-asserted-by":"crossref","unstructured":"Sun F, Ozay N, Wolff EM, Liu J, Murray RM (2014) Efficient control synthesis for augmented finite transition systems with an application to switching protocols. In: Proceedings of ACC","DOI":"10.1109\/ACC.2014.6859428"},{"key":"243_CR34","doi-asserted-by":"crossref","unstructured":"Svorenova M, Kretinsky J, Chmelik M, Chatterjee K, Cerna I, Belta C (2015) Temporal logic control for stochastic linear systems using abstraction refinement of probabilistic games. In: Proceedings of HSCC, pp 259\u2013268","DOI":"10.1145\/2728606.2728608"},{"key":"243_CR35","doi-asserted-by":"crossref","unstructured":"Tabuada P (2009) Verification and control of hybrid systems: a symbolic approach. Springer","DOI":"10.1007\/978-1-4419-0224-5"},{"key":"243_CR36","doi-asserted-by":"crossref","unstructured":"Walter W, Thompson R (1998) Ordinary differential equations, 1 edn. Springer","DOI":"10.1007\/978-1-4612-0601-9_1"},{"key":"243_CR37","doi-asserted-by":"crossref","unstructured":"Wolff E, Topcu U, Murray R (2013) Efficient reactive controller synthesis for a fragment of linear temporal logic. In: Proceedings of IEEE ICRA, pp. 5033\u20135040","DOI":"10.1109\/ICRA.2013.6631296"},{"key":"243_CR38","doi-asserted-by":"crossref","unstructured":"Yang L, Ozay N, Karnik A (2016) Synthesis of fault tolerant switching protocols for vehicle engine thermal management. In: Proceedings of ACC, pp 4213\u20134220","DOI":"10.1109\/ACC.2016.7525584"},{"issue":"6","key":"243_CR39","doi-asserted-by":"publisher","first-page":"1491","DOI":"10.1109\/TAC.2011.2178328","volume":"57","author":"B Yordanov","year":"2012","unstructured":"Yordanov B, Tumova J, Cerna I, Barnat J, Belta C (2012) Temporal logic control of discrete-time piecewise affine systems. IEEE Trans Automatic Control 57(6):1491\u20131504","journal-title":"IEEE Trans Automatic Control"}],"container-title":["Discrete Event Dynamic Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10626-017-0243-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10626-017-0243-z\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10626-017-0243-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,7,27]],"date-time":"2022-07-27T03:05:47Z","timestamp":1658891147000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10626-017-0243-z"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,3,31]]},"references-count":39,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2017,6]]}},"alternative-id":["243"],"URL":"https:\/\/doi.org\/10.1007\/s10626-017-0243-z","relation":{},"ISSN":["0924-6703","1573-7594"],"issn-type":[{"value":"0924-6703","type":"print"},{"value":"1573-7594","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,3,31]]},"assertion":[{"value":"19 February 2016","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"9 March 2017","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"31 March 2017","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}