{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T21:08:15Z","timestamp":1776373695828,"version":"3.51.2"},"reference-count":33,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2020,12,15]],"date-time":"2020-12-15T00:00:00Z","timestamp":1607990400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2020,12,15]],"date-time":"2020-12-15T00:00:00Z","timestamp":1607990400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/100009567","name":"Budapest University of Technology and Economics","doi-asserted-by":"crossref","id":[{"id":"10.13039\/100009567","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Acta Informatica"],"published-print":{"date-parts":[[2022,2]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Algorithms and protocols with time dependent behavior are often specified formally using timed automata. For practical real-time systems, besides real-valued clock variables, these specifications typically contain discrete data variables with nontrivial data flow. In this paper, we propose a configurable lazy abstraction framework for the location reachability problem of timed automata that potentially contain discrete variables. Moreover, based on our previous work, we uniformly formalize in our framework several abstraction refinement strategies for both clock and discrete variables that can be freely combined, resulting in many distinct algorithm configurations. Besides the proposed refinement strategies, the configurability of the framework allows the integration of existing efficient lazy abstraction algorithms for clock variables based on <jats:inline-formula><jats:alternatives><jats:tex-math>$${\\textit{LU}}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mi>LU<\/mml:mi>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula>-bounds. We demonstrate the applicability of the framework and the proposed refinement strategies by an empirical evaluation on a wide range of timed automata models, including ones that contain discrete variables or diagonal constraints.<\/jats:p>","DOI":"10.1007\/s00236-020-00393-4","type":"journal-article","created":{"date-parts":[[2020,12,15]],"date-time":"2020-12-15T13:35:09Z","timestamp":1608039309000},"page":"1-35","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Configurable verification of timed automata with\u00a0discrete\u00a0variables"],"prefix":"10.1007","volume":"59","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-7176-1278","authenticated-orcid":false,"given":"Tam\u00e1s","family":"T\u00f3th","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1184-2882","authenticated-orcid":false,"given":"Istv\u00e1n","family":"Majzik","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2020,12,15]]},"reference":[{"issue":"2","key":"393_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. Theor. Comput. Sci. 126(2), 183\u2013235 (1994). https:\/\/doi.org\/10.1016\/0304-3975(94)90010-8","journal-title":"Theor. Comput. Sci."},{"key":"393_CR2","unstructured":"Barrett, C., Sebastiani, R., Seshia, S.A., Tinelli, C.: Satisfiability modulo theories. In: Handbook of Satisfiability, chap.\u00a026, pp. 825\u2013885. IOS Press (2009). https:\/\/doi.org\/10.3233\/978-1-58603-929-5-825"},{"key":"393_CR3","doi-asserted-by":"crossref","unstructured":"Behrmann, G., Bouyer, P., Fleury, E., Larsen, K.G.: Static guard analysis in timed automata verification. In: TACAS 2003, LNCS, vol. 2619, pp. 254\u2013270. Springer (2003). https:\/\/doi.org\/10.1007\/3-540-36577-X_18","DOI":"10.1007\/3-540-36577-X_18"},{"key":"393_CR4","doi-asserted-by":"crossref","unstructured":"Behrmann, G., Bouyer, P., Larsen, K.G., Pel\u00e1nek, R.: Lower and upper bounds in zone based abstractions of timed automata. In: TACAS 2004, LNCS, vol. 2988, pp. 312\u2013326. Springer (2004). https:\/\/doi.org\/10.1007\/978-3-540-24730-2_25","DOI":"10.1007\/978-3-540-24730-2_25"},{"key":"393_CR5","doi-asserted-by":"crossref","unstructured":"Bengtsson, J., Yi, W.: Timed automata: semantics, algorithms and tools. In: ACPN 2003, LNCS, vol. 3098, pp. 87\u2013124. Springer (2004). https:\/\/doi.org\/10.1007\/978-3-540-27755-2_3","DOI":"10.1007\/978-3-540-27755-2_3"},{"issue":"2,3","key":"393_CR6","doi-asserted-by":"publisher","first-page":"145","DOI":"10.3233\/FI-1998-36233","volume":"36","author":"B B\u00e9rard","year":"1998","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). https:\/\/doi.org\/10.3233\/FI-1998-36233","journal-title":"Fundamenta Informaticae"},{"key":"393_CR7","doi-asserted-by":"crossref","unstructured":"Beyer, D., L\u00f6we, S.: Explicit-state software model checking based on CEGAR and interpolation. In: FASE 2013, LNCS, vol. 7793, pp. 146\u2013162. Springer (2013). https:\/\/doi.org\/10.1007\/978-3-642-37057-1_11","DOI":"10.1007\/978-3-642-37057-1_11"},{"key":"393_CR8","doi-asserted-by":"crossref","unstructured":"Bouyer, P.: Untameable timed automata! In: STACS 2003, LNCS, vol. 2607, pp. 620\u2013631. Springer (2003). https:\/\/doi.org\/10.1007\/3-540-36494-3_54","DOI":"10.1007\/3-540-36494-3_54"},{"issue":"4","key":"393_CR9","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. Combin. 10(4), 393\u2013405 (2005). https:\/\/doi.org\/10.25596\/jalc-2005-393","journal-title":"J. Autom. Lang. Combin."},{"key":"393_CR10","doi-asserted-by":"crossref","unstructured":"Bouyer, P., Laroussinie, F., Reynier, P.A.: Diagonal constraints in timed automata: forward analysis of timed systems. In: FORMATS 2005, LNCS, vol. 3829, pp. 112\u2013126. Springer (2005). https:\/\/doi.org\/10.1007\/11603009_10","DOI":"10.1007\/11603009_10"},{"key":"393_CR11","doi-asserted-by":"crossref","unstructured":"Bradley, A.R.: SAT-based model checking without unrolling. In: VMCAI 2011, LNCS, vol. 6538, pp. 70\u201387. Springer (2011). https:\/\/doi.org\/10.1007\/978-3-642-18275-4_7","DOI":"10.1007\/978-3-642-18275-4_7"},{"key":"393_CR12","unstructured":"Carioni, A., Ghilardi, S., Ranise, S.: Mcmt in the land of parametrized timed automata. In: International Verification Workshop (VERIFY-2010), pp. 47\u201364 (2010)"},{"key":"393_CR13","doi-asserted-by":"crossref","unstructured":"Cimatti, A., Griggio, A., Sebastiani, R.: Efficient interpolant generation in satisfiability modulo theories. In: TACAS 2008, LNCS, vol. 4963, pp. 397\u2013412. Springer (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_30","DOI":"10.1007\/978-3-540-78800-3_30"},{"issue":"5","key":"393_CR14","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. J. ACM 50(5), 752\u2013794 (2003). https:\/\/doi.org\/10.1145\/876638.876643","journal-title":"J. ACM"},{"key":"393_CR15","doi-asserted-by":"crossref","unstructured":"Daws, C., Tripakis, S.: Model checking of real-time reachability properties using abstractions. In: TACAS 1998, LNCS, vol. 1384, pp. 313\u2013329. Springer (1998). https:\/\/doi.org\/10.1007\/BFb0054180","DOI":"10.1007\/BFb0054180"},{"key":"393_CR16","doi-asserted-by":"crossref","unstructured":"Dierks, H., Kupferschmid, S., Larsen, K.G.: Automatic abstraction refinement for timed automata. In: FORMATS 2007, LNCS, vol. 4763, pp. 114\u2013129. Springer (2007). https:\/\/doi.org\/10.1007\/978-3-540-75454-1_10","DOI":"10.1007\/978-3-540-75454-1_10"},{"key":"393_CR17","doi-asserted-by":"crossref","unstructured":"Dill, D.L.: Timing assumptions and verification of finite-state concurrent systems. In: CAV 1989, LNCS, vol. 407, pp. 197\u2013212. Springer (1990). https:\/\/doi.org\/10.1007\/3-540-52148-8_17","DOI":"10.1007\/3-540-52148-8_17"},{"key":"393_CR18","unstructured":"Gastin, P., Mukherjee, S., Srivathsan, B.: Reachability in timed automata with diagonal constraints. In: International Conference on Concurrency Theory, LIPIcs, vol. 118, pp. 1\u201317. Dagstuhl (2018). https:\/\/doi.org\/10.4230\/LIPIcs.CONCUR.2018.28"},{"key":"393_CR19","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: Principles of Programming Languages, pp. 58\u201370. ACM (2002). https:\/\/doi.org\/10.1145\/503272.503279","DOI":"10.1145\/565816.503279"},{"key":"393_CR20","unstructured":"Herbreteau, F., Kini, D., Srivathsan, B., Walukiewicz, I.: Using non-convex approximations for efficient analysis of timed automata. In: Foundations of Software Technology and Theoretical Computer Science, LIPIcs, vol.\u00a013, pp. 78\u201389. Dagstuhl (2011). https:\/\/doi.org\/10.4230\/LIPIcs.FSTTCS.2011.78"},{"key":"393_CR21","doi-asserted-by":"crossref","unstructured":"Herbreteau, F., Srivathsan, B., Walukiewicz, I.: Better abstractions for timed automata. In: Logic in Computer Science, pp. 375\u2013384. IEEE (2012). https:\/\/doi.org\/10.1109\/LICS.2012.48","DOI":"10.1109\/LICS.2012.48"},{"key":"393_CR22","doi-asserted-by":"crossref","unstructured":"Herbreteau, F., Srivathsan, B., Walukiewicz, I.: Lazy abstractions for timed automata. In: CAV 2013, LNCS, vol. 8044, pp. 990\u20131005. Springer (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_71","DOI":"10.1007\/978-3-642-39799-8_71"},{"key":"393_CR23","doi-asserted-by":"crossref","unstructured":"Hojjat, H., R\u00fcmmer, P., Subotic, P., Yi, W.: Horn clauses for communicating timed systems. In: Horn Clauses for Verification and Synthesis, EPTCS, vol. 169, pp. 39\u201352. Open Publishing Association (2014). https:\/\/doi.org\/10.4204\/EPTCS.169.6","DOI":"10.4204\/EPTCS.169.6"},{"key":"393_CR24","doi-asserted-by":"crossref","unstructured":"Isenberg, T., Wehrheim, H.: Timed automata verification via IC3 with zones. In: ICFEM 2014, LNCS, vol. 8829, pp. 203\u2013218. Springer (2014). https:\/\/doi.org\/10.1007\/978-3-319-11737-9_14","DOI":"10.1007\/978-3-319-11737-9_14"},{"key":"393_CR25","doi-asserted-by":"crossref","unstructured":"Kindermann, R., Junttila, T., Niemel\u00e4, I.: SMT-based induction methods for timed systems. In: FORMATS 2012, LNCS, vol. 7595, pp. 171\u2013187. Springer (2012). https:\/\/doi.org\/10.1007\/978-3-642-33365-1_13","DOI":"10.1007\/978-3-642-33365-1_13"},{"key":"393_CR26","doi-asserted-by":"crossref","unstructured":"McMillan, K.L.: Interpolation and SAT-based model checking. In: CAV 2003, LNCS, vol. 2725, pp. 1\u201313. Springer (2003). https:\/\/doi.org\/10.1007\/978-3-540-45069-6_1","DOI":"10.1007\/978-3-540-45069-6_1"},{"key":"393_CR27","doi-asserted-by":"crossref","unstructured":"Morb\u00e9, G., Pigorsch, F., Scholl, C.: Fully symbolic model checking for timed automata. In: CAV 2011, LNCS, vol. 6806, pp. 616\u2013632. Springer (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_50","DOI":"10.1007\/978-3-642-22110-1_50"},{"key":"393_CR28","unstructured":"Reynier, P.A.: Diagonal constraints handled efficiently in Uppaal. Technical Report, LSV-07-02, Laboratoire Sp\u00e9cification et V\u00e9rification, ENS Cachan, France (2007)"},{"key":"393_CR29","doi-asserted-by":"crossref","unstructured":"T\u00f3th, T., Hajdu, \u00c1., V\u00f6r\u00f6s, A., Micskei, Z., Majzik, I.: Theta: A framework for abstraction refinement-based model checking. In: Formal Methods in Computer Aided Design, pp. 176\u2013179. FMCAD Inc. (2017). https:\/\/doi.org\/10.23919\/FMCAD.2017.8102257","DOI":"10.23919\/FMCAD.2017.8102257"},{"key":"393_CR30","doi-asserted-by":"crossref","unstructured":"T\u00f3th, T., Majzik, I.: Lazy reachability checking for timed automata using interpolants. In: FORMATS 2017, LNCS, vol. 10419, pp. 264\u2013280. Springer (2017). https:\/\/doi.org\/10.1007\/978-3-319-65765-3_15","DOI":"10.1007\/978-3-319-65765-3_15"},{"key":"393_CR31","doi-asserted-by":"crossref","unstructured":"T\u00f3th, T., Majzik, I.: Lazy reachability checking for timed automata with discrete variables. In: SPIN 2018, LNCS, vol. 10869, pp. 235\u2013254. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-94111-0_14","DOI":"10.1007\/978-3-319-94111-0_14"},{"key":"393_CR32","doi-asserted-by":"crossref","unstructured":"T\u00f3th, T., Majzik, I.: Supplementary material for the paper \u201cConfigurable verification of timed automata with discrete variables\u201d. Zenodo (2020). https:\/\/doi.org\/10.5281\/zenodo.3965792","DOI":"10.1007\/s00236-020-00393-4"},{"key":"393_CR33","doi-asserted-by":"crossref","unstructured":"Wang, W., Jiao, L.: Difference bound constraint abstraction for timed automata reachability checking. In: FORTE 2015, LNCS, vol. 9039, pp. 146\u2013160. Springer (2015). https:\/\/doi.org\/10.1007\/978-3-319-19195-9_10","DOI":"10.1007\/978-3-319-19195-9_10"}],"container-title":["Acta Informatica"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-020-00393-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s00236-020-00393-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-020-00393-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,2,17]],"date-time":"2022-02-17T11:10:11Z","timestamp":1645096211000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s00236-020-00393-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,12,15]]},"references-count":33,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2022,2]]}},"alternative-id":["393"],"URL":"https:\/\/doi.org\/10.1007\/s00236-020-00393-4","relation":{},"ISSN":["0001-5903","1432-0525"],"issn-type":[{"value":"0001-5903","type":"print"},{"value":"1432-0525","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020,12,15]]},"assertion":[{"value":"5 March 2019","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"27 October 2020","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"15 December 2020","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}