{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,11,7]],"date-time":"2026-11-07T12:08:48Z","timestamp":1794053328004,"version":"4.8.0"},"publisher-location":"Cham","reference-count":53,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031308192","type":"print"},{"value":"9783031308208","type":"electronic"}],"license":[{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2023,4,20]],"date-time":"2023-04-20T00:00:00Z","timestamp":1681948800000},"content-version":"vor","delay-in-days":109,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We present algorithms for model checking and controller synthesis of timed automata, seeing a timed automaton model as a parallel composition of a large finite-state machine and a relatively smaller timed automaton, and using compositional reasoning on this composition. We use automata learning algorithms to learn finite automata approximations of the timed automaton component, in order to reduce the problem at hand to finite-state model checking or to finite-state controller synthesis. We present an experimental evaluation of our approach.<\/jats:p>","DOI":"10.1007\/978-3-031-30820-8_21","type":"book-chapter","created":{"date-parts":[[2023,4,19]],"date-time":"2023-04-19T19:02:36Z","timestamp":1681930956000},"page":"329-349","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":9,"title":["Timed Automata Verification and Synthesis via Finite Automata Learning"],"prefix":"10.1007","author":[{"given":"Ocan","family":"Sankur","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2023,4,20]]},"reference":[{"key":"21_CR1","doi-asserted-by":"crossref","unstructured":"Rajeev Alur and David\u00a0L. Dill. A theory of timed automata. Theoretical Computer Science, 126(2):183\u2013235, 1994.","DOI":"10.1016\/0304-3975(94)90010-8"},{"key":"21_CR2","doi-asserted-by":"crossref","unstructured":"\u00c9tienne Andr\u00e9 and Shang-Wei Lin. Learning-based compositional parameter synthesis for event-recording automata. In Ahmed Bouajjani and Alexandra Silva, editors, Formal Techniques for Distributed Objects, Components, and Systems, pages 17\u201332, Cham, 2017. Springer International Publishing.","DOI":"10.1007\/978-3-319-60225-7_2"},{"key":"21_CR3","doi-asserted-by":"crossref","unstructured":"Dana Angluin. Learning regular sets from queries and counterexamples. Information and Computation, 75(2):87\u2013106, 1987.","DOI":"10.1016\/0890-5401(87)90052-6"},{"key":"21_CR4","doi-asserted-by":"crossref","unstructured":"Eugene Asarin, Oded Maler, and Amir Pnueli. Symbolic controller synthesis for discrete and timed systems. In Hybrid Systems II, volume 999 of LNCS, pages 1\u201320. Springer, 1995.","DOI":"10.1007\/3-540-60472-3_1"},{"key":"21_CR5","doi-asserted-by":"crossref","unstructured":"Gerd Behrmann, Patricia Bouyer, Kim\u00a0G. Larsen, and Radek Pelanek. Lower and upper bounds in zone-based abstractions of timed automata. Int. J. Softw. Tools Technol. Transf., 8(3):204\u2013215, June 2006.","DOI":"10.1007\/s10009-005-0190-0"},{"key":"21_CR6","doi-asserted-by":"crossref","unstructured":"Gerd Behrmann, Agnes Cougnard, Alexandre David, Emmanuel Fleury, Kim\u00a0G Larsen, and Didier Lime. Uppaal-tiga: Time for playing games! In International Conference on Computer Aided Verification, pages 121\u2013125. Springer, 2007.","DOI":"10.1007\/978-3-540-73368-3_14"},{"key":"21_CR7","unstructured":"Gerd Behrmann, Alexandre David, Kim\u00a0Guldstrand Larsen, John H\u00e5kansson, Paul Pettersson, Wang Yi, and Martijn Hendriks. UPPAAL 4.0. In Third International Conference on the Quantitative Evaluation of Systems (QEST 2006), 11-14 September 2006, Riverside, California, USA, pages 125\u2013126, 2006."},{"key":"21_CR8","doi-asserted-by":"crossref","unstructured":"V.\u00a0Bertin, E.\u00a0Closse, M.\u00a0Poize, J.\u00a0Pulou, J.\u00a0Sifakis, P.\u00a0Venier, D.\u00a0Weil, and S.\u00a0Yovine. 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), volume\u00a03, pages 2875\u20132880 vol.3, 2001.","DOI":"10.1109\/CDC.2001.980712"},{"key":"21_CR9","doi-asserted-by":"crossref","unstructured":"Dirk Beyer, Claus Lewerentz, and Andreas Noack. Rabbit: A tool for BDD-based verification of real-time systems. In Proc. 15th International Conference on Computer Aided Verification (CAV\u201903), volume 2725 of Lecture Notes in Computer Science, pages 122\u2013125. Springer, 2003.","DOI":"10.1007\/978-3-540-45069-6_13"},{"key":"21_CR10","doi-asserted-by":"crossref","unstructured":"Patricia Bouyer, Paul Gastin, Fr\u00e9d\u00e9ric Herbreteau, Ocan Sankur, and B.\u00a0Srivathsan. 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, 2022.","DOI":"10.1007\/978-3-031-15839-1_2"},{"key":"21_CR11","doi-asserted-by":"crossref","unstructured":"Romain Brenguier, Guillermo\u00a0A. P\u00e9rez, Jean-Fran\u00e7ois Raskin, and Ocan Sankur. Abssynthe: abstract synthesis from succinct safety specifications. In Krishnendu Chatterjee, R\u00fcdiger Ehlers, and Susmit Jha, editors, Proceedings 3rd Workshop on Synthesis (SYNT\u201914), volume 157 of Electronic Proceedings in Theoretical Computer Science, pages 100\u2013116. Open Publishing Association, 2014.","DOI":"10.4204\/EPTCS.157.11"},{"key":"21_CR12","doi-asserted-by":"crossref","unstructured":"Romain Brenguier, Guillermo\u00a0A. P\u00e9rez, Jean-Fran\u00e7ois Raskin, and Ocan Sankur. Compositional algorithms for succinct safety games. In Pavol \u010cern\u00fd, Viktor Kuncak, and Madhusudan Parthasarathy, editors, Proceedings Fourth Workshop on Synthesis (SYNT\u201915), San Francisco, CA, USA, 18th July 2015, volume 202 of Electronic Proceedings in Theoretical Computer Science, pages 98\u2013111. Open Publishing Association, 2016.","DOI":"10.4204\/EPTCS.202.7"},{"key":"21_CR13","doi-asserted-by":"crossref","unstructured":"Franck Cassez, Alexandre David, Emmanuel Fleury, Kim\u00a0Guldstrand Larsen, and Didier Lime. Efficient on-the-fly algorithms for the analysis of timed games. In Proc. 16th International Conference on Concurrency Theory (CONCUR\u201905), volume 3653 of Lecture Notes in Computer Science, pages 66\u201380. Springer, 2005.","DOI":"10.1007\/11539452_9"},{"key":"21_CR14","doi-asserted-by":"crossref","unstructured":"Franck Cassez, Peter\u00a0Gj\u00f8l Jensen, and Kim\u00a0Guldstrand Larsen. Verification and parameter synthesis for real-time programs using refinement of trace abstraction. Fundam. Informaticae, 178(1-2):31\u201357, 2021.","DOI":"10.3233\/FI-2021-1997"},{"key":"21_CR15","doi-asserted-by":"crossref","unstructured":"Alessandro Cimatti, Alberto Griggio, Enrico Magnago, Marco Roveri, and Stefano Tonetta. Extending nuxmv with timed transition systems and timed temporal properties. In International Conference on Computer Aided Verification, pages 376\u2013386. Springer, 2019.","DOI":"10.1007\/978-3-030-25540-4_21"},{"key":"21_CR16","doi-asserted-by":"crossref","unstructured":"Alessandro Cimatti, Alberto Griggio, Sergio Mover, and Stefano Tonetta. 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), volume 8413 of Lecture Notes in Computer Science, pages 46\u201361, 2014.","DOI":"10.1007\/978-3-642-54862-8_4"},{"key":"21_CR17","doi-asserted-by":"crossref","unstructured":"Edmund Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, and Helmut Veith. Counterexample-guided abstraction refinement for symbolic model checking. Journal of the ACM (JACM), 50(5):752\u2013794, 2003.","DOI":"10.1145\/876638.876643"},{"key":"21_CR18","doi-asserted-by":"crossref","unstructured":"Edmund\u00a0M Clarke, Thomas\u00a0A Henzinger, Helmut Veith, Roderick Bloem, et\u00a0al. Handbook of model checking, volume\u00a010. Springer, 2018.","DOI":"10.1007\/978-3-319-10575-8"},{"key":"21_CR19","doi-asserted-by":"crossref","unstructured":"Werner Damm, Henning Dierks, Stefan Disch, Willem Hagemann, Florian Pigorsch, Christoph Scholl, Uwe Waldmann, and Boris Wirtz. Exact and fully symbolic verification of linear hybrid automata with large discrete state spaces. Science of Computer Programming, 77(10):1122\u20131150, 2012.","DOI":"10.1016\/j.scico.2011.07.006"},{"key":"21_CR20","doi-asserted-by":"crossref","unstructured":"Luca de Alfaro and Pritam Roy. Solving games via three-valued abstraction refinement. Information and Computation, 208(6):666\u2013676, 2010. Special Issue: 18th International Conference on Concurrency Theory (CONCUR 2007).","DOI":"10.1016\/j.ic.2009.05.007"},{"key":"21_CR21","doi-asserted-by":"crossref","unstructured":"Carole Delporte-Gallet, St\u00e9phane Devismes, and Hugues Fauconnier. Robust stabilizing leader election. In Toshimitsu Masuzawa and S\u00e9bastien Tixeuil, editors, Stabilization, Safety, and Security of Distributed Systems, pages 219\u2013233, Berlin, Heidelberg, 2007. Springer Berlin Heidelberg.","DOI":"10.1007\/978-3-540-76627-8_18"},{"key":"21_CR22","doi-asserted-by":"crossref","unstructured":"Rudiger Ehlers, Daniel Fass, Michael Gerke, and Hans-Jorg Peter. Fully symbolic timed model checking using constraint matrix diagrams. In Proc. 31th IEEE Real-Time Systems Symposium (RTSS\u201910), pages 360\u2013371. IEEE Computer Society Press, 2010.","DOI":"10.1109\/RTSS.2010.36"},{"key":"21_CR23","doi-asserted-by":"crossref","unstructured":"Olga Grinchtein, Bengt Jonsson, and Martin Leucker. Learning of event-recording automata. Theoretical Computer Science, 411(47):4029\u20134054, 2010.","DOI":"10.1016\/j.tcs.2010.07.008"},{"key":"21_CR24","doi-asserted-by":"crossref","unstructured":"Matthias Heizmann, Jochen Hoenicke, and Andreas Podelski. Refinement of trace abstraction. In International Static Analysis Symposium, pages 69\u201385. Springer, 2009.","DOI":"10.1007\/978-3-642-03237-0_7"},{"key":"21_CR25","doi-asserted-by":"crossref","unstructured":"Thomas\u00a0A Henzinger, Ranjit Jhala, and Rupak Majumdar. Counterexample-guided control. In International Colloquium on Automata, Languages, and Programming, pages 886\u2013902. Springer, 2003.","DOI":"10.1007\/3-540-45061-0_69"},{"key":"21_CR26","doi-asserted-by":"crossref","unstructured":"Thomas\u00a0A. Henzinger, Rupak Majumdar, Freddy Mang, and Jean-Fran\u00e7ois Raskin. Abstract interpretation of game properties. In Jens Palsberg, editor, Static Analysis, pages 220\u2013239, Berlin, Heidelberg, 2000. Springer Berlin Heidelberg.","DOI":"10.1007\/978-3-540-45099-3_12"},{"key":"21_CR27","unstructured":"Fr\u00e9d\u00e9ric Herbreteau and G\u00e9rald Point. The TChecker tool and librairies. https:\/\/github.com\/ticktac-project\/tchecker."},{"key":"21_CR28","doi-asserted-by":"crossref","unstructured":"Malte Isberner, Falk Howar, and Bernhard Steffen. The ttt algorithm: a redundancy-free approach to active automata learning. In International Conference on Runtime Verification, pages 307\u2013322. Springer, 2014.","DOI":"10.1007\/978-3-319-11164-3_26"},{"key":"21_CR29","doi-asserted-by":"crossref","unstructured":"Malte Isberner, Falk Howar, and Bernhard Steffen. The open-source learnlib. In Daniel Kroening and Corina\u00a0S. P\u0103s\u0103reanu, editors, Computer Aided Verification, pages 487\u2013495, Cham, 2015. Springer International Publishing.","DOI":"10.1007\/978-3-319-21690-4_32"},{"key":"21_CR30","doi-asserted-by":"crossref","unstructured":"Swen Jacobs, Roderick Bloem, Romain Brenguier, R\u00fcdiger Ehlers, Timotheus Hell, Robert K\u00f6nighofer, Guillermo\u00a0A P\u00e9rez, Jean-Fran\u00e7ois Raskin, Leonid Ryzhyk, Ocan Sankur, et\u00a0al. The first reactive synthesis competition (syntcomp 2014). International journal on software tools for technology transfer, 19(3):367\u2013390, 2017.","DOI":"10.1007\/s10009-016-0416-3"},{"key":"21_CR31","unstructured":"Swen Jacobs, Guillermo\u00a0A Perez, Remco Abraham, Veronique Bruyere, Michael Cadilhac, Maximilien Colange, Charly Delfosse, Tom van Dijk, Alexandre Duret-Lutz, Peter Faymonville, et\u00a0al. The reactive synthesis competition (syntcomp): 2018-2021. arXiv preprint arXiv:2206.00251, 2022."},{"key":"21_CR32","doi-asserted-by":"crossref","unstructured":"Roland Kindermann, Tommi Junttila, and Ilkka Niemela. Modeling for symbolic analysis of safety instrumented systems with clocks. In Proc. 11th International Conference on Application of Concurrency to System Design (ACSD\u201911), pages 185\u2013194. IEEE Computer Society Press, 2011.","DOI":"10.1109\/ACSD.2011.29"},{"key":"21_CR33","unstructured":"Branislav Kusy and Sherif Abdelwahed. Ftsp protocol verification using spin. May 2006."},{"key":"21_CR34","doi-asserted-by":"crossref","unstructured":"Shang-Wei Lin, \u00c9tienne Andr\u00e9, Yang Liu, Jun Sun, and Jin\u00a0Song Dong. Learning assumptions for compositional verification of timed systems. Transactions on Software Engineering, 40(2):137\u2013153, mar 2014.","DOI":"10.1109\/TSE.2013.57"},{"key":"21_CR35","doi-asserted-by":"crossref","unstructured":"Gang Luo, G.\u00a0von Bochmann, and A.\u00a0Petrenko. Test selection based on communicating nondeterministic finite-state machines using a generalized wp-method. IEEE Transactions on Software Engineering, 20(2):149\u2013162, 1994.","DOI":"10.1109\/32.265636"},{"key":"21_CR36","doi-asserted-by":"crossref","unstructured":"Oded Maler and Irini-Eleftheria Mens. Learning regular languages over large alphabets. In Erika \u00c1brah\u00e1m and Klaus Havelund, editors, Tools and Algorithms for the Construction and Analysis of Systems, pages 485\u2013499, Berlin, Heidelberg, 2014. Springer Berlin Heidelberg.","DOI":"10.1007\/978-3-642-54862-8_41"},{"key":"21_CR37","unstructured":"Oded Maler and Irini-Eleftheria Mens. A generic algorithm for learning symbolic automata from membership queries. In Luca Aceto, Giorgio Bacci, Giovanni Bacci, Anna Ing\u00f3lfsd\u00f3ttir, Axel Legay, and Radu Mardare, editors, Models, Algorithms, Logics and Tools: Essays Dedicated to Kim Guldstrand Larsen on the Occasion of His 60th Birthday, pages 146\u2013169, Cham, 2017. Springer International Publishing."},{"key":"21_CR38","doi-asserted-by":"crossref","unstructured":"Oded Maler, Amir Pnueli, and Joseph Sifakis. On the synthesis of discrete controllers for timed systems (an extended abstract). In STACS, pages 229\u2013242, 1995.","DOI":"10.1007\/3-540-59042-0_76"},{"key":"21_CR39","doi-asserted-by":"crossref","unstructured":"Mikl\u00f3s Mar\u00f3ti, Branislav Kusy, Gyula Simon, and \u00c1kos L\u00e9deczi. The flooding time synchronization protocol. In Proceedings of the 2Nd International Conference on Embedded Networked Sensor Systems, SenSys \u201904, pages 39\u201349, New York, NY, USA, 2004. ACM.","DOI":"10.1145\/1031495.1031501"},{"key":"21_CR40","doi-asserted-by":"crossref","unstructured":"A.\u00a0I. McInnes. Model-checking the flooding time synchronization protocol. In Control and Automation, 2009. ICCA 2009. IEEE International Conference on, pages 422\u2013429, Dec 2009.","DOI":"10.1109\/ICCA.2009.5410508"},{"key":"21_CR41","doi-asserted-by":"crossref","unstructured":"Truong\u00a0Khanh Nguyen, Jun Sun, Yang Liu, Jin\u00a0Song Dong, and Yan Liu. Improved BDD-based discrete analysis of timed systems. In Proc. 20th International Symposium on Formal Methods (FM\u201912), volume 7436, pages 326\u2013340. Springer, 2012.","DOI":"10.1007\/978-3-642-32759-9_28"},{"key":"21_CR42","doi-asserted-by":"crossref","unstructured":"Corina\u00a0S P\u0103s\u0103reanu, Dimitra Giannakopoulou, Mihaela\u00a0Gheorghiu Bobaru, Jamieson\u00a0M Cobleigh, and Howard Barringer. Learning to divide and conquer: applying the L* algorithm to automate assume-guarantee reasoning. Formal Methods in System Design, 32(3):175\u2013205, 2008.","DOI":"10.1007\/s10703-008-0049-6"},{"key":"21_CR43","doi-asserted-by":"crossref","unstructured":"Hans-J\u00f6rg Peter, R\u00fcdiger Ehlers, and Robert Mattm\u00fcller. Synthia: Verification and synthesis for timed automata. In International Conference on Computer Aided Verification, pages 649\u2013655. Springer, 2011.","DOI":"10.1007\/978-3-642-22110-1_52"},{"key":"21_CR44","doi-asserted-by":"crossref","unstructured":"R.L. Rivest and R.E. Schapire. Inference of finite automata using homing sequences. Information and Computation, 103(2):299\u2013347, 1993.","DOI":"10.1006\/inco.1993.1021"},{"key":"21_CR45","doi-asserted-by":"crossref","unstructured":"Victor Roussanaly, Ocan Sankur, and Nicolas Markey. Abstraction refinement algorithms for timed automata. In Isil Dillig and Serdar Tasiran, editors, Computer Aided Verification (CAV\u201919), pages 22\u201340, Cham, 2019. Springer International Publishing.","DOI":"10.1007\/978-3-030-25540-4_2"},{"key":"21_CR46","unstructured":"Ocan Sankur. Artifact for the paper: Timed Automata Verification and Synthesis via Finite Automata Learning. https:\/\/doi.org\/10.5281\/zenodo.7487508, December 2022.Ocan Sankur. Artifact for the paper: Timed Automata Verification and Synthesis via Finite Automata Learning. https:\/\/doi.org\/10.5281\/zenodo.7487508, December 2022."},{"key":"21_CR47","doi-asserted-by":"crossref","unstructured":"Ocan Sankur and Jean-Pierre Talpin. 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, pages 23\u201340, 2017.","DOI":"10.1007\/978-3-662-54577-5_2"},{"key":"21_CR48","doi-asserted-by":"crossref","unstructured":"Sanjit\u00a0A. Seshia and Randal\u00a0E. Bryant. Unbounded, fully symbolic model checking of timed automata using boolean methods. In Warren\u00a0A. Hunt and Fabio Somenzi, editors, Computer Aided Verification, pages 154\u2013166, Berlin, Heidelberg, 2003. Springer Berlin Heidelberg.","DOI":"10.1007\/978-3-540-45069-6_16"},{"key":"21_CR49","doi-asserted-by":"crossref","unstructured":"Jun Sun, Yang Liu, Jin\u00a0Song Dong, and Jun Pang. Pat: Towards flexible verification under fairness. In Proceedings of the 21th International Conference on Computer Aided Verification (CAV\u201909), volume 5643 of Lecture Notes in Computer Science, pages 709\u2013714. Springer, 2009.","DOI":"10.1007\/978-3-642-02658-4_59"},{"key":"21_CR50","doi-asserted-by":"crossref","unstructured":"Yann Thierry-Mieg. Symbolic model-checking using ITS-tools. In Proc. 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201915), pages 231\u2013237. Springer, 2015.","DOI":"10.1007\/978-3-662-46681-0_20"},{"key":"21_CR51","doi-asserted-by":"crossref","unstructured":"Wolfgang Thomas. On the synthesis of strategies in infinite games. In Ernst\u00a0W. Mayr and Claude Puech, editors, STACS 95, pages 1\u201313, Berlin, Heidelberg, 1995. Springer Berlin Heidelberg.","DOI":"10.1007\/3-540-59042-0_57"},{"key":"21_CR52","doi-asserted-by":"crossref","unstructured":"Farn Wang. 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), volume 197 of IFIP Conference Proceedings, pages 235\u2013250. Kluwer, 2001.","DOI":"10.1007\/0-306-47003-9_15"},{"key":"21_CR53","doi-asserted-by":"crossref","unstructured":"Weifeng Wang and Li\u00a0Jiao. Trace abstraction refinement for timed automata. In Franck Cassez and Jean-Fran\u00e7ois Raskin, editors, Automated Technology for Verification and Analysis, pages 396\u2013410, Cham, 2014. Springer International Publishing.","DOI":"10.1007\/978-3-319-11936-6_28"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-30820-8_21","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,10,18]],"date-time":"2024-10-18T20:03:31Z","timestamp":1729281811000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-30820-8_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031308192","9783031308208"],"references-count":53,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-30820-8_21","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"20 April 2023","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TACAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Paris","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"France","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2023","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 April 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 April 2023","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2023\/tacas","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","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":"169","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":"56","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":"6","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","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":"11","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)"}}]}}