{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T09:59:06Z","timestamp":1776333546917,"version":"3.51.2"},"publisher-location":"Cham","reference-count":39,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031377051","type":"print"},{"value":"9783031377068","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,7,17]],"date-time":"2023-07-17T00:00:00Z","timestamp":1689552000000},"content-version":"vor","delay-in-days":197,"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>In this paper, we consider a model of <jats:italic>generalized timed automata<\/jats:italic> (GTA) with two kinds of clocks, <jats:italic>history<\/jats:italic> and <jats:italic>future<\/jats:italic>, that can express many timed features succinctly, including timed automata, event-clock automata with and without diagonal constraints, and automata with timers.<\/jats:p><jats:p>Our main contribution is a new simulation-based zone algorithm for checking reachability in this unified model. While such algorithms are known to exist for timed automata, and have recently been shown for event-clock automata without diagonal constraints, this is the first result that can handle event-clock automata with diagonal constraints and automata with timers. We also provide a prototype implementation for our model and show experimental results on several benchmarks. To the best of our knowledge, this is the first effective implementation not just for our unified model, but even just for automata with timers or for event-clock automata (with predicting clocks) without going through a costly translation via timed automata. Last but not least, beyond being interesting in their own right, generalized timed automata can be used for model-checking event-clock specifications over timed automata models.<\/jats:p>","DOI":"10.1007\/978-3-031-37706-8_14","type":"book-chapter","created":{"date-parts":[[2023,7,16]],"date-time":"2023-07-16T10:01:21Z","timestamp":1689501681000},"page":"266-288","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["A Unified Model for\u00a0Real-Time Systems: Symbolic Techniques and\u00a0Implementation"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-2471-5997","authenticated-orcid":false,"given":"S.","family":"Akshay","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1313-7722","authenticated-orcid":false,"given":"Paul","family":"Gastin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1634-5893","authenticated-orcid":false,"given":"R.","family":"Govind","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1884-7894","authenticated-orcid":false,"given":"Aniruddha R.","family":"Joshi","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":[[2023,7,17]]},"reference":[{"issue":"3","key":"14_CR1","doi-asserted-by":"publisher","first-page":"262","DOI":"10.1007\/s10703-012-0179-8","volume":"42","author":"S Akshay","year":"2013","unstructured":"Akshay, S., Bollig, B., Gastin, P.: Event clock message passing automata: a logical characterization and an emptiness checking algorithm. Formal Methods Syst. Des. 42(3), 262\u2013300 (2013)","journal-title":"Formal Methods Syst. Des."},{"key":"14_CR2","doi-asserted-by":"crossref","unstructured":"Akshay, S., Gastin, P., Govind, R., Joshi, A.R., Srivathsan, B.: A unified model for real-time systems: Symbolic techniques and implementation. CoRR abs\/2305.17824 (2023)","DOI":"10.1007\/978-3-031-37706-8_14"},{"key":"14_CR3","unstructured":"Akshay, S., Gastin, P., Govind, R., Srivathsan, B.: Simulations for event-clock automata. In: CONCUR. LIPIcs, vol. 243, pp. 13:1\u201313:18 (2022)"},{"key":"14_CR4","unstructured":"Akshay, S., Gastin, P., Govind, R., Srivathsan, B.: Simulations for event-clock automata. CoRR abs\/2207.02633 (2022)"},{"key":"14_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"619","DOI":"10.1007\/978-3-030-81685-8_30","volume-title":"Computer Aided Verification","author":"S Akshay","year":"2021","unstructured":"Akshay, S., Gastin, P., Prakash, K.R.: Fast zone-based algorithms for reachability in pushdown timed automata. In: Silva, A., Leino, K.R.M. (eds.) CAV 2021. LNCS, vol. 12759, pp. 619\u2013642. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-81685-8_30"},{"key":"14_CR6","unstructured":"Alur, R.: Techniques for automatic verification of real-time systems. Ph.D. thesis, Stanford University (1991)"},{"key":"14_CR7","doi-asserted-by":"crossref","unstructured":"Alur, R., Courcoubetis, C., Henzinger, T.A., Ho, P.: Hybrid automata: An algorithmic approach to the specification and verification of hybrid systems. In: Hybrid Systems, pp. 209\u2013229 (1992)","DOI":"10.1007\/3-540-57318-6_30"},{"key":"14_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"322","DOI":"10.1007\/BFb0032042","volume-title":"Automata, Languages and Programming","author":"R Alur","year":"1990","unstructured":"Alur, R., Dill, D.: Automata for modeling real-time systems. In: Paterson, M.S. (ed.) ICALP 1990. LNCS, vol. 443, pp. 322\u2013335. Springer, Heidelberg (1990). https:\/\/doi.org\/10.1007\/BFb0032042"},{"key":"14_CR9","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. Theoret. Comput. Sci. 126, 183\u2013235 (1994)","journal-title":"Theoret. Comput. Sci."},{"issue":"1\u20132","key":"14_CR10","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1016\/S0304-3975(97)00173-4","volume":"211","author":"R Alur","year":"1999","unstructured":"Alur, R., Fix, L., Henzinger, T.A.: Event-clock automata: a determinizable class of timed automata. Theor. Comput. Sci. 211(1\u20132), 253\u2013273 (1999)","journal-title":"Theor. Comput. Sci."},{"key":"14_CR11","doi-asserted-by":"crossref","unstructured":"de\u00a0Bakker, J.W., Huizing, C., de\u00a0Roever, W.P., Rozenberg, G.: Real-Time: Theory in Practice: REX Workshop, Mook, The Netherlands. Proceedings, vol.\u00a0600 (1992)","DOI":"10.1007\/BFb0031984"},{"key":"14_CR12","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). https:\/\/doi.org\/10.1007\/978-3-540-27755-2_3"},{"key":"14_CR13","doi-asserted-by":"crossref","unstructured":"Bernstein, A.J., Jr., P.K.H.: Proving real-time properties of programs with temporal logic. In: SOSP, pp. 1\u201311. ACM (1981)","DOI":"10.1145\/1067627.806585"},{"issue":"3","key":"14_CR14","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. Formal Methods Syst. Des. 24(3), 281\u2013320 (2004)","journal-title":"Formal Methods Syst. Des."},{"issue":"4","key":"14_CR15","first-page":"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)","journal-title":"J. Autom. Lang. Comb."},{"key":"14_CR16","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). https:\/\/doi.org\/10.1007\/978-3-319-41528-4_28"},{"issue":"2\u20133","key":"14_CR17","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)","journal-title":"Theor. Comput. Sci."},{"key":"14_CR18","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: FORMATS. LNCS, vol. 13465, pp. 16\u201342. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-031-15839-1_2","DOI":"10.1007\/978-3-031-15839-1_2"},{"key":"14_CR19","unstructured":"Bozzelli, L., Montanari, A., Peron, A.: Taming the complexity of timeline-based planning over dense temporal domains. In: FSTTCS. LIPIcs, vol. 150, pp. 34:1\u201334:14 (2019)"},{"key":"14_CR20","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1016\/j.tcs.2021.12.004","volume":"901","author":"L Bozzelli","year":"2022","unstructured":"Bozzelli, L., Montanari, A., Peron, A.: Complexity issues for timeline-based planning over dense time under future and minimal semantics. Theor. Comput. Sci. 901, 87\u2013113 (2022)","journal-title":"Theor. Comput. Sci."},{"key":"14_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"208","DOI":"10.1007\/BFb0020947","volume-title":"Hybrid Systems III","author":"C Daws","year":"1996","unstructured":"Daws, C., Olivero, A., Tripakis, S., Yovine, S.: The tool Kronos. In: Alur, R., Henzinger, T.A., Sontag, E.D. (eds.) HS 1995. LNCS, vol. 1066, pp. 208\u2013219. Springer, Heidelberg (1996). https:\/\/doi.org\/10.1007\/BFb0020947"},{"key":"14_CR22","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). https:\/\/doi.org\/10.1007\/3-540-52148-8_17"},{"key":"14_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"68","DOI":"10.1007\/978-3-540-30206-3_7","volume-title":"Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems","author":"D D\u2019Souza","year":"2004","unstructured":"D\u2019Souza, D., Tabareau, N.: On timed automata with input-determined guards. In: Lakhnech, Y., Yovine, S. (eds.) FORMATS\/FTRTFT -2004. LNCS, vol. 3253, pp. 68\u201383. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-30206-3_7"},{"key":"14_CR24","unstructured":"Gastin, P., Mukherjee, S., Srivathsan, B.: Reachability in timed automata with diagonal constraints. In: CONCUR. LIPIcs, vol. 118, pp. 28:1\u201328:17 (2018)"},{"key":"14_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1007\/978-3-030-25540-4_3","volume-title":"Computer Aided Verification","author":"P Gastin","year":"2019","unstructured":"Gastin, P., Mukherjee, S., Srivathsan, B.: Fast algorithms for handling diagonal constraints in timed automata. In: Dillig, I., Tasiran, S. (eds.) CAV 2019. LNCS, vol. 11561, pp. 41\u201359. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-25540-4_3"},{"key":"14_CR26","unstructured":"Gastin, P., Mukherjee, S., Srivathsan, B.: Reachability for updatable timed automata made faster and more effective. In: FSTTCS. LIPIcs, vol. 182, pp. 47:1\u201347:17 (2020)"},{"key":"14_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1007\/978-3-642-24310-3_15","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"G Geeraerts","year":"2011","unstructured":"Geeraerts, G., Raskin, J.-F., Sznajder, N.: Event clock automata: from theory to practice. In: Fahrenberg, U., Tripakis, S. (eds.) FORMATS 2011. LNCS, vol. 6919, pp. 209\u2013224. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-24310-3_15"},{"issue":"3","key":"14_CR28","doi-asserted-by":"publisher","first-page":"330","DOI":"10.1007\/s10703-014-0212-1","volume":"45","author":"G Geeraerts","year":"2014","unstructured":"Geeraerts, G., Raskin, J.-F., Sznajder, N.: On regions and zones for event-clock automata. Formal Methods Syst Design 45(3), 330\u2013380 (2014). https:\/\/doi.org\/10.1007\/s10703-014-0212-1","journal-title":"Formal Methods Syst Design"},{"key":"14_CR29","unstructured":"Herbreteau, F., Point, G.: TChecker. https:\/\/github.com\/fredher\/tchecker (v02 - April 2019)"},{"key":"14_CR30","unstructured":"ITU-TS Recommendation Z.120: Message Sequence Chart (MSC \u201999) (1999)"},{"key":"14_CR31","unstructured":"Jonsson, B., Vaandrager, F.: Learning mealy machines with timers. Tech. rep. (2018). https:\/\/sws.cs.ru.nl\/publications\/papers\/fvaan\/MMT\/"},{"key":"14_CR32","doi-asserted-by":"crossref","unstructured":"Koymans, R., Vytopil, J., de Roever, W.P.: Real-time programming and asynchronous message passing. In: PODC, pp. 187\u2013197. ACM (1983)","DOI":"10.1145\/800221.806721"},{"key":"14_CR33","unstructured":"Kurose, J.F., Ross, K.W.: Computer networking - a top-down approach featuring the internet. Addison-Wesley-Longman (2001)"},{"issue":"1","key":"14_CR34","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1016\/j.tcs.2005.07.023","volume":"345","author":"D Lugiez","year":"2005","unstructured":"Lugiez, D., Niebert, P., Zennou, S.: A partial order semantics approach to the clock explosion problem of timed automata. Theor. Comput. Sci. 345(1), 27\u201359 (2005)","journal-title":"Theor. Comput. Sci."},{"key":"14_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"188","DOI":"10.1007\/978-3-642-33365-1_14","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"M Mu\u00f1iz","year":"2012","unstructured":"Mu\u00f1iz, M., Westphal, B., Podelski, A.: Timed automata with disjoint activity. In: Jurdzi\u0144ski, M., Ni\u010dkovi\u0107, D. (eds.) FORMATS 2012. LNCS, vol. 7595, pp. 188\u2013203. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-33365-1_14"},{"issue":"3","key":"14_CR36","first-page":"247","volume":"4","author":"J Raskin","year":"1999","unstructured":"Raskin, J., Schobbens, P.: The logic of event clocks - decidability, complexity and expressiveness. J. Autom. Lang. Comb. 4(3), 247\u2013282 (1999)","journal-title":"J. Autom. Lang. Comb."},{"key":"14_CR37","unstructured":"Sorea, M.: Tempo: A model checker for event-recording automata. Tech. rep., In: Proceedings of RT-Tools\u201901 (2001)"},{"issue":"3","key":"14_CR38","doi-asserted-by":"publisher","first-page":"6","DOI":"10.1145\/3559736.3559738","volume":"9","author":"B Srivathsan","year":"2022","unstructured":"Srivathsan, B.: Reachability in timed automata. ACM SIGLOG News 9(3), 6\u201328 (2022)","journal-title":"ACM SIGLOG News"},{"issue":"1","key":"14_CR39","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1023\/A:1008734703554","volume":"18","author":"S Tripakis","year":"2001","unstructured":"Tripakis, S., Yovine, S.: Analysis of timed systems using time-abstracting bisimulations. Formal Methods Syst. Des. 18(1), 25\u201368 (2001)","journal-title":"Formal Methods Syst. Des."}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-37706-8_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,1,5]],"date-time":"2024-01-05T11:05:22Z","timestamp":1704452722000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-37706-8_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031377051","9783031377068"],"references-count":39,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-37706-8_14","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":"17 July 2023","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":"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":"17 July 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 July 2023","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"35","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/www.i-cav.org\/2023\/","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":"hotcrp","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"261","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":"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)"}}]}}