{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,8]],"date-time":"2025-03-08T10:40:15Z","timestamp":1741430415527,"version":"3.38.0"},"reference-count":82,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2011,8,9]],"date-time":"2011-08-09T00:00:00Z","timestamp":1312848000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2012,4]]},"DOI":"10.1007\/s10009-011-0209-7","type":"journal-article","created":{"date-parts":[[2011,8,8]],"date-time":"2011-08-08T05:54:16Z","timestamp":1312782856000},"page":"119-143","source":"Crossref","is-referenced-by-count":5,"title":["Extrapolating (omega-)regular model checking"],"prefix":"10.1007","volume":"14","author":[{"given":"Axel","family":"Legay","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2011,8,9]]},"reference":[{"key":"209_CR1","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Bouajjani, A., d\u2019Orso, J.: Deciding monotonic games. In: CSL. LNCS, vol. 2803, pp. 1\u201314. Springer, Berlin (2003)","DOI":"10.1007\/978-3-540-45220-1_1"},{"key":"209_CR2","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Bouajjani, A., Jonsson, B.: On-the-fly analysis of systems with unbounded, lossy FIFO channels. In: CAV. LNCS, vol. 1427, pp. 305\u2013318. Springer, Berlin (1998)","DOI":"10.1007\/BFb0028754"},{"key":"209_CR3","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Delzanno, G., Rezine, A.: Parameterized verification of infinite-state processes with global conditions. In: CAV. LNCS, vol. 4590, pp. 145\u2013157. Springer, Berlin (2007)","DOI":"10.1007\/978-3-540-73368-3_17"},{"issue":"2","key":"209_CR4","doi-asserted-by":"crossref","first-page":"91","DOI":"10.1006\/inco.1996.0053","volume":"127","author":"P.A. Abdulla","year":"1996","unstructured":"Abdulla P.A., Jonsson B.: Verifying programs with unreliable channels. Inf. Comput. 127(2), 91\u2013101 (1996)","journal-title":"Inf. Comput."},{"key":"209_CR5","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Jonsson, B., Nilsson, M., d\u2019Orso, J.: Algorithmic improvements in regular model checking. In: CAV. LNCS, vol. 2725, pp. 236\u2013248. Springer, Berlin (2003)","DOI":"10.1007\/978-3-540-45069-6_25"},{"key":"209_CR6","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Jonsson, B., Nilsson, M., d\u2019Orso, J., Saksena, M.: Regular model checking for ltl(mso). In: CAV. LNCS, vol. 3114, pp. 348\u2013360. Springer, Berlin (2004)","DOI":"10.1007\/978-3-540-27813-9_27"},{"key":"209_CR7","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Jonsson, B., Nilsson, M., d\u2019Orso, J., Saksena, M.: Regular model checking for ltl(mso). Special Section on Regular Model Checking STTT (2010, in this volume)","DOI":"10.1007\/s10009-011-0212-z"},{"key":"209_CR8","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Jonsson, B., Rezine, A., Saksena, M.: Proving liveness by backwards reachability. In: CONCUR. LNCS, vol. 4137, pp. 95\u2013109. Springer, Berlin (2006)","DOI":"10.1007\/11817949_7"},{"key":"209_CR9","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Legay, A., Rezine, A., d\u2019Orso, J.: Simulation-based iteration of tree transducers. In: TACAS. LNCS, vol. 3440, pp. 30\u201340. Springer, Berlin (2005)","DOI":"10.1007\/978-3-540-31980-1_3"},{"key":"209_CR10","doi-asserted-by":"crossref","unstructured":"Adler, B.T., de Alfaro, L., da Silva, L.D., Faella, M., Legay, A., Raman, V., Roy, P.: Ticc: A tool for interface compatibility and composition. In: CAV. LNCS, vol. 4144, pp. 59\u201362. Springer, Berlin (2006)","DOI":"10.1007\/11817963_8"},{"issue":"1","key":"209_CR11","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/0304-3975(94)00202-T","volume":"138","author":"R. Alur","year":"1995","unstructured":"Alur R., Courcoubetis C., Halbwachs N., Henzinger T.A., Ho P., Nicollin X., Olivero A., Sifakis J., Yovine S.: The algorithmic analysis of hybrid systems. Theor. Compu. Sci. 138(1), 3\u201334 (1995)","journal-title":"Theor. Compu. Sci."},{"issue":"2","key":"209_CR12","doi-asserted-by":"crossref","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)","journal-title":"Theor. Comput. Sci."},{"issue":"2","key":"209_CR13","doi-asserted-by":"crossref","first-page":"87","DOI":"10.1016\/0890-5401(87)90052-6","volume":"75","author":"D. Angluin","year":"1987","unstructured":"Angluin D.: Learning regular sets from queries and counterexamples. Inf. Comp. 75(2), 87\u2013106 (1987)","journal-title":"Inf. Comp."},{"issue":"6","key":"209_CR14","doi-asserted-by":"crossref","first-page":"307","DOI":"10.1016\/0020-0190(86)90071-2","volume":"22","author":"K.R. Apt","year":"1986","unstructured":"Apt K.R., Kozen D.: Limits for automatic verification of finite-state concurrent systems. Inf. Process. Lett. 22(6), 307\u2013309 (1986)","journal-title":"Inf. Process. Lett."},{"key":"209_CR15","unstructured":"Arnold, A.: Finite transition systems: semantics of communicating systems. Prentice Hall International (UK) Ltd., Translator-John Plaice (1994)"},{"key":"209_CR16","doi-asserted-by":"crossref","unstructured":"Bardin, S., Finkel, A., Leroux, J.: Faster acceleration of counter automata in practice. In: TACAS. LNCS, vol. 2988, pp. 576\u2013590. Springer, Berlin (2004)","DOI":"10.1007\/978-3-540-24730-2_42"},{"key":"209_CR17","doi-asserted-by":"crossref","unstructured":"Bardin, S., Leroux, J., Point, G.: Fast extended release. In: CAV. LNCS, vol. 4144, pp. 63\u201366. Springer, Berlin (2006)","DOI":"10.1007\/11817963_9"},{"key":"209_CR18","doi-asserted-by":"crossref","unstructured":"Becker, B., Dax, C., Eisinger, J., Klaedtke F. LIRA: handling constraints of linear arithmetics over the integers and the reals. In: CAV. LNCS, vol. 4590, pp. 307\u2013310. Springer, Berlin (2007)","DOI":"10.1007\/978-3-540-73368-3_36"},{"key":"209_CR19","volume-title":"Symbolic Methods for Exploring Infinite State Spaces","author":"B. Boigelot","year":"1999","unstructured":"Boigelot B.: Symbolic Methods for Exploring Infinite State Spaces. ULG, Li\u00e8ge (1999)"},{"issue":"1\u20133","key":"209_CR20","doi-asserted-by":"crossref","first-page":"413","DOI":"10.1016\/S0304-3975(03)00314-1","volume":"309","author":"B. Boigelot","year":"2003","unstructured":"Boigelot B.: On iterating linear transformations over recognizable sets of integers. Theor. Comput. Sci. 309(1\u20133), 413\u2013468 (2003)","journal-title":"Theor. Comput. Sci."},{"key":"209_CR21","unstructured":"Boigelot, B.: Advance project: deliverables 2004. Technical report, Universit\u00e9 de Li\u00e8ge (2004)"},{"key":"209_CR22","unstructured":"Boigelot, B.: Domain-specific regular acceleration. Special Section on Regular Model Checking STTT (2010, in this volume)"},{"key":"209_CR23","doi-asserted-by":"crossref","unstructured":"Boigelot, B., Godefroid, P.: Symbolic verification of communication protocols with infinite state spaces using qdds (extended abstract). In: CAV. LNCS, vol. 1102, pp. 1\u201312. Springer, Berlin (1996)","DOI":"10.1007\/3-540-61474-5_53"},{"key":"209_CR24","doi-asserted-by":"crossref","unstructured":"Boigelot, B., Herbreteau, F.: The power of hybrid acceleration. In: CAV. LNCS, vol. 4144, pp. 438\u2013451. Springer, Berlin (2006)","DOI":"10.1007\/11817963_40"},{"key":"209_CR25","doi-asserted-by":"crossref","unstructured":"Boigelot, B., Herbreteau, F., Jodogne, S.: Hybrid acceleration using real vector automata. In: CAV. LNCS, vol. 2725, pp. 193\u2013205. Springer, Berlin (2003)","DOI":"10.1007\/978-3-540-45069-6_19"},{"key":"209_CR26","doi-asserted-by":"crossref","unstructured":"Boigelot, B., Jodogne, S., Wolper, P.: On the use of weak automata for deciding linear arithmetic with integer and real variables. In: IJCAR. LNCS, vol. 2083, pp. 611\u2013625, Siena, Italy. Springer, Berlin (2001)","DOI":"10.1007\/3-540-45744-5_50"},{"key":"209_CR27","doi-asserted-by":"crossref","unstructured":"Boigelot, B., Legay, A., Wolper, P.: Iterating transducers in the large. In: CAV. LNCS, pp. 223\u2013235. Springer, Berlin (2003)","DOI":"10.1007\/978-3-540-45069-6_24"},{"key":"209_CR28","doi-asserted-by":"crossref","unstructured":"Boigelot, B., Legay, A., Wolper, P.: Omega-regular model checking. In: TACAS. LNCS, vol. 2988, pp. 561\u2013575. Springer, Berlin (2004)","DOI":"10.1007\/978-3-540-24730-2_41"},{"key":"209_CR29","doi-asserted-by":"crossref","unstructured":"Boigelot, B., Rassart, S., Wolper, P.: On the expressiveness of real and integer arithmetic automata (extended abstract). In: Proceedings of 25th International Colloquium on Automata, Languages and Programming (ICALP). LNCS, vol. 1443, pp. 152\u2013163. Springer, Berlin (1998)","DOI":"10.1007\/BFb0055049"},{"key":"209_CR30","doi-asserted-by":"crossref","unstructured":"Boigelot, B., Wolper, P.: Symbolic verification with periodic sets. In: CAV. LNCS, volume 818, pp. 55\u201367. Springer, Berlin (1994)","DOI":"10.1007\/3-540-58179-0_43"},{"key":"209_CR31","doi-asserted-by":"crossref","unstructured":"Boigelot, B., Wolper, P.: Representing arithmetic constraints with finite automata: an overview. In: ICLP. LNCS, vol. 2401, pp. 1\u201319. Springer, Berlin (2002)","DOI":"10.1007\/3-540-45619-8_1"},{"key":"209_CR32","doi-asserted-by":"crossref","unstructured":"Bouajjani, A., Esparza, J., Maler, O.: Reachability analysis of pushdown automata: application to model-checking. In: CONCUR. LNCS, vol. 1243, pp. 135\u2013150. Springer, Berlin (1997)","DOI":"10.1007\/3-540-63141-0_10"},{"key":"209_CR33","doi-asserted-by":"crossref","unstructured":"Bouajjani, A., Habermehl, P.: Symbolic reachability analysis of fifo channel systems with nonregular sets of configurations. In: ICALP. LNCS, vol. 1256, pp. 560\u2013570. Springer, Berlin (1997)","DOI":"10.1007\/3-540-63165-8_211"},{"key":"209_CR34","doi-asserted-by":"crossref","unstructured":"Bouajjani, A., Habermehl, P., Moro, P., Vojnar, T.: Verifying programs with dynamic 1-selector-linked structures in regular model checking. In: TACAS. LNCS, vol. 3440, pp. 13\u201329. Springer, Berlin (2005)","DOI":"10.1007\/978-3-540-31980-1_2"},{"key":"209_CR35","doi-asserted-by":"crossref","unstructured":"Bouajjani, A., Habermehl, P., Rogalewicz, A., Vojnar, T.: Abstract regular (tree) model checking. Special Section on Regular Model Checking STTT (2010, in this volume)","DOI":"10.1007\/s10009-011-0205-y"},{"key":"209_CR36","doi-asserted-by":"crossref","unstructured":"Bouajjani, A., Habermehl, P., Vojnar, T.: Abstract regular model checking. In: CAV. LNCS, vol. 3114, pp. 372\u2013386. Springer, Berlin (2004)","DOI":"10.1007\/978-3-540-27813-9_29"},{"key":"209_CR37","doi-asserted-by":"crossref","unstructured":"Bouajjani, A., Jonsson, B., Nilsson, M., Touili, T.: Regular model checking. In: CAV. LNCS, vol. 1855, pp. 403\u2013418. Springer, Berlin (2000)","DOI":"10.1007\/10722167_31"},{"key":"209_CR38","doi-asserted-by":"crossref","unstructured":"Bouajjani, A., Legay, A., Wolper, P.: Handling liveness properties in (omega-)regular model checking. In: INFINITY. ENTCS, vol. 138(3) Elsevier, Amsterdam (2005)","DOI":"10.1016\/j.entcs.2005.02.061"},{"key":"209_CR39","doi-asserted-by":"crossref","unstructured":"Bouajjani, A., Touili, T.: Extrapolating tree transformations. In: CAV. LNCS, vol. 2404, pp. 539\u2013554. Springer, Berlin (2002)","DOI":"10.1007\/3-540-45657-0_46"},{"key":"209_CR40","doi-asserted-by":"crossref","unstructured":"Bouajjani, A., Touili, T.: Widening techniques for regular tree model checking. Special Section on Regular Model Checking STTT (2010, in this volume)","DOI":"10.1007\/s10009-011-0208-8"},{"key":"209_CR41","doi-asserted-by":"crossref","unstructured":"Bouyer, P., Cassez, F., Fleury, E., Larsen, K.G.: Synthesis of optimal strategies using hytech. In: GDV, vol. 119, pp. 11\u201331 (2005)","DOI":"10.1016\/j.entcs.2004.07.006"},{"key":"209_CR42","doi-asserted-by":"crossref","unstructured":"Broy, M., Jonsson, B., Katoen, J.-P., Leucker, M., Pretschner, A. (eds.): Model-based testing of reactive systems. LNCS, vol. 3472. Springer, Berlin (2005)","DOI":"10.1007\/b137241"},{"issue":"3","key":"209_CR43","doi-asserted-by":"crossref","first-page":"293","DOI":"10.1145\/136035.136043","volume":"24","author":"R. Bryant","year":"1992","unstructured":"Bryant R.: Symbolic boolean manipulation with ordered binary-decision diagrams. ACM Comput. Surv. 24(3), 293\u2013318 (1992)","journal-title":"ACM Comput. Surv."},{"issue":"2","key":"209_CR44","doi-asserted-by":"crossref","first-page":"142","DOI":"10.1016\/0890-5401(92)90017-A","volume":"98","author":"J.R. Burch","year":"1992","unstructured":"Burch J.R., Clarke E.M., McMillan K.L., Dill D.L., Hwang L.J.: Symbolic model checking: 1020 states and beyond. Inf. Comput. 98(2), 142\u2013170 (1992)","journal-title":"Inf. Comput."},{"key":"209_CR45","doi-asserted-by":"crossref","unstructured":"Cantin, F., Legay, A., Wolper, P.: Computing convex hull by automata iteration. In: CIAA. LNCS, vol. 5148, pp. 112\u2013121. Springer, Berlin (2008)","DOI":"10.1007\/978-3-540-70844-5_12"},{"key":"209_CR46","doi-asserted-by":"crossref","unstructured":"Dams, D., Lakhnech, Y., Steffen, M.: Iterating transducers. J. Log. Algebraic Program. (JLAP) 52\u201353:109\u2013127 (2002)","DOI":"10.1016\/S1567-8326(02)00025-5"},{"key":"209_CR47","doi-asserted-by":"crossref","unstructured":"de Alfaro, L., da Silva, L.D., Faella, M., Legay, A., Roy, P., Sorea, M.: Sociable interfaces. In: FROCOS. LNCS, vol. 3717, pp. 81\u2013105. Springer, Berlin (2005)","DOI":"10.1007\/11559306_5"},{"key":"209_CR48","doi-asserted-by":"crossref","unstructured":"de Alfaro, L., Henzinger, T.A.: Interface theories for component-based design. In: EMSOFT, LNCS, vol. 2211, pp. 148\u2013165. Springer, Berlin (2001)","DOI":"10.1007\/3-540-45449-7_11"},{"key":"209_CR49","doi-asserted-by":"crossref","unstructured":"de Alfaro, L., Henzinger, T.A., Majumdar, R.: Symbolic algorithms for infinite-state games. In: CONCUR. LNCS, vol. 2154, pp. 536\u2013550. Springer, Berlin (2001)","DOI":"10.1007\/3-540-44685-0_36"},{"key":"209_CR50","unstructured":"Delzano, G., Rezine, A.: A lightweight regular model checking approach for parameterized systems. Special Section on Regular Model Checking STTT (2010, in this volume)"},{"key":"209_CR51","doi-asserted-by":"crossref","unstructured":"Eisinger, J., Klaedtke, F.; Don\u2019t care words with an application to the automata-based approach for real addition. In: CAV. LNCS, vol. 4144, pp. 67\u201380. Springer, Berlin (2006)","DOI":"10.1007\/11817963_10"},{"key":"209_CR52","doi-asserted-by":"crossref","unstructured":"Finkel, A., Leroux, J.: How to compose presburger-accelerations: Applications to broadcast protocols. In: FSTTCS. LNCS, vol. 2556, pp. 145\u2013156. Springer, Berlin (2002)","DOI":"10.1007\/3-540-36206-1_14"},{"key":"209_CR53","doi-asserted-by":"crossref","unstructured":"Finkel, A., Willems, B., Wolper, P.: A direct symbolic approach to model checking pushdown systems. In: INFINITY. ENTCS, vol. 9. Elsevier Science Publishers, Amsterdam (1997)","DOI":"10.1016\/S1571-0661(05)80426-8"},{"key":"209_CR54","doi-asserted-by":"crossref","unstructured":"Fisman, D., Pnueli, A.: Beyond regular model checking. In: FSTTCS. LNCS, vol. 2245, pp. 156\u2013170. Springer, Berlin (2001)","DOI":"10.1007\/3-540-45294-X_14"},{"key":"209_CR55","doi-asserted-by":"crossref","unstructured":"Habermehl, P., Vojnar, T.: Regular model checking using inference of regular languages. In: INFINITY. ENTCS, vol. 138(3). Elsevier Science Publishers, Amsterdam (2004)","DOI":"10.1016\/j.entcs.2005.01.044"},{"key":"209_CR56","unstructured":"Hopcroft, J.E.: An n log n algorithm for minimizing states in a finite automaton. Theory Mach. Comput. 71(192), 189\u2013196 (1971)"},{"key":"209_CR57","doi-asserted-by":"crossref","unstructured":"Jonsson, B., Nilsson, M.: Transitive closures of regular relations for verifying infinite-state systems. In: TACAS. LNCS, vol. 1785, pp. 220\u2013234. Springer, Berlin (2000)","DOI":"10.1007\/3-540-46419-0_16"},{"key":"209_CR58","doi-asserted-by":"crossref","unstructured":"Kesten, Y., Maler, O., Marcus, M., Pnueli, A., Shahar, E.: Symbolic model checking with rich assertional languages. In: CAV. LNCS, vol. 1254, pp. 424\u2013435. Springer, Berlin (1997)","DOI":"10.1007\/3-540-63166-6_41"},{"key":"209_CR59","volume-title":"Generic Techniques for the Verification of Infinite-State Systems","author":"A. Legay","year":"2007","unstructured":"Legay A.: Generic Techniques for the Verification of Infinite-State Systems. Collection des publications de la Facult\u00e9 des Sciences Appliqu\u00e9es de l\u2019Universit\u00e9 de Li\u00e8ge, Li\u00e8ge (2007)"},{"key":"209_CR60","doi-asserted-by":"crossref","unstructured":"Legay, A.: T(o)rmc: a tool for (omega-)regular model checking. In: CAV. LNCS, vol. 5123, pp. 548\u2013551. Springer, Berlin (2008)","DOI":"10.1007\/978-3-540-70545-1_52"},{"issue":"1","key":"209_CR61","first-page":"46","volume":"12","author":"A. Legay","year":"2011","unstructured":"Legay A., Wolper P.: (Omega-)regular model checking. ACM TOCL 12(1), 46\u201390 (2011)","journal-title":"ACM TOCL"},{"issue":"3","key":"209_CR62","doi-asserted-by":"crossref","first-page":"105","DOI":"10.1016\/S0020-0190(00)00183-6","volume":"79","author":"C. L\u00f6ding","year":"2001","unstructured":"L\u00f6ding C.: Efficient minimization of deterministic weak \u03c9-automata. Inf. Process. Lett. 79(3), 105\u2013109 (2001)","journal-title":"Inf. Process. Lett."},{"key":"209_CR63","volume-title":"Distributed Algorithms","author":"N. Lynch","year":"1996","unstructured":"Lynch N.: Distributed Algorithms. Kaufmann, San Fransisco (1996)"},{"key":"209_CR64","doi-asserted-by":"crossref","unstructured":"Min\u00e9, A.: The octagon abstract domain. In: WCRE, p. 310 (2001)","DOI":"10.1109\/WCRE.2001.957836"},{"key":"209_CR65","doi-asserted-by":"crossref","unstructured":"Muller, D.E., Saoudi, A., Schupp, P.E.: Alternating automata, the weak monadic theory of the tree and its complexity. In: ICALP, pp. 275\u2013283. Springer, Berlin (1986)","DOI":"10.1007\/3-540-16761-7_77"},{"key":"209_CR66","unstructured":"Nilsson, M.: Regular model checking. Master\u2019s thesis, Uppsala University (2001)"},{"key":"209_CR67","unstructured":"Nilsson, M.: Regular model checking. PhD thesis, Uppsala University (2005)"},{"key":"209_CR68","volume-title":"Petri Net Theory and the Modeling of Systems","author":"J. Peterson","year":"1981","unstructured":"Peterson J.: Petri Net Theory and the Modeling of Systems. Prentice Hall, Boston (1981)"},{"key":"209_CR69","doi-asserted-by":"crossref","unstructured":"Safra, S.: Exponential determinization for \u03c9-automata with strong-fairness acceptance condition. In: Proceedings of the 24th ACM Symposium on Theory of Computing, Victoria (1992)","DOI":"10.1145\/129712.129739"},{"issue":"4","key":"209_CR70","doi-asserted-by":"crossref","first-page":"469","DOI":"10.1007\/s100090100059","volume":"3","author":"D.P.L. Simons","year":"2001","unstructured":"Simons D.P.L., Stoelinga M.: Verification of the ieee 1394a root contention protocol using uppaal2k. STTT 3(4), 469\u2013485 (2001)","journal-title":"STTT"},{"key":"209_CR71","unstructured":"The Li\u00e8ge Automata-based Symbolic Handler (LASH). http:\/\/www.montefiore.ulg.ac.be\/~boigelot\/research\/lash\/"},{"key":"209_CR72","unstructured":"The parma polyhedra library. http:\/\/www.cs.unipr.it\/ppl\/"},{"key":"209_CR73","unstructured":"The regular model checking tool (RMC). http:\/\/www.it.uu.se\/research\/docs\/fm\/apv\/rmc"},{"key":"209_CR74","doi-asserted-by":"crossref","unstructured":"Touili, T.: Regular model checking using widening techniques. In: ENTCS, vol. 50(4), pp. 342\u2013356 (2001)","DOI":"10.1016\/S1571-0661(04)00187-2"},{"key":"209_CR75","unstructured":"Touili, T.: Analyse Symbolique de Syst\u00e8mes infinis bas\u00e9e sur les automates: Application \u00e0 la v\u00e9rification de syst\u00e8mes param\u00e9tr\u00e9s. PhD thesis, Paris 7 (2003)"},{"key":"209_CR76","unstructured":"Vardhan, A.: Learning to verify systems. PhD thesis, Univeristy of Illinois (2006)"},{"key":"209_CR77","doi-asserted-by":"crossref","unstructured":"Vardhan, A., Sen, K., Viswanathan, M., Agha, G.: Actively learning to verify safety for fifo automata. In: FSTTCS. LNCS, vol. 3328, pp. 494\u2013505. Springer, Berlin (2004)","DOI":"10.1007\/978-3-540-30538-5_41"},{"key":"209_CR78","doi-asserted-by":"crossref","unstructured":"Vardhan, A., Viswanathan, M.: Lever: a tool for learning based verification. In: CAV. LNCS, vol. 4144, pp. 471\u2013474. Springer, Berlin (2006)","DOI":"10.1007\/11817963_43"},{"key":"209_CR79","unstructured":"Vardi, M.Y.: From church and prior to psl (2007)"},{"key":"209_CR80","doi-asserted-by":"crossref","unstructured":"Wolper, P., Boigelot, B.: An automata-theoretic approach to presburger arithmetic constraints (extended abstract). In: Proceedings of 2nd International Symposium on Static Analysis (SAS). LNCS, vol. 983, pp. 21\u201332. Springer, Berlin (1995)","DOI":"10.1007\/3-540-60360-3_30"},{"key":"209_CR81","doi-asserted-by":"crossref","unstructured":"Wolper, P., Boigelot, B.: Verifying systems with infinite but regular state spaces. In: CAV, LNCS, vol. 1427, pp. 88\u201397. Springer, Berlin (1998)","DOI":"10.1007\/BFb0028736"},{"key":"209_CR82","doi-asserted-by":"crossref","unstructured":"Wolper, P., Boigelot, B.: On the construction of automata from linear arithmetic constraints. In: TACAS. LNCS, vol. 1785, pp. 1\u201319. Springer, Berlin (2000)","DOI":"10.1007\/3-540-46419-0_1"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-011-0209-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-011-0209-7\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-011-0209-7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,8]],"date-time":"2025-03-08T09:48:10Z","timestamp":1741427290000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-011-0209-7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,8,9]]},"references-count":82,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2012,4]]}},"alternative-id":["209"],"URL":"https:\/\/doi.org\/10.1007\/s10009-011-0209-7","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"type":"print","value":"1433-2779"},{"type":"electronic","value":"1433-2787"}],"subject":[],"published":{"date-parts":[[2011,8,9]]}}}