{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,7]],"date-time":"2026-05-07T02:44:50Z","timestamp":1778121890111,"version":"3.51.4"},"publisher-location":"Cham","reference-count":33,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030255398","type":"print"},{"value":"9783030255404","type":"electronic"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019]]},"DOI":"10.1007\/978-3-030-25540-4_3","type":"book-chapter","created":{"date-parts":[[2019,7,12]],"date-time":"2019-07-12T11:02:35Z","timestamp":1562929355000},"page":"41-59","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["Fast Algorithms for Handling Diagonal Constraints in Timed Automata"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-1313-7722","authenticated-orcid":false,"given":"Paul","family":"Gastin","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6473-3172","authenticated-orcid":false,"given":"Sayan","family":"Mukherjee","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2666-0691","authenticated-orcid":false,"given":"B.","family":"Srivathsan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2019,7,12]]},"reference":[{"issue":"2","key":"3_CR1","doi-asserted-by":"publisher","first-page":"272","DOI":"10.1016\/j.tcs.2005.11.018","volume":"354","author":"Y Abdeddaim","year":"2006","unstructured":"Abdeddaim, Y., Asarin, E., Maler, O.: Scheduling with timed automata. Theor. Comput. Sci. 354(2), 272\u2013300 (2006). \n                      https:\/\/doi.org\/10.1016\/j.tcs.2005.11.018","journal-title":"Theor. Comput. Sci."},{"issue":"2","key":"3_CR2","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. Theor. Comput. Sci. 126(2), 183\u2013235 (1994). \n                      https:\/\/doi.org\/10.1016\/0304-3975(94)90010-8","journal-title":"Theor. Comput. Sci."},{"key":"3_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"460","DOI":"10.1007\/3-540-46002-0_32","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"T Amnell","year":"2002","unstructured":"Amnell, T., Fersman, E., Mokrushin, L., Pettersson, P., Yi, W.: TIMES b\u2014 a tool for modelling and implementation of embedded systems. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol. 2280, pp. 460\u2013464. Springer, Heidelberg (2002). \n                      https:\/\/doi.org\/10.1007\/3-540-46002-0_32"},{"key":"3_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"254","DOI":"10.1007\/3-540-36577-X_18","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"G Behrmann","year":"2003","unstructured":"Behrmann, G., Bouyer, P., Fleury, E., Larsen, K.G.: Static guard analysis in timed automata verification. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 254\u2013270. Springer, Heidelberg (2003). \n                      https:\/\/doi.org\/10.1007\/3-540-36577-X_18"},{"issue":"3","key":"3_CR5","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., Pel\u00e1nek, R.: Lower and upper bounds in zone-based abstractions of timed automata. STTT 8(3), 204\u2013215 (2006). \n                      https:\/\/doi.org\/10.1007\/s10009-005-0190-0","journal-title":"STTT"},{"key":"3_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1007\/978-3-540-27755-2_3","volume-title":"Lectures on Concurrency and Petri Nets","author":"J Bengtsson","year":"2004","unstructured":"Bengtsson, J., Yi, W.: Timed automata: semantics, algorithms and tools. In: Desel, J., Reisig, W., Rozenberg, G. (eds.) ACPN 2003. LNCS, vol. 3098, pp. 87\u2013124. Springer, Heidelberg (2004). \n                      https:\/\/doi.org\/10.1007\/978-3-540-27755-2_3"},{"key":"3_CR7","doi-asserted-by":"publisher","unstructured":"B\u00e9rard, B., Petit, A., Diekert, V., Gastin, P.: Characterization of the expressive power of silent transitions in timed automata. Fundamenta Informaticae 36(2,3), 145\u2013182 (1998). \n                      https:\/\/doi.org\/10.3233\/FI-1998-36233","DOI":"10.3233\/FI-1998-36233"},{"key":"3_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"620","DOI":"10.1007\/3-540-36494-3_54","volume-title":"STACS 2003","author":"P Bouyer","year":"2003","unstructured":"Bouyer, P.: Untameable timed automata!. In: Alt, H., Habib, M. (eds.) STACS 2003. LNCS, vol. 2607, pp. 620\u2013631. Springer, Heidelberg (2003). \n                      https:\/\/doi.org\/10.1007\/3-540-36494-3_54"},{"issue":"3","key":"3_CR9","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1023\/B:FORM.0000026093.21513.31","volume":"24","author":"P Bouyer","year":"2004","unstructured":"Bouyer, P.: Forward analysis of updatable timed automata. Form. Methods Syst. Des. 24(3), 281\u2013320 (2004). \n                      https:\/\/doi.org\/10.1023\/B:FORM.0000026093.21513.31","journal-title":"Form. Methods Syst. Des."},{"issue":"4","key":"3_CR10","doi-asserted-by":"publisher","first-page":"393","DOI":"10.25596\/jalc-2005-393","volume":"10","author":"P Bouyer","year":"2005","unstructured":"Bouyer, P., Chevalier, F.: On conciseness of extensions of timed automata. J. Autom. Lang. Comb. 10(4), 393\u2013405 (2005). \n                      https:\/\/doi.org\/10.25596\/jalc-2005-393","journal-title":"J. Autom. Lang. Comb."},{"key":"3_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"513","DOI":"10.1007\/978-3-319-41528-4_28","volume-title":"Computer Aided Verification","author":"P Bouyer","year":"2016","unstructured":"Bouyer, P., Colange, M., Markey, N.: Symbolic optimal reachability in weighted timed automata. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9779, pp. 513\u2013530. Springer, Cham (2016). \n                      https:\/\/doi.org\/10.1007\/978-3-319-41528-4_28"},{"issue":"2\u20133","key":"3_CR12","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1016\/j.tcs.2004.04.003","volume":"321","author":"P Bouyer","year":"2004","unstructured":"Bouyer, P., Dufourd, C., Fleury, E., Petit, A.: Updatable timed automata. Theor. Comput. Sci. 321(2\u20133), 291\u2013345 (2004). \n                      https:\/\/doi.org\/10.1016\/j.tcs.2004.04.003","journal-title":"Theor. Comput. Sci."},{"key":"3_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"112","DOI":"10.1007\/11603009_10","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"P Bouyer","year":"2005","unstructured":"Bouyer, P., Laroussinie, F., Reynier, P.-A.: Diagonal constraints in timed automata: forward analysis of timed systems. In: Pettersson, P., Yi, W. (eds.) FORMATS 2005. LNCS, vol. 3829, pp. 112\u2013126. Springer, Heidelberg (2005). \n                      https:\/\/doi.org\/10.1007\/11603009_10"},{"key":"3_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"313","DOI":"10.1007\/BFb0054180","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"C Daws","year":"1998","unstructured":"Daws, C., Tripakis, S.: Model checking of real-time reachability properties using abstractions. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol. 1384, pp. 313\u2013329. Springer, Heidelberg (1998). \n                      https:\/\/doi.org\/10.1007\/BFb0054180"},{"key":"3_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"197","DOI":"10.1007\/3-540-52148-8_17","volume-title":"Automatic Verification Methods for Finite State Systems","author":"DL Dill","year":"1990","unstructured":"Dill, D.L.: Timing assumptions and verification of finite-state concurrent systems. In: Sifakis, J. (ed.) CAV 1989. LNCS, vol. 407, pp. 197\u2013212. Springer, Heidelberg (1990). \n                      https:\/\/doi.org\/10.1007\/3-540-52148-8_17"},{"key":"3_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/978-3-319-95582-7_9","volume-title":"Formal Methods","author":"T Ferr\u00e8re","year":"2018","unstructured":"Ferr\u00e8re, T.: The compound interest in relaxing punctuality. In: Havelund, K., Peleska, J., Roscoe, B., de Vink, E. (eds.) FM 2018. LNCS, vol. 10951, pp. 147\u2013164. Springer, Cham (2018). \n                      https:\/\/doi.org\/10.1007\/978-3-319-95582-7_9"},{"key":"3_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1007\/3-540-46002-0_6","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E Fersman","year":"2002","unstructured":"Fersman, E., Pettersson, P., Yi, W.: Timed automata with asynchronous processes: schedulability and decidability. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol. 2280, pp. 67\u201382. Springer, Heidelberg (2002). \n                      https:\/\/doi.org\/10.1007\/3-540-46002-0_6"},{"key":"3_CR18","doi-asserted-by":"publisher","unstructured":"Gastin, P., Mukherjee, S., Srivathsan, B.: Reachability in timed automata with diagonal constraints. In: Schewe, S., Zhang, L. (eds.) CONCUR 2018. Leibniz International Proceedings in Informatics (LIPIcs), vol. 118, pp. 28:1\u201328:17. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany (2018). \n                      https:\/\/doi.org\/10.4230\/LIPIcs.CONCUR.2018.28","DOI":"10.4230\/LIPIcs.CONCUR.2018.28"},{"key":"3_CR19","unstructured":"Gastin, P., Mukherjee, S., Srivathsan, B.: Fast algorithms for handling diagonal constraints in timed automata. CoRR abs\/1904.08590 (2019). \n                      http:\/\/arxiv.org\/abs\/1904.08590"},{"key":"3_CR20","doi-asserted-by":"publisher","unstructured":"Hatvani, L., David, A., Seceleanu, C., Pettersson, P.: Adaptive task automata with earliest-deadline-first scheduling. In: Proceedings of the 14th International Workshop on Automated Verification of Critical Systems (AVoCS 2014), vol. 70. Electronic Communications of the EASST (2014). \n                      https:\/\/doi.org\/10.14279\/tuj.eceasst.70.975","DOI":"10.14279\/tuj.eceasst.70.975"},{"key":"3_CR21","unstructured":"Herbreteau, F., Point, G.: TChecker, April 2019 \n                      https:\/\/github.com\/fredher\/tchecker\n                      \n                     (v02)"},{"key":"3_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"990","DOI":"10.1007\/978-3-642-39799-8_71","volume-title":"Computer Aided Verification","author":"F Herbreteau","year":"2013","unstructured":"Herbreteau, F., Srivathsan, B., Walukiewicz, I.: Lazy abstractions for timed automata. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 990\u20131005. Springer, Heidelberg (2013). \n                      https:\/\/doi.org\/10.1007\/978-3-642-39799-8_71"},{"key":"3_CR23","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1016\/j.ic.2016.07.004","volume":"251","author":"F Herbreteau","year":"2016","unstructured":"Herbreteau, F., Srivathsan, B., Walukiewicz, I.: Better abstractions for timed automata. Inf. Comput. 251, 67\u201390 (2016). \n                      https:\/\/doi.org\/10.1016\/j.ic.2016.07.004","journal-title":"Inf. Comput."},{"key":"3_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"124","DOI":"10.1007\/978-3-319-22975-1_9","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"F Herbreteau","year":"2015","unstructured":"Herbreteau, F., Tran, T.-T.: Improving search order for reachability testing in timed automata. In: Sankaranarayanan, S., Vicario, E. (eds.) FORMATS 2015. LNCS, vol. 9268, pp. 124\u2013139. Springer, Cham (2015). \n                      https:\/\/doi.org\/10.1007\/978-3-319-22975-1_9"},{"key":"3_CR25","doi-asserted-by":"publisher","unstructured":"Ho, H.: Revisiting timed logics with automata modalities. In: Proceedings of the 22nd ACM International Conference on Hybrid Systems: Computation and Control, HSCC 2019, pp. 67\u201376. ACM, New York (2019). \n                      https:\/\/doi.org\/10.1145\/3302504.3311818","DOI":"10.1145\/3302504.3311818"},{"key":"3_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"692","DOI":"10.1007\/978-3-662-46681-0_61","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"G Kant","year":"2015","unstructured":"Kant, G., Laarman, A., Meijer, J., van de Pol, J., Blom, S., van Dijk, T.: LTSmin: high-performance language-independent model checking. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 692\u2013707. Springer, Heidelberg (2015). \n                      https:\/\/doi.org\/10.1007\/978-3-662-46681-0_61"},{"key":"3_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"236","DOI":"10.1007\/978-3-540-24730-2_20","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"P Kr\u010d\u00e1l","year":"2004","unstructured":"Kr\u010d\u00e1l, P., Yi, W.: Decidable and undecidable problems in schedulability analysis using timed automata. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 236\u2013250. Springer, Heidelberg (2004). \n                      https:\/\/doi.org\/10.1007\/978-3-540-24730-2_20"},{"issue":"1\u20132","key":"3_CR28","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/s100090050010","volume":"1","author":"KG Larsen","year":"1997","unstructured":"Larsen, K.G., Pettersson, P., Yi, W.: UPPAAL in a nutshell. STTT 1(1\u20132), 134\u2013152 (1997). \n                      https:\/\/doi.org\/10.1007\/s100090050010","journal-title":"STTT"},{"issue":"4","key":"3_CR29","doi-asserted-by":"publisher","first-page":"11:1","DOI":"10.1145\/1734229.1734230","volume":"19","author":"J Ponge","year":"2010","unstructured":"Ponge, J., Benatallah, B., Casati, F., Toumani, F.: Analysis and applications of timed service protocols. ACM Trans. Softw. Eng. Methodol. 19(4), 11:1\u201311:38 (2010). \n                      https:\/\/doi.org\/10.1145\/1734229.1734230","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"key":"3_CR30","unstructured":"Reynier, P.A.: Diagonal constraints handled efficiently in UPPAAL. In: Research report LSV-07-02. Laboratoire Sp\u00e9cification et V\u00e9rification, ENS Cachan, France (2007)"},{"issue":"1","key":"3_CR31","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1007\/s10009-003-0135-4","volume":"6","author":"F Wang","year":"2004","unstructured":"Wang, F.: Efficient verification of timed automata with BDD-like data structures. Int. J. Softw. Tools Technol. Transf. 6(1), 77\u201397 (2004). \n                      https:\/\/doi.org\/10.1007\/s10009-003-0135-4","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"3_CR32","doi-asserted-by":"publisher","unstructured":"Yovine, S.: Kronos: a verification tool for real-time systems. (Kronos user\u2019s manual release 2.2). STTT 1, 123\u2013133 (1997). \n                      https:\/\/doi.org\/10.1007\/s100090050009","DOI":"10.1007\/s100090050009"},{"issue":"3","key":"3_CR33","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1016\/j.ipl.2005.05.027","volume":"96","author":"J Zhao","year":"2005","unstructured":"Zhao, J., Li, X., Zheng, G.: A quadratic-time dbm-based successor algorithm for checking timed automata. Inf. Process. Lett. 96(3), 101\u2013105 (2005). \n                      https:\/\/doi.org\/10.1016\/j.ipl.2005.05.027","journal-title":"Inf. Process. Lett."}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-25540-4_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,7,12]],"date-time":"2019-07-12T11:02:54Z","timestamp":1562929374000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-25540-4_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030255398","9783030255404"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-25540-4_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"12 July 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"New York City, NY","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"USA","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"15 July 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"18 July 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"31","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav0","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/i-cav.org\/2019\/","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":"258","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":"67","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":"0","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":"26% - 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":"9","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":"No","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}