{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T07:25:18Z","timestamp":1740122718910,"version":"3.37.3"},"reference-count":36,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2020,7,8]],"date-time":"2020-07-08T00:00:00Z","timestamp":1594166400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2020,7,8]],"date-time":"2020-07-08T00:00:00Z","timestamp":1594166400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"funder":[{"name":"Vysok\u00e9 Ucen\u00ed Technick\u00e9 v Brne","award":["FIT-S-17-4014"],"award-info":[{"award-number":["FIT-S-17-4014"]}]},{"name":"Grantov\u00e1 Agentura Cesk\u00e9 Republiky","award":["17-12465S"],"award-info":[{"award-number":["17-12465S"]}]},{"name":"Ministerstvo \u0160kolstv\u00ed, Ml\u00e1de\u017ee a Telov\u00fdchovy","award":["IT4IXS"],"award-info":[{"award-number":["IT4IXS"]}]},{"DOI":"10.13039\/501100001665","name":"Agence Nationale de la Recherche","doi-asserted-by":"crossref","award":["VECOLIB ANR-14-CE28-0018"],"award-info":[{"award-number":["VECOLIB ANR-14-CE28-0018"]}],"id":[{"id":"10.13039\/501100001665","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2020,11]]},"DOI":"10.1007\/s10703-020-00345-1","type":"journal-article","created":{"date-parts":[[2020,7,8]],"date-time":"2020-07-08T04:53:42Z","timestamp":1594184022000},"page":"137-170","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Abstraction refinement and antichains for trace inclusion of infinite state systems"],"prefix":"10.1007","volume":"55","author":[{"given":"Luk\u00e1\u0161","family":"Hol\u00edk","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Radu","family":"Iosif","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7911-0549","authenticated-orcid":false,"given":"Adam","family":"Rogalewicz","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tom\u00e1\u0161","family":"Vojnar","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2020,7,8]]},"reference":[{"key":"345_CR1","doi-asserted-by":"crossref","unstructured":"Abdulla P, Chen YF, Holik L, Mayr R, Vojnar T (2010) When simulation meets antichains. In: Proceedings of TACAS\u201910, LNCS, vol 6015. Springer, pp 158\u2013174","DOI":"10.1007\/978-3-642-12002-2_14"},{"issue":"2","key":"345_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 DL (1994) A theory of timed automata. Theor Comput Sci 126(2):183\u2013235","journal-title":"Theor Comput Sci"},{"key":"345_CR3","doi-asserted-by":"crossref","unstructured":"Bardin S, Finkel A, Leroux J, Petrucci L (2003) Fast: fast acceleration of symbolic transition systems. In: Proceedings of CAV\u201903, LNCS, vol 2725. Springer","DOI":"10.1007\/978-3-540-45069-6_12"},{"key":"345_CR4","doi-asserted-by":"crossref","unstructured":"Beyene TA, Popeea C, Rybalchenko A (2013) Solving existentially quantified horn clauses. In: Proceedings of CAV\u201913, LNCS, vol 8044. Springer","DOI":"10.1007\/978-3-642-39799-8_61"},{"key":"345_CR5","first-page":"24","volume-title":"Horn clause solvers for program verification","author":"N Bj\u00f8rner","year":"2015","unstructured":"Bj\u00f8rner N, Gurfinkel A, McMillan K, Rybalchenko A (2015) Horn clause solvers for program verification. Springer, Cham, pp 24\u201351"},{"issue":"4","key":"345_CR6","doi-asserted-by":"publisher","first-page":"27:1","DOI":"10.1145\/1970398.1970403","volume":"12","author":"M Boja\u0144czyk","year":"2011","unstructured":"Boja\u0144czyk M, David C, Muscholl A, Schwentick T, Segoufin L (2011) Two-variable logic on data words. ACM Trans Comput Logic 12(4):27:1\u201327:26","journal-title":"ACM Trans Comput Logic"},{"key":"345_CR7","doi-asserted-by":"crossref","unstructured":"Bonchi F, Pous D (2013) Checking NFA equivalence with bisimulations up to congruence. In: Proceedings of POPL\u201913. ACM","DOI":"10.1145\/2429069.2429124"},{"key":"345_CR8","doi-asserted-by":"crossref","unstructured":"Bozga M, Habermehl P, Iosif R, Konecn\u00fd F, Vojnar T (2009) Automatic verification of integer array programs. In: Proceedings of CAV\u201909, LNCS, vol 5643, pp 157\u2013172","DOI":"10.1007\/978-3-642-02658-4_15"},{"key":"345_CR9","doi-asserted-by":"crossref","unstructured":"Cimatti A, Griggio A, Schaafsma B, Sebastiani R (2013) The MathSAT5 SMT solver. In: Proceedings of TACAS, LNCS, vol 7795","DOI":"10.1007\/978-3-642-36742-7_7"},{"key":"345_CR10","unstructured":"Comon H, Dauchet M, Gilleron R, L\u00f6ding C, Jacquemard F, Lugiez D, Tison, S, Tommasi M (2007) Tree automata techniques and applications. http:\/\/www.grappa.univ-lille3.fr\/tata. Release 12 Oct 2007"},{"key":"345_CR11","doi-asserted-by":"crossref","unstructured":"Cook B, Khlaaf H, Piterman N (2015) On automation of CTL* verification for infinite-state systems. In: Proceedings of CAV\u201915, LNCS, vol 9206. Springer","DOI":"10.1007\/978-3-319-21690-4_2"},{"issue":"3","key":"345_CR12","doi-asserted-by":"publisher","first-page":"269","DOI":"10.2307\/2963594","volume":"22","author":"W Craig","year":"1957","unstructured":"Craig W (1957) Three uses of the herbrand-gentzen theorem in relating model theory and proof theory. J. Symb. Log. 22(3):269\u2013285","journal-title":"J. Symb. Log."},{"key":"345_CR13","doi-asserted-by":"crossref","unstructured":"D\u2019Antoni L, Alur R (2014) Symbolic visibly pushdown automata. In: Proceedings of CAV\u201914, LNCS, vol 8559. Springer","DOI":"10.1007\/978-3-319-08867-9_14"},{"key":"345_CR14","doi-asserted-by":"crossref","unstructured":"Decker N, Habermehl P, Leucker M, Thoma D (2014) Ordered navigation on multi-attributed data words. In: Proceedings of CONCUR\u201914, LNCS, vol 8704, pp 497\u2013511","DOI":"10.1007\/978-3-662-44584-6_34"},{"key":"345_CR15","unstructured":"Dhar A (2014) Algorithms for model-checking flat counter systems. Ph.D. thesis, Univ. Paris 7"},{"key":"345_CR16","unstructured":"Fribourg L (1998) A closed-form evaluation for extended timed automata. Tech. rep, CNRS et Ecole Normale Sup\u00e9rieure de Cachan"},{"key":"345_CR17","doi-asserted-by":"crossref","unstructured":"Grebenshchikov S, Lopes NP, Popeea C, Rybalchenko A (2012) Synthesizing software verifiers from proof rules. In: ACM SIGPLAN conference on programming language design and implementation, PLDI \u201912, Beijing, China\u2014June 11\u201316, 2012, pp 405\u2013416","DOI":"10.1145\/2345156.2254112"},{"key":"345_CR18","doi-asserted-by":"crossref","unstructured":"Habermehl P, Iosif R, Vojnar T (2008) A logic of singly indexed arrays. In: Proceedings of LPAR\u201908, LNCS, vol 5330, pp 558\u2013573","DOI":"10.1007\/978-3-540-89439-1_39"},{"key":"345_CR19","doi-asserted-by":"crossref","unstructured":"Habermehl P, Iosif R, Vojnar T (2008) What else is decidable about integer arrays? In: Proceedings of FOSSACS\u201908, LNCS, vol 4962, pp 474\u2013489","DOI":"10.1007\/978-3-540-78499-9_33"},{"key":"345_CR20","doi-asserted-by":"crossref","unstructured":"Henzinger MR, Henzinger TA, Kopke PW (1995) Computing simulations on finite and infinite graphs. In: Proceedings of the 36th annual symposium on foundations of computer science, FOCS \u201995, pp 453","DOI":"10.1109\/SFCS.1995.492576"},{"key":"345_CR21","doi-asserted-by":"crossref","unstructured":"Henzinger TA, Jhala R, Majumdar R, Sutre G (2002) Lazy abstraction. In: Proceedings of POPL\u201902. ACM","DOI":"10.1145\/503272.503279"},{"key":"345_CR22","doi-asserted-by":"crossref","unstructured":"Henzinger TA, Jhala R, Majumdar R, Sutre G (2003) Software verification with blast. In: Proceedings of 10th SPIN workshop, LNCS, vol 2648","DOI":"10.1007\/3-540-44829-2_17"},{"key":"345_CR23","first-page":"394","volume":"111","author":"TA Henzinger","year":"1992","unstructured":"Henzinger TA, Nicollin X, Sifakis J, Yovine S (1992) Symbolic model checking for real-time systems. Inf Comput 111:394\u2013406","journal-title":"Inf Comput"},{"key":"345_CR24","doi-asserted-by":"crossref","unstructured":"Iosif R, Rogalewicz A, Vojnar T (2016) Abstraction refinement and antichains for trace inclusion of infinite state systems. In: Proceedings of TACAS\u201916, LNCS, vol 9636. Springer, pp 71\u201389","DOI":"10.1007\/978-3-662-49674-9_5"},{"key":"345_CR25","doi-asserted-by":"crossref","unstructured":"Iosif R, Xu X (2018) Abstraction refinement for emptiness checking of alternating data automata. In: Proceedings of TACAS\u201918, LNCS, vol 10806. Springer, pp 93\u2013111","DOI":"10.1007\/978-3-319-89963-3_6"},{"issue":"2","key":"345_CR26","doi-asserted-by":"publisher","first-page":"329","DOI":"10.1016\/0304-3975(94)90242-9","volume":"134","author":"M Kaminski","year":"1994","unstructured":"Kaminski M, Francez N (1994) Finite-memory automata. Theor Comput Sci 134(2):329\u2013363. https:\/\/doi.org\/10.1016\/0304-3975(94)90242-9","journal-title":"Theor Comput Sci"},{"key":"345_CR27","doi-asserted-by":"crossref","unstructured":"McMillan KL (2006) Lazy abstraction with interpolants. In: Proceedings of CAV\u201906, LNCS, vol 4144. Springer","DOI":"10.1007\/11817963_14"},{"key":"345_CR28","unstructured":"McMillan KL (2011) Interpolants from z3 proofs. In: Proceedings of the international conference on formal methods in computer-aided design, FMCAD \u201911, pp 19\u201327. FMCAD Inc"},{"key":"345_CR29","unstructured":"Milner R (1971) An algebraic definition of simulation between programs. In: Proceedings of of IJCAI\u201971. Morgan Kaufmann Publishers Inc"},{"key":"345_CR30","volume-title":"Computation: finite and infinite machines","author":"M Minsky","year":"1967","unstructured":"Minsky M (1967) Computation: finite and infinite machines. Prentice-Hall, Upper Saddle River"},{"key":"345_CR31","unstructured":"Numerical Transition Systems Repository (2012). http:\/\/nts.imag.fr\/index.php\/Flata"},{"key":"345_CR32","doi-asserted-by":"crossref","unstructured":"Ouaknine J, Worrell J (2004) On the language inclusion problem for timed automata: closing a decidability gap. In: Proceedings of LICS\u201904. IEEE Computer Society","DOI":"10.21236\/ADA461167"},{"key":"345_CR33","doi-asserted-by":"crossref","unstructured":"Smrcka A, Vojnar T (2007) Verifying parametrised hardware designs via counter automata. In: HVC\u201907, pp 51\u201368","DOI":"10.1007\/978-3-540-77966-7_8"},{"key":"345_CR34","unstructured":"Tripakis S (1998) The analysis of timed systems in practice. Ph.D. thesis, Univ. Joseph Fourier, Grenoble (December)"},{"key":"345_CR35","unstructured":"Wulf MD, Doyen L, Henzinger TA, Raskin J (2006) Antichains: a new algorithm for checking universality of finite automata. In: Proceedings of CAV\u201906, LNCS, vol 4144. Springer"},{"key":"345_CR36","first-page":"1","volume":"79","author":"A Zbrzezny","year":"2007","unstructured":"Zbrzezny A, Polrola A (2007) Sat-based reachability checking for timed automata with discrete data. Fundam Inf 79:1\u201315","journal-title":"Fundam Inf"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-020-00345-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10703-020-00345-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-020-00345-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,7,8]],"date-time":"2021-07-08T00:38:59Z","timestamp":1625704739000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10703-020-00345-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,7,8]]},"references-count":36,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2020,11]]}},"alternative-id":["345"],"URL":"https:\/\/doi.org\/10.1007\/s10703-020-00345-1","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"type":"print","value":"0925-9856"},{"type":"electronic","value":"1572-8102"}],"subject":[],"published":{"date-parts":[[2020,7,8]]},"assertion":[{"value":"8 July 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}