{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,25]],"date-time":"2026-08-25T14:37:51Z","timestamp":1787668671165,"version":"build-2736575974"},"reference-count":64,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2025,6,1]],"date-time":"2025-06-01T00:00:00Z","timestamp":1748736000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,6,1]],"date-time":"2025-06-01T00:00:00Z","timestamp":1748736000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"funder":[{"name":"Agence nationale de la recherche scientifique, France","award":["ANR-22-CE48-0012"],"award-info":[{"award-number":["ANR-22-CE48-0012"]}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2025,6]]},"DOI":"10.1007\/s10817-025-09730-z","type":"journal-article","created":{"date-parts":[[2025,6,13]],"date-time":"2025-06-13T04:25:55Z","timestamp":1749788755000},"update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Timed Automata Verification and Synthesis Via Finite Automata Learning"],"prefix":"10.1007","volume":"69","author":[{"given":"Ocan","family":"Sankur","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2025,6,13]]},"reference":[{"issue":"2","key":"9730_CR1","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R Alur","year":"1994","unstructured":"Alur, R., Dill, D.L.: A theory of timed automata. Theoretical Computer Science 126(2), 183\u2013235 (1994)","journal-title":"Theoretical Computer Science"},{"issue":"3","key":"9730_CR2","doi-asserted-by":"publisher","first-page":"204","DOI":"10.1007\/s10009-005-0190-0","volume":"8","author":"G Behrmann","year":"2006","unstructured":"Behrmann, G., Bouyer, P., Larsen, K.G., Pelanek, R.: Lower and upper bounds in zone-based abstractions of timed automata. Int. J. Softw. Tools Technol. Transf. 8(3), 204\u2013215 (2006). https:\/\/doi.org\/10.1007\/s10009-005-0190-0","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"9730_CR3","doi-asserted-by":"publisher","unstructured":"Behrmann, G., David, A., Larsen, K.G., H\u00e5kansson, J., Pettersson, P., Yi, W., Hendriks, M.: UPPAAL 4.0. In: Third International Conference on the Quantitative Evaluation of Systems (QEST 2006), 11-14 September 2006, Riverside, California, USA, pp. 125\u2013126 (2006). https:\/\/doi.org\/10.1109\/QEST.2006.59","DOI":"10.1109\/QEST.2006.59"},{"key":"9730_CR4","unstructured":"Herbreteau, F., Point, G.: The TChecker tool and librairies. https:\/\/github.com\/ticktac-project\/tchecker"},{"key":"9730_CR5","doi-asserted-by":"crossref","unstructured":"Sun, J., Liu, Y., Dong, J.S., Pang, J.: Pat: Towards flexible verification under fairness. In: Proceedings of the 21th International Conference on Computer Aided Verification (CAV\u201909). Lecture Notes in Computer Science, vol. 5643, pp. 709\u2013714. Springer, Berlin Heidelberg (2009)","DOI":"10.1007\/978-3-642-02658-4_59"},{"key":"9730_CR6","doi-asserted-by":"publisher","unstructured":"Bouyer, P., Gastin, P., Herbreteau, F., Sankur, O., Srivathsan, B.: Zone-based verification of timed automata: extrapolations, simulations and what next? In: 20th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS 2022). Springer, Berlin Heidelberg (2022). https:\/\/doi.org\/10.48550\/arXiv.2207.07479","DOI":"10.48550\/arXiv.2207.07479"},{"key":"9730_CR7","doi-asserted-by":"crossref","unstructured":"Wang, F.: Symbolic verification of complex real-time systems with clock-restriction diagram. In: Proc. 21st International Conference on Formal Techniques for Networked and Distributed Systems (FORTE\u201901). IFIP Conference Proceedings, vol. 197, pp. 235\u2013250. Kluwer (2001)","DOI":"10.1007\/0-306-47003-9_15"},{"key":"9730_CR8","doi-asserted-by":"crossref","unstructured":"Beyer, D., Lewerentz, C., Noack, A.: Rabbit: A tool for BDD-based verification of real-time systems. In: Proc. 15th International Conference on Computer Aided Verification (CAV\u201903). Lecture Notes in Computer Science, vol. 2725, pp. 122\u2013125. Springer (2003)","DOI":"10.1007\/978-3-540-45069-6_13"},{"key":"9730_CR9","doi-asserted-by":"publisher","unstructured":"Ehlers, R., Fass, D., Gerke, M., Peter, H.-J.: Fully symbolic timed model checking using constraint matrix diagrams. In: Proc. 31th IEEE Real-Time Systems Symposium (RTSS\u201910), pp. 360\u2013371. IEEE Computer Society Press (2010). https:\/\/doi.org\/10.1109\/RTSS.2010.36","DOI":"10.1109\/RTSS.2010.36"},{"key":"9730_CR10","doi-asserted-by":"crossref","unstructured":"Nguyen, T.K., Sun, J., Liu, Y., Dong, J.S., Liu, Y.: Improved BDD-based discrete analysis of timed systems. In: Proc. 20th International Symposium on Formal Methods (FM\u201912), vol. 7436, pp. 326\u2013340. Springer (2012)","DOI":"10.1007\/978-3-642-32759-9_28"},{"key":"9730_CR11","doi-asserted-by":"crossref","unstructured":"Thierry-Mieg, Y.: Symbolic model-checking using ITS-tools. In: Proc. 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201915), pp. 231\u2013237 (2015). Springer","DOI":"10.1007\/978-3-662-46681-0_20"},{"key":"9730_CR12","doi-asserted-by":"crossref","unstructured":"Cimatti, A., Griggio, A., Mover, S., Tonetta, S.: IC3 modulo theories via implicit predicate abstraction. In: Proc. 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201914). Lecture Notes in Computer Science, vol. 8413, pp. 46\u201361 (2014)","DOI":"10.1007\/978-3-642-54862-8_4"},{"key":"9730_CR13","doi-asserted-by":"crossref","unstructured":"Cimatti, A., Griggio, A., Magnago, E., Roveri, M., Tonetta, S.: Extending nuxmv with timed transition systems and timed temporal properties. In: International Conference on Computer Aided Verification, pp. 376\u2013386 (2019). Springer","DOI":"10.1007\/978-3-030-25540-4_21"},{"key":"9730_CR14","doi-asserted-by":"crossref","unstructured":"Roussanaly, V., Sankur, O., Markey, N.: Abstraction refinement algorithms for timed automata. In: Dillig, I., Tasiran, S. (eds.) Computer Aided Verification (CAV\u201919), pp. 22\u201340. Springer, Cham (2019). https:\/\/link.springer.com\/chapter\/10.1007%2F978-3-030-25540-4_2","DOI":"10.1007\/978-3-030-25540-4_2"},{"key":"9730_CR15","first-page":"1","volume-title":"STACS 95","author":"W Thomas","year":"1995","unstructured":"Thomas, W.: On the synthesis of strategies in infinite games. In: Mayr, E.W., Puech, C. (eds.) STACS 95, pp. 1\u201313. Springer, Berlin, Heidelberg (1995)"},{"key":"9730_CR16","doi-asserted-by":"crossref","unstructured":"Maler, O., Pnueli, A., Sifakis, J.: On the synthesis of discrete controllers for timed systems (an extended abstract). In: STACS, pp. 229\u2013242 (1995)","DOI":"10.1007\/3-540-59042-0_76"},{"key":"9730_CR17","doi-asserted-by":"crossref","unstructured":"Asarin, E., Maler, O., Pnueli, A.: Symbolic controller synthesis for discrete and timed systems. In: Hybrid Systems II. LNCS, vol. 999, pp. 1\u201320. Springer (1995)","DOI":"10.1007\/3-540-60472-3_1"},{"key":"9730_CR18","doi-asserted-by":"crossref","unstructured":"Cassez, F., David, A., Fleury, E., Larsen, K.G., Lime, D.: Efficient on-the-fly algorithms for the analysis of timed games. In: Proc. 16th International Conference on Concurrency Theory (CONCUR\u201905). Lecture Notes in Computer Science, vol. 3653, pp. 66\u201380. Springer (2005)","DOI":"10.1007\/11539452_9"},{"key":"9730_CR19","doi-asserted-by":"crossref","unstructured":"Behrmann, G., Cougnard, A., David, A., Fleury, E., Larsen, K.G., Lime, D.: UPPAAL-Tiga: Time for playing games! In: Proc. 19th International Conference on Computer Aided Verification (CAV\u201907). Lecture Notes in Computer Science, vol. 4590, pp. 121\u2013125. Springer (2007)","DOI":"10.1007\/978-3-540-73368-3_14"},{"key":"9730_CR20","doi-asserted-by":"crossref","unstructured":"Peter, H.-J., Ehlers, R., Mattm\u00fcller, R.: Synthia: Verification and synthesis for timed automata. In: International Conference on Computer Aided Verification, pp. 649\u2013655 (2011). Springer","DOI":"10.1007\/978-3-642-22110-1_52"},{"issue":"3","key":"9730_CR21","doi-asserted-by":"publisher","first-page":"367","DOI":"10.1007\/s10009-016-0416-3","volume":"19","author":"S Jacobs","year":"2017","unstructured":"Jacobs, S., Bloem, R., Brenguier, R., Ehlers, R., Hell, T., K\u00f6nighofer, R., P\u00e9rez, G.A., Raskin, J.-F., Ryzhyk, L., Sankur, O., et al.: The first reactive synthesis competition (syntcomp 2014). International journal on software tools for technology transfer 19(3), 367\u2013390 (2017)","journal-title":"International journal on software tools for technology transfer"},{"key":"9730_CR22","doi-asserted-by":"publisher","unstructured":"Bertin, V., Closse, E., Poize, M., Pulou, J., Sifakis, J., Venier, P., Weil, D., Yovine, S.: Taxys=esterel+kronos. a tool for verifying real-time properties of embedded systems. In: Proceedings of the 40th IEEE Conference on Decision and Control (Cat. No.01CH37228), vol. 3, pp. 2875\u201328803 (2001). https:\/\/doi.org\/10.1109\/CDC.2001.980712","DOI":"10.1109\/CDC.2001.980712"},{"issue":"3","key":"9730_CR23","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1007\/s10703-008-0049-6","volume":"32","author":"CS P\u0103s\u0103reanu","year":"2008","unstructured":"P\u0103s\u0103reanu, C.S., Giannakopoulou, D., Bobaru, M.G., Cobleigh, J.M., Barringer, H.: Learning to divide and conquer: applying the L* algorithm to automate assume-guarantee reasoning. Formal Methods in System Design 32(3), 175\u2013205 (2008)","journal-title":"Formal Methods in System Design"},{"issue":"2","key":"9730_CR24","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1016\/0890-5401(87)90052-6","volume":"75","author":"D Angluin","year":"1987","unstructured":"Angluin, D.: Learning regular sets from queries and counterexamples. Information and Computation 75(2), 87\u2013106 (1987). https:\/\/doi.org\/10.1016\/0890-5401(87)90052-6","journal-title":"Information and Computation"},{"key":"9730_CR25","doi-asserted-by":"crossref","unstructured":"Isberner, M., Howar, F., Steffen, B.: The ttt algorithm: a redundancy-free approach to active automata learning. In: International Conference on Runtime Verification, pp. 307\u2013322 (2014). Springer","DOI":"10.1007\/978-3-319-11164-3_26"},{"issue":"1","key":"9730_CR26","doi-asserted-by":"publisher","first-page":"411","DOI":"10.1016\/S0304-3975(02)00334-1","volume":"300","author":"L Aceto","year":"2003","unstructured":"Aceto, L., Bouyer, P., Burgue\u00f1o, A., Larsen, K.G.: The power of reachability testing for timed automata. Theoretical Computer Science 300(1), 411\u2013475 (2003). https:\/\/doi.org\/10.1016\/S0304-3975(02)00334-1","journal-title":"Theoretical Computer Science"},{"key":"9730_CR27","doi-asserted-by":"crossref","unstructured":"Sankur, O.: Timed Automata Verification and Synthesis via Finite Automata Learning. In: TACAS 2023 - 29th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Paris, France (2023). https:\/\/hal.science\/hal-03947462","DOI":"10.1007\/978-3-031-30820-8_21"},{"issue":"2","key":"9730_CR28","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1006\/inco.1993.1021","volume":"103","author":"RL Rivest","year":"1993","unstructured":"Rivest, R.L., Schapire, R.E.: Inference of finite automata using homing sequences. Information and Computation 103(2), 299\u2013347 (1993). https:\/\/doi.org\/10.1006\/inco.1993.1021","journal-title":"Information and Computation"},{"key":"9730_CR29","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R., et al.: Handbook of Model Checking vol. 10. Springer (2018)","DOI":"10.1007\/978-3-319-10575-8"},{"issue":"2","key":"9730_CR30","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1109\/TSE.2013.57","volume":"40","author":"S-W Lin","year":"2014","unstructured":"Lin, S.-W., Andr\u00e9, \u00c9., Liu, Y., Sun, J., Dong, J.S.: Learning assumptions for compositional verification of timed systems. Transactions on Software Engineering 40(2), 137\u2013153 (2014). https:\/\/doi.org\/10.1109\/TSE.2013.57","journal-title":"Transactions on Software Engineering"},{"key":"9730_CR31","doi-asserted-by":"crossref","unstructured":"Isberner, M., Howar, F., Steffen, B.: The open-source learnlib. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) Computer Aided Verification, pp. 487\u2013495. Springer, Cham (2015)","DOI":"10.1007\/978-3-319-21690-4_32"},{"key":"9730_CR32","doi-asserted-by":"crossref","unstructured":"Cimatti, A., Griggio, A.: Software model checking via ic3. In: Madhusudan, P., Seshia, S.A. (eds.) Computer Aided Verification, pp. 277\u2013293. Springer, Berlin, Heidelberg (2012)","DOI":"10.1007\/978-3-642-31424-7_23"},{"key":"9730_CR33","doi-asserted-by":"crossref","unstructured":"Delporte-Gallet, C., Devismes, S., Fauconnier, H.: Robust stabilizing leader election. In: Masuzawa, T., Tixeuil, S. (eds.) Stabilization, Safety, and Security of Distributed Systems, pp. 219\u2013233. Springer, Berlin, Heidelberg (2007)","DOI":"10.1007\/978-3-540-76627-8_18"},{"key":"9730_CR34","doi-asserted-by":"publisher","unstructured":"Mar\u00f3ti, M., Kusy, B., Simon, G., L\u00e9deczi, A.: The flooding time synchronization protocol. In: Proceedings of the 2Nd International Conference on Embedded Networked Sensor Systems. SenSys \u201904, pp. 39\u201349. ACM, New York, NY, USA (2004). https:\/\/doi.org\/10.1145\/1031495.1031501","DOI":"10.1145\/1031495.1031501"},{"key":"9730_CR35","doi-asserted-by":"publisher","unstructured":"McInnes, A.I.: Model-checking the flooding time synchronization protocol. In: Control and Automation, 2009. ICCA 2009. IEEE International Conference On, pp. 422\u2013429 (2009). https:\/\/doi.org\/10.1109\/ICCA.2009.5410508","DOI":"10.1109\/ICCA.2009.5410508"},{"key":"9730_CR36","unstructured":"Kusy, B., Abdelwahed, S.: Ftsp protocol verification using spin (2006)"},{"key":"9730_CR37","doi-asserted-by":"publisher","unstructured":"Sankur, O., Talpin, J.: An abstraction technique for parameterized model checking of leader election protocols: Application to FTSP. In: Tools and Algorithms for the Construction and Analysis of Systems - 23rd International Conference, TACAS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings, Part I, pp. 23\u201340 (2017). https:\/\/doi.org\/10.1007\/978-3-662-54577-5_2","DOI":"10.1007\/978-3-662-54577-5_2"},{"key":"9730_CR38","unstructured":"Dierks, H.: Time, Abstraction and Heuristics - Automatic Verification and Planning of Timed Systems Using Abstraction and Heuristics. Berichte aus dem Department f\u00fcr Informatik \/ Universit\u00e4t Oldenburg \/ Fachbereich Informatik, vol. 01-06 (2006)"},{"key":"9730_CR39","doi-asserted-by":"crossref","unstructured":"Bengtsson, J., Yi, W.: Timed automata: Semantics, algorithms and tools. In: Desel, J., Reisig, W., Rozenberg, G. (eds.) Lectures on Concurrency and Petri Nets. Lecture Notes in Computer Science, vol. 2098, pp. 87\u2013124. Springer (2004)","DOI":"10.1007\/978-3-540-27755-2_3"},{"issue":"2","key":"9730_CR40","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1109\/32.265636","volume":"20","author":"G Luo","year":"1994","unstructured":"Luo, G., Bochmann, G., Petrenko, A.: Test selection based on communicating nondeterministic finite-state machines using a generalized wp-method. IEEE Transactions on Software Engineering 20(2), 149\u2013162 (1994). https:\/\/doi.org\/10.1109\/32.265636","journal-title":"IEEE Transactions on Software Engineering"},{"key":"9730_CR41","doi-asserted-by":"publisher","unstructured":"Brenguier, R., P\u00e9rez, G.A., Raskin, J.-F., Sankur, O.: Abssynthe: abstract synthesis from succinct safety specifications. In: Chatterjee, K., Ehlers, R., Jha, S. (eds.) Proceedings 3rd Workshop On Synthesis (SYNT\u201914). Electronic Proceedings in Theoretical Computer Science, vol. 157, pp. 100\u2013116. Open Publishing Association (2014). https:\/\/doi.org\/10.4204\/EPTCS.157.11 . http:\/\/arxiv.org\/abs\/1407.5961v1","DOI":"10.4204\/EPTCS.157.11"},{"key":"9730_CR42","doi-asserted-by":"crossref","unstructured":"Behrmann, G., Cougnard, A., David, A., Fleury, E., Larsen, K.G., Lime, D.: Uppaal-tiga: Time for playing games! In: International Conference on Computer Aided Verification, pp. 121\u2013125 (2007). Springer","DOI":"10.1007\/978-3-540-73368-3_14"},{"key":"9730_CR43","doi-asserted-by":"crossref","unstructured":"Valizadeh, M., Fijalkow, N., Berger, M.: Ltl learning on gpus. In: International Conference on Computer Aided Verification, pp. 209\u2013231 (2024). Springer","DOI":"10.1007\/978-3-031-65633-0_10"},{"key":"9730_CR44","doi-asserted-by":"crossref","unstructured":"Behrmann, G., Bouyer, P., Fleury, E., Larsen, K.G.: Static guard analysis in timed automata verification. In: Garavel, H., Hatcliff, J. (eds.) Proceedings of the 9th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS\u201903). Lecture Notes in Computer Science, vol. 2619, pp. 254\u2013277. Springer, Warsaw, Poland (2003). http:\/\/www.lsv.ens-cachan.fr\/Publis\/PAPERS\/PDF\/BBFL-tacas-2003.pdf","DOI":"10.1007\/3-540-36577-X_18"},{"issue":"2","key":"9730_CR45","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1006\/inco.1994.1045","volume":"111","author":"TA Henzinger","year":"1994","unstructured":"Henzinger, T.A., Nicollin, X., Sifakis, J., Yovine, S.: Symbolic model checking for real time systems. Information & Computation 111(2), 193\u2013244 (1994)","journal-title":"Information & Computation"},{"key":"9730_CR46","doi-asserted-by":"publisher","unstructured":"Brenguier, R., G\u00f6ller, S., Sankur, O.: A\u00a0comparison of succinctly represented finite-state systems. In: Koutny, M., Ulidowski, I. (eds.) Proceedings of the 23rd International Conference on Concurrency Theory (CONCUR\u201912). Lecture Notes in Computer Science, vol. 7454, pp. 147\u2013161. Springer, Newcastle, UK (2012). https:\/\/doi.org\/10.1007\/978-3-642-32940-1_12 . http:\/\/www.lsv.ens-cachan.fr\/Publis\/PAPERS\/PDF\/BGS-concur12.pdf","DOI":"10.1007\/978-3-642-32940-1_12"},{"key":"9730_CR47","doi-asserted-by":"crossref","unstructured":"Heizmann, M., Hoenicke, J., Podelski, A.: Refinement of trace abstraction. In: International Static Analysis Symposium, pp. 69\u201385 (2009). Springer","DOI":"10.1007\/978-3-642-03237-0_7"},{"key":"9730_CR48","doi-asserted-by":"crossref","unstructured":"Wang, W., Jiao, L.: Trace abstraction refinement for timed automata. In: Cassez, F., Raskin, J.-F. (eds.) Automated Technology for Verification and Analysis, pp. 396\u2013410. Springer, Cham (2014)","DOI":"10.1007\/978-3-319-11936-6_28"},{"issue":"1\u20132","key":"9730_CR49","doi-asserted-by":"publisher","first-page":"31","DOI":"10.3233\/FI-2021-1997","volume":"178","author":"F Cassez","year":"2021","unstructured":"Cassez, F., Jensen, P.G., Larsen, K.G.: Verification and parameter synthesis for real-time programs using refinement of trace abstraction. Fundam. Informaticae 178(1\u20132), 31\u201357 (2021). https:\/\/doi.org\/10.3233\/FI-2021-1997","journal-title":"Fundam. Informaticae"},{"issue":"5","key":"9730_CR50","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. Journal of the ACM (JACM) 50(5), 752\u2013794 (2003)","journal-title":"Journal of the ACM (JACM)"},{"issue":"47","key":"9730_CR51","doi-asserted-by":"publisher","first-page":"4029","DOI":"10.1016\/j.tcs.2010.07.008","volume":"411","author":"O Grinchtein","year":"2010","unstructured":"Grinchtein, O., Jonsson, B., Leucker, M.: Learning of event-recording automata. Theoretical Computer Science 411(47), 4029\u20134054 (2010). https:\/\/doi.org\/10.1016\/j.tcs.2010.07.008","journal-title":"Theoretical Computer Science"},{"key":"9730_CR52","doi-asserted-by":"crossref","unstructured":"Andr\u00e9, \u00c9., Lin, S.-W.: Learning-based compositional parameter synthesis for event-recording automata. In: Bouajjani, A., Silva, A. (eds.) Formal Techniques for Distributed Objects, Components, and Systems, pp. 17\u201332. Springer, Cham (2017)","DOI":"10.1007\/978-3-319-60225-7_2"},{"key":"9730_CR53","doi-asserted-by":"publisher","unstructured":"Kindermann, R., Junttila, T., Niemela, I.: Modeling for symbolic analysis of safety instrumented systems with clocks. In: Proc. 11th International Conference on Application of Concurrency to System Design (ACSD\u201911), pp. 185\u2013194. IEEE Computer Society Press (2011). https:\/\/doi.org\/10.1109\/ACSD.2011.29","DOI":"10.1109\/ACSD.2011.29"},{"key":"9730_CR54","doi-asserted-by":"crossref","unstructured":"Seshia, S.A., Bryant, R.E.: Unbounded, fully symbolic model checking of timed automata using boolean methods. In: Hunt, W.A., Somenzi, F. (eds.) Computer Aided Verification, pp. 154\u2013166. Springer, Berlin, Heidelberg (2003)","DOI":"10.1007\/978-3-540-45069-6_16"},{"issue":"10","key":"9730_CR55","doi-asserted-by":"publisher","first-page":"1122","DOI":"10.1016\/j.scico.2011.07.006","volume":"77","author":"W Damm","year":"2012","unstructured":"Damm, W., Dierks, H., Disch, S., Hagemann, W., Pigorsch, F., Scholl, C., Waldmann, U., Wirtz, B.: Exact and fully symbolic verification of linear hybrid automata with large discrete state spaces. Science of Computer Programming 77(10), 1122\u20131150 (2012). https:\/\/doi.org\/10.1016\/j.scico.2011.07.006","journal-title":"Science of Computer Programming"},{"key":"9730_CR56","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Majumdar, R., Mang, F., Raskin, J.-F.: Abstract interpretation of game properties. In: Palsberg, J. (ed.) Static Analysis, pp. 220\u2013239. Springer, Berlin, Heidelberg (2000)","DOI":"10.1007\/978-3-540-45099-3_12"},{"key":"9730_CR57","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R.: Counterexample-guided control. In: International Colloquium on Automata, Languages, and Programming, pp. 886\u2013902 (2003). Springer","DOI":"10.1007\/3-540-45061-0_69"},{"key":"9730_CR58","doi-asserted-by":"publisher","unstructured":"de Alfaro, L., Roy, P.: Solving games via three-valued abstraction refinement. Information and Computation 208(6), 666\u2013676 (2010). https:\/\/doi.org\/10.1016\/j.ic.2009.05.007. Special Issue: 18th International Conference on Concurrency Theory (CONCUR 2007)","DOI":"10.1016\/j.ic.2009.05.007"},{"key":"9730_CR59","doi-asserted-by":"publisher","unstructured":"Brenguier, R., P\u00e9rez, G.A., Raskin, J.-F., Sankur, O.: Compositional algorithms for succinct safety games. In: \u010cern\u00fd, P., Kuncak, V., Parthasarathy, M. (eds.) Proceedings Fourth Workshop on Synthesis (SYNT\u201915), San Francisco, CA, USA, 18th July 2015. Electronic Proceedings in Theoretical Computer Science, vol. 202, pp. 98\u2013111. Open Publishing Association (2016). https:\/\/doi.org\/10.4204\/EPTCS.202.7","DOI":"10.4204\/EPTCS.202.7"},{"key":"9730_CR60","unstructured":"Jacobs, S., Perez, G.A., Abraham, R., Bruyere, V., Cadilhac, M., Colange, M., Delfosse, C., Dijk, T., Duret-Lutz, A., Faymonville, P., et al.: The reactive synthesis competition (syntcomp): 2018-2021. arXiv preprint arXiv:2206.00251 (2022)"},{"key":"9730_CR61","doi-asserted-by":"crossref","unstructured":"Maler, O., Mens, I.-E.: Learning regular languages over large alphabets. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, pp. 485\u2013499. Springer, Berlin, Heidelberg (2014)","DOI":"10.1007\/978-3-642-54862-8_41"},{"key":"9730_CR62","doi-asserted-by":"publisher","unstructured":"Maler, O., Mens, I.-E.: A generic algorithm for learning symbolic automata from membership queries. In: Aceto, L., Bacci, G., Bacci, G., Ing\u00f3lfsd\u00f3ttir, A., Legay, A., Mardare, R. (eds.) Models, Algorithms, Logics and Tools: Essays Dedicated to Kim Guldstrand Larsen on the Occasion of His 60th Birthday, pp. 146\u2013169. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63121-9_8","DOI":"10.1007\/978-3-319-63121-9_8"},{"key":"9730_CR63","doi-asserted-by":"publisher","unstructured":"Sankur, O.: Automatic assume-guarantee reasoning for safety andliveness using passive learning. Preprint (2024)https:\/\/doi.org\/10.21203\/rs.3.rs-3910982\/v1","DOI":"10.21203\/rs.3.rs-3910982\/v1"},{"key":"9730_CR64","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.7487508","author":"O Sankur","year":"2022","unstructured":"Sankur, O.: Artifact for the paper: Timed Automata Verification and Synthesis via Finite Automata Learning. Zenodo (2022). https:\/\/doi.org\/10.5281\/zenodo.7487508","journal-title":"Zenodo"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-025-09730-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10817-025-09730-z\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-025-09730-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,23]],"date-time":"2025-06-23T05:04:12Z","timestamp":1750655052000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10817-025-09730-z"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,6]]},"references-count":64,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2025,6]]}},"alternative-id":["9730"],"URL":"https:\/\/doi.org\/10.1007\/s10817-025-09730-z","relation":{"has-preprint":[{"id-type":"doi","id":"10.21203\/rs.3.rs-4363303\/v1","asserted-by":"object"}]},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,6]]},"assertion":[{"value":"3 May 2024","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"13 May 2025","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"13 June 2025","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"The authors declare no competing interests.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Competing interests"}}],"article-number":"15"}}