{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,10]],"date-time":"2026-02-10T20:43:15Z","timestamp":1770756195791,"version":"3.50.0"},"publisher-location":"Cham","reference-count":36,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032111753","type":"print"},{"value":"9783032111760","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,11,23]],"date-time":"2025-11-23T00:00:00Z","timestamp":1763856000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,11,23]],"date-time":"2025-11-23T00:00:00Z","timestamp":1763856000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"DOI":"10.1007\/978-3-032-11176-0_20","type":"book-chapter","created":{"date-parts":[[2025,11,22]],"date-time":"2025-11-22T20:11:24Z","timestamp":1763842284000},"page":"338-356","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["AP-Observation Automata for\u00a0Abstraction-Based Verification of\u00a0Continuous-Time Systems"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-5929-9014","authenticated-orcid":false,"given":"Sasinee","family":"Pruekprasert","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3009-6747","authenticated-orcid":false,"given":"Clovis","family":"Eberhart","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,11,23]]},"reference":[{"key":"20_CR1","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: 18th Annual Symposium on Foundations of Computer Science (SFCS 1977), pp. 46\u201357. IEEE (1977)","DOI":"10.1109\/SFCS.1977.32"},{"issue":"2","key":"20_CR2","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1145\/307988.307989","volume":"4","author":"C Kern","year":"1999","unstructured":"Kern, C., Greenstreet, M.R.: Formal verification in hardware design: a survey. ACM Trans. Des. Autom. Electron. Syst. (TODAES) 4(2), 123\u2013193 (1999)","journal-title":"ACM Trans. Des. Autom. Electron. Syst. (TODAES)"},{"key":"20_CR3","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: Applications of temporal logic to the specification and verification of reactive systems: a survey of current trends. In: Current Trends in Concurrency: Overviews and Tutorials, pp. 510\u2013584 (2005)","DOI":"10.1007\/BFb0027047"},{"issue":"2","key":"20_CR4","doi-asserted-by":"publisher","first-page":"163","DOI":"10.1016\/j.cosrev.2010.06.002","volume":"5","author":"KY Rozier","year":"2011","unstructured":"Rozier, K.Y.: Linear temporal logic symbolic model checking. Comput. Sci. Rev. 5(2), 163\u2013203 (2011)","journal-title":"Comput. Sci. Rev."},{"issue":"1","key":"20_CR5","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1109\/MRA.2007.339624","volume":"14","author":"C Belta","year":"2007","unstructured":"Belta, C., Bicchi, A., Egerstedt, M., Frazzoli, E., Klavins, E., Pappas, G.J.: Symbolic planning and control of robot motion [grand challenges of robotics]. IEEE Robot. Autom. Mag. 14(1), 61\u201370 (2007)","journal-title":"IEEE Robot. Autom. Mag."},{"issue":"1","key":"20_CR6","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1146\/annurev-control-053018-023717","volume":"2","author":"C Belta","year":"2019","unstructured":"Belta, C., Sadraddini, S.: Formal methods for control synthesis: an optimization perspective. Ann. Rev. Control Robot. Auton. Syst. 2(1), 115\u2013140 (2019)","journal-title":"Ann. Rev. Control Robot. Auton. Syst."},{"key":"20_CR7","doi-asserted-by":"crossref","unstructured":"Banerjee, A., Choppella, V.: Challenges and opportunities in the industrial usage controller synthesis tools: a review of LTL-based opensource tools for automated control design. Results Control Optim. 100511 (2025)","DOI":"10.1016\/j.rico.2024.100511"},{"key":"20_CR8","unstructured":"Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification. In: 1st Symposium in Logic in Computer Science (LICS). IEEE Computer Society (1986)"},{"key":"20_CR9","series-title":"IFIP Advances in Information and Communication Technology","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-0-387-34892-6_1","volume-title":"Protocol Specification, Testing and Verification XV","author":"R Gerth","year":"1996","unstructured":"Gerth, R., Peled, D., Vardi, M.Y., Wolper, P.: Simple on-the-fly automatic verification of linear temporal logic. In: Dembi\u0144ski, P., \u015aredniawa, M. (eds.) PSTV 1995. IAICT, pp. 3\u201318. Springer, Boston, MA (1996). https:\/\/doi.org\/10.1007\/978-0-387-34892-6_1"},{"key":"20_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/3-540-44585-4_6","volume-title":"Computer Aided Verification","author":"P Gastin","year":"2001","unstructured":"Gastin, P., Oddoux, D.: Fast LTL to B\u00fcchi automata translation. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 53\u201365. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-44585-4_6"},{"key":"20_CR11","unstructured":"Ogata, K., et\u00a0al.: Modern Control Engineering. Prentice Hall India (2009)"},{"key":"20_CR12","volume-title":"Nonlinear Systems","author":"HK Khalil","year":"2002","unstructured":"Khalil, H.K., Grizzle, J.W.: Nonlinear Systems, vol. 3. Prentice Hall, Upper Saddle River (2002)"},{"issue":"2","key":"20_CR13","doi-asserted-by":"publisher","first-page":"158","DOI":"10.1115\/1.1569950","volume":"125","author":"K Gu","year":"2003","unstructured":"Gu, K., Niculescu, S.-I.: Survey on recent results in the stability and control of time-delay systems. J. Dyn. Syst. Meas. Contr. 125(2), 158\u2013165 (2003)","journal-title":"J. Dyn. Syst. Meas. Contr."},{"key":"20_CR14","unstructured":"Sastry, S., Bodson, M.: Adaptive Control: Stability, Convergence and Robustness. Courier Corporation (2011)"},{"issue":"8","key":"20_CR15","doi-asserted-by":"publisher","first-page":"3861","DOI":"10.1109\/TAC.2016.2638961","volume":"62","author":"AD Ames","year":"2016","unstructured":"Ames, A.D., Xu, X., Grizzle, J.W., Tabuada, P.: Control barrier function based quadratic programs for safety critical systems. IEEE Trans. Autom. Control 62(8), 3861\u20133876 (2016)","journal-title":"IEEE Trans. Autom. Control"},{"key":"20_CR16","doi-asserted-by":"publisher","first-page":"332","DOI":"10.1007\/s10458-009-9079-8","volume":"19","author":"P Doherty","year":"2009","unstructured":"Doherty, P., Kvarnstr\u00f6m, J., Heintz, F.: A temporal logic-based planning and execution monitoring framework for unmanned aircraft systems. Auton. Agent. Multi-Agent Syst. 19, 332\u2013377 (2009)","journal-title":"Auton. Agent. Multi-Agent Syst."},{"key":"20_CR17","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1007\/s10817-017-9413-9","volume":"60","author":"S Jha","year":"2018","unstructured":"Jha, S., Raman, V., Sadigh, D., Seshia, S.A.: Safe autonomy under perception uncertainty using chance-constrained temporal logic. J. Autom. Reason. 60, 43\u201362 (2018)","journal-title":"J. Autom. Reason."},{"key":"20_CR18","doi-asserted-by":"crossref","unstructured":"Arechiga, N.: Specifying safety of autonomous vehicles in signal temporal logic. In: 2019 IEEE Intelligent Vehicles Symposium (IV), pp. 58\u201363. IEEE (2019)","DOI":"10.1109\/IVS.2019.8813875"},{"key":"20_CR19","doi-asserted-by":"publisher","unstructured":"Tabuada, P.: Approximate simulation relations and finite abstractions of quantized control systems. In: Bemporad, A., Bicchi, A., Buttazzo, G. (eds.) HSCC 2007. LNCS, vol. 4416, pp. 529\u2013542. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-71493-4_41","DOI":"10.1007\/978-3-540-71493-4_41"},{"issue":"10","key":"20_CR20","doi-asserted-by":"publisher","first-page":"2508","DOI":"10.1016\/j.automatica.2008.02.021","volume":"44","author":"G Pola","year":"2008","unstructured":"Pola, G., Girard, A., Tabuada, P.: Approximately bisimilar symbolic models for nonlinear control systems. Automatica 44(10), 2508\u20132516 (2008)","journal-title":"Automatica"},{"issue":"6","key":"20_CR21","doi-asserted-by":"publisher","first-page":"1406","DOI":"10.1109\/TAC.2008.925824","volume":"53","author":"P Tabuada","year":"2008","unstructured":"Tabuada, P.: An approximate simulation approach to symbolic control. IEEE Trans. Autom. Control 53(6), 1406\u20131418 (2008)","journal-title":"IEEE Trans. Autom. Control"},{"issue":"11","key":"20_CR22","doi-asserted-by":"publisher","first-page":"4676","DOI":"10.1109\/TAC.2019.2902643","volume":"64","author":"P-J Meyer","year":"2019","unstructured":"Meyer, P.-J., Dimarogonas, D.V.: Hierarchical decomposition of LTL synthesis problem for nonlinear control systems. IEEE Trans. Autom. Control 64(11), 4676\u20134683 (2019)","journal-title":"IEEE Trans. Autom. Control"},{"key":"20_CR23","doi-asserted-by":"crossref","unstructured":"Pruekprasert, S., Eberhart, C., Dubut, J.: Fast synthesis for symbolic self-triggered control under right-recursive LTL specifications. In: 2021 60th IEEE Conference on Decision and Control (CDC), pp. 1321\u20131328. IEEE (2021)","DOI":"10.1109\/CDC45484.2021.9683328"},{"issue":"4","key":"20_CR24","doi-asserted-by":"publisher","first-page":"2576","DOI":"10.1109\/TAC.2022.3188483","volume":"68","author":"E Macoveiciuc","year":"2022","unstructured":"Macoveiciuc, E., Reissig, G.: On-the-fly symbolic synthesis with memory reduction guarantees. IEEE Trans. Autom. Control 68(4), 2576\u20132583 (2022)","journal-title":"IEEE Trans. Autom. Control"},{"issue":"11","key":"20_CR25","doi-asserted-by":"publisher","first-page":"7630","DOI":"10.1109\/TAC.2024.3394313","volume":"69","author":"W Ren","year":"2024","unstructured":"Ren, W., Jungers, R.M., Dimarogonas, D.V.: Zonotope-based symbolic controller synthesis for linear temporal logic specifications. IEEE Trans. Autom. Control 69(11), 7630\u20137645 (2024)","journal-title":"IEEE Trans. Autom. Control"},{"key":"20_CR26","doi-asserted-by":"crossref","unstructured":"Pruekprasert, S., Eberhart, C., Dubut, J.: Symbolic self-triggered control of continuous-time non-deterministic systems without stability assumptions for 2-LTL specifications. In: 2020 16th International Conference on Control, Automation, Robotics and Vision (ICARCV), pp. 548\u2013554. IEEE (2020)","DOI":"10.1109\/ICARCV50220.2020.9305387"},{"issue":"7","key":"20_CR27","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":"2","key":"20_CR28","doi-asserted-by":"publisher","first-page":"561","DOI":"10.1109\/TAC.2019.2910947","volume":"65","author":"K Hashimoto","year":"2019","unstructured":"Hashimoto, K., Dimarogonas, D.V.: Synthesizing communication plans for reachability and safety specifications. IEEE Trans. Autom. Control 65(2), 561\u2013576 (2019)","journal-title":"IEEE Trans. Autom. Control"},{"key":"20_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1007\/3-540-57318-6_30","volume-title":"Hybrid Systems","author":"R Alur","year":"1993","unstructured":"Alur, R., Courcoubetis, C., Henzinger, T.A., Ho, P.-H.: Hybrid automata: an algorithmic approach to the specification and verification of hybrid systems. In: Grossman, R.L., Nerode, A., Ravn, A.P., Rischel, H. (eds.) HS 1991-1992. LNCS, vol. 736, pp. 209\u2013229. Springer, Heidelberg (1993). https:\/\/doi.org\/10.1007\/3-540-57318-6_30"},{"issue":"1","key":"20_CR30","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1007\/s10009-017-0458-1","volume":"21","author":"S Bak","year":"2019","unstructured":"Bak, S., Beg, O.A., Bogomolov, S., Johnson, T.T., Nguyen, L.V., Schilling, C.: Hybrid automata: from verification to implementation. Int. J. Softw. Tools Technol. Transfer 21(1), 87\u2013104 (2019)","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"20_CR31","doi-asserted-by":"crossref","unstructured":"Pruekprasert, S., Eberhart, C.: AP-observation automata for abstraction-based verification of continuous-time systems (extended version) (2025). https:\/\/arxiv.org\/abs\/2509.08343","DOI":"10.1007\/978-3-032-11176-0_20"},{"issue":"1","key":"20_CR32","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1109\/TAC.2002.806650","volume":"48","author":"J Lygeros","year":"2003","unstructured":"Lygeros, J., Johansson, K.H., Simic, S.N., Zhang, J., Sastry, S.S.: Dynamical properties of hybrid automata. IEEE Trans. Autom. Control 48(1), 2\u201317 (2003)","journal-title":"IEEE Trans. Autom. Control"},{"issue":"3","key":"20_CR33","doi-asserted-by":"publisher","first-page":"617","DOI":"10.1109\/TAC.2015.2444131","volume":"61","author":"D Panagou","year":"2015","unstructured":"Panagou, D., Stipanovi\u0107, D.M., Voulgaris, P.G.: Distributed coordination control for multi-robot networks using lyapunov-like barrier functions. IEEE Trans. Autom. Control 61(3), 617\u2013632 (2015)","journal-title":"IEEE Trans. Autom. Control"},{"key":"20_CR34","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT Press, Cambridge (2008)"},{"issue":"3","key":"20_CR35","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2597631","volume":"61","author":"K Chatterjee","year":"2014","unstructured":"Chatterjee, K., Henzinger, M.: Efficient and dynamic algorithms for alternating b\u00fcchi games and maximal end-component decomposition. J. ACM (JACM) 61(3), 1\u201340 (2014)","journal-title":"J. ACM (JACM)"},{"issue":"1\u20132","key":"20_CR36","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1016\/S0304-3975(98)00009-7","volume":"200","author":"W Zielonka","year":"1998","unstructured":"Zielonka, W.: Infinite games on finitely coloured graphs with applications to automata on infinite trees. Theor. Comput. Sci. 200(1\u20132), 135\u2013183 (1998)","journal-title":"Theor. Comput. Sci."}],"container-title":["Lecture Notes in Computer Science","Theoretical Aspects of Computing \u2013 ICTAC 2025"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-11176-0_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,2,10]],"date-time":"2026-02-10T11:09:51Z","timestamp":1770721791000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-11176-0_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,11,23]]},"ISBN":["9783032111753","9783032111760"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-11176-0_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,11,23]]},"assertion":[{"value":"23 November 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ICTAC","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Colloquium on Theoretical Aspects of Computing","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Marrakesh","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Morocco","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24 November 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28 November 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"ictac2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/ictac2025.digital-hub.sh\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}