{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,8]],"date-time":"2025-03-08T05:13:09Z","timestamp":1741410789859,"version":"3.38.0"},"reference-count":55,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2011,7,20]],"date-time":"2011-07-20T00:00:00Z","timestamp":1311120000000},"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-0206-x","type":"journal-article","created":{"date-parts":[[2011,7,19]],"date-time":"2011-07-19T18:43:45Z","timestamp":1311101025000},"page":"193-206","source":"Crossref","is-referenced-by-count":4,"title":["Domain-specific regular acceleration"],"prefix":"10.1007","volume":"14","author":[{"given":"Bernard","family":"Boigelot","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2011,7,20]]},"reference":[{"key":"206_CR1","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Bouajjani, A., Jonsson, B.: On-the-fly analysis of systems with unbounded, lossy FIFO channels. In: Proceedings of 10th International Conference on Computer-Aided Verification (CAV\u201998). Lecture Notes in Computer Science, vol. 1427, pp. 305\u2013318. Springer, Berlin (1998)","DOI":"10.1007\/BFb0028754"},{"issue":"1","key":"206_CR2","doi-asserted-by":"crossref","first-page":"39","DOI":"10.1023\/B:FORM.0000033962.51898.1a","volume":"25","author":"P. Aziz Abdulla","year":"2004","unstructured":"Aziz Abdulla P., Collomb-Annichini A., Bouajjani A., Jonsson B.: Using forward reachability analysis for verification of lossy channel systems. Formal Methods Syst. Des. 25(1), 39\u201365 (2004)","journal-title":"Formal Methods Syst. Des."},{"key":"206_CR3","doi-asserted-by":"crossref","unstructured":"Alur, R., Courcoubetis, C., Dill, D.: Model-checking for real-time systems. In: Proceedings of 5th Symposium on Logic in Computer Science (LICS\u201990), pp. 414\u2013425, Philadelphia (1990)","DOI":"10.1109\/LICS.1990.113766"},{"key":"206_CR4","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.-H., Nicollin X., Olivero A., Sifakis J., Yovine S.: The algorithmic analysis of hybrid systems. Theor. Comput. Sci. 138, 3\u201334 (1995)","journal-title":"Theor. Comput. Sci."},{"key":"206_CR5","doi-asserted-by":"crossref","unstructured":"Alur, R., Henzinger, T.A., Ho, P.H.: Automatic symbolic verification of embedded systems. In: Proceedings of 14th annual IEEE Real-Time Systems Symposium, pp. 2\u201311 (1993)","DOI":"10.1109\/REAL.1993.393520"},{"issue":"2","key":"206_CR6","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":"206_CR7","unstructured":"Abdulla, P.A., Jonsson, B., Nilsson, M., d\u2019Orso, J.: Regular model checking made simple and efficient. In: Proceedings of 15th International Conference on Computer-Aided Verification (CAV\u201903). Lecture Notes in Computer Science, vol. 2725, pp. 237\u2013248, Boulder, USA. Springer, Berlin (2003)"},{"key":"206_CR8","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Jonsson, B., Nilsson, M., Saksena, M.: A survey of regular model checking. In: Proceedings of 15th International Conference on Concurrency Theory (CONCUR\u201904). Lecture Notes in Computer Science, vol. 3170, pp. 35\u201348. Springer, Berlin (2004)","DOI":"10.1007\/978-3-540-28644-8_3"},{"key":"206_CR9","doi-asserted-by":"crossref","unstructured":"Boigelot, B., Brusten, J., Leroux, J.: A generalization of Semenov\u2019s theorem to automata over real numbers. In: Proceedings of 22nd International Conference on Automated Deduction (CADE\u201909). Lecture Notes in Computer Science, vol. 5663, pp. 469\u2013484. Springer, Berlin (2009)","DOI":"10.1007\/978-3-642-02959-2_34"},{"key":"206_CR10","doi-asserted-by":"crossref","unstructured":"Boigelot, B., Bronne, L., Rassart, S.: An improved reachability analysis method for strongly linear hybrid systems. In: Proceedings of 9th International Conference on Computer-Aided Verification (CAV\u201997). LNCS, vol. 1254, pp. 167\u2013177, Haifa. Springer, Berlin (1997)","DOI":"10.1007\/3-540-63166-6_18"},{"key":"206_CR11","doi-asserted-by":"crossref","unstructured":"Boudet, A., Comon, H.: Diophantine equations, Presburger arithmetic and finite automata. In: Proceedings of 21st International Colloquium on Trees in Algebra and Programming (CAAP\u201996). Lecture Notes in Computer Science, vol. 1059, pp. 30\u201343. Springer, Berlin (1996)","DOI":"10.1007\/3-540-61064-2_27"},{"issue":"2","key":"206_CR12","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":"206_CR13","doi-asserted-by":"crossref","unstructured":"Bardin, S., Finkel, A., Leroux, J., Petrucci, L: Fast: fast acceleration of symbolic transition systems. In: Proceedings of 15th International Conference on Computer-Aided Verification (CAV\u201903). Lecture Notes in Computer Science, vol. 2725, pp. 118\u2013121. Springer, Berlin (2003)","DOI":"10.1007\/978-3-540-45069-6_12"},{"key":"206_CR14","doi-asserted-by":"crossref","unstructured":"Boigelot, B., Godefroid, P., Willems, B. Wolper, P.: The power of QDDs. In: Proceedings of 4th International Symposium on Static Analysis (SAS\u201997). Lecture Notes in Computer Science, vol. 1302, pp. 172\u2013186, Paris. Springer, Berlin (1997)","DOI":"10.1007\/BFb0032741"},{"issue":"1\u20132","key":"206_CR15","doi-asserted-by":"crossref","first-page":"211","DOI":"10.1016\/S0304-3975(99)00033-X","volume":"221","author":"A. Bouajjani","year":"1999","unstructured":"Bouajjani A., Habermehl P.: Symbolic reachability analysis of FIFO-channel systems with nonregular sets of configurations. Theor. Comput. Sci. 221(1\u20132), 211\u2013250 (1999)","journal-title":"Theor. Comput. Sci."},{"key":"206_CR16","doi-asserted-by":"crossref","unstructured":"Boigelot, B., Herbreteau, F.: The power of hybrid acceleration. In: Proceedings of 18th International Conference on Computer-Aided Verification (CAV\u201906). Lecture Notes in Computer Science, vol. 4144, pp. 438\u2013451. Springer, Berlin (2006)","DOI":"10.1007\/11817963_40"},{"key":"206_CR17","doi-asserted-by":"crossref","unstructured":"Boigelot, B., Herbreteau, F., Jodogne, S.: Hybrid acceleration using real vector automata. In: Proceedings of 15th International Conference on Computer-Aided Verification (CAV\u201903). Lecture Notes in Computer Science, vol. 2725, pp. 193\u2013205. Springer, Berlin (2003)","DOI":"10.1007\/978-3-540-45069-6_19"},{"issue":"2","key":"206_CR18","doi-asserted-by":"crossref","first-page":"191","DOI":"10.36045\/bbms\/1103408547","volume":"1","author":"V. Bruy\u00e8re","year":"1994","unstructured":"Bruy\u00e8re V., Hansel G., Michaux C., Villemaire R.: Logic and p-recognizable sets of integers. Bull. Belgian Math. Soc. 1(2), 191\u2013238 (1994)","journal-title":"Bull. Belgian Math. Soc."},{"issue":"3","key":"206_CR19","doi-asserted-by":"crossref","first-page":"614","DOI":"10.1145\/1071596.1071601","volume":"6","author":"B. Boigelot","year":"2005","unstructured":"Boigelot B., Jodogne S., Wolper P.: An effective decision procedure for linear arithmetic over the integers and reals. ACM Trans. Comput. Log. 6(3), 614\u2013633 (2005)","journal-title":"ACM Trans. Comput. Log."},{"issue":"1","key":"206_CR20","doi-asserted-by":"crossref","first-page":"17","DOI":"10.1016\/j.tcs.2003.10.002","volume":"313","author":"B. Boigelot","year":"2004","unstructured":"Boigelot B., Latour L.: Counting the solutions of Presburger equations without enumerating them. Theor. Comput. Sci. 313(1), 17\u201329 (2004)","journal-title":"Theor. Comput. Sci."},{"key":"206_CR21","doi-asserted-by":"crossref","unstructured":"Boigelot, B., Legay, A., Wolper, P.: Iterating transducers in the large. In: Proceedings of 15th International Conference on Computer-Aided Verification (CAV\u201903). Lecture Notes in Computer Science, vol. 2725, pp. 223\u2013235, Boulder, USA. Springer, Berlin (2003)","DOI":"10.1007\/978-3-540-45069-6_24"},{"key":"206_CR22","unstructured":"Boigelot, B.: Symbolic Methods for Exploring Infinite State Spaces. PhD thesis, Universit\u00e9 de Li\u00e8ge (1998)"},{"issue":"1\u20133","key":"206_CR23","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."},{"issue":"3","key":"206_CR24","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."},{"key":"206_CR25","doi-asserted-by":"crossref","unstructured":"Bouajjani, A., Touili T.: Widening techniques for regular tree model checking. Special Section on Regular Model Checking STTT in this volume (2011). doi: 10.1007\/s10009-011-0208-8","DOI":"10.1007\/s10009-011-0208-8"},{"key":"206_CR26","doi-asserted-by":"crossref","unstructured":"Boigelot, B., Wolper, P.: Symbolic verification with periodic sets. In: Proceedings of 6th International Conference on Computer-Aided Verification (CAV\u201994). Lecture Notes in Computer Science, vol. 818, pp. 55\u201367, Stanford. Springer, Berlin (1994)","DOI":"10.1007\/3-540-58179-0_43"},{"issue":"2","key":"206_CR27","doi-asserted-by":"crossref","first-page":"323","DOI":"10.1145\/322374.322380","volume":"30","author":"D. Brand","year":"1983","unstructured":"Brand D., Zafiropoulo P.: On communicating finite-state machines. J. ACM 30(2), 323\u2013342 (1983)","journal-title":"J. ACM"},{"key":"206_CR28","unstructured":"B\u00fcchi, J.R.: On a decision method in restricted second order arithmetic. In: Proceedings of International Congress on Logic, Methodoloy and Philosophy of Science, pp. 1\u201312. Stanford University Press, Stanford (1962)"},{"key":"206_CR29","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proceedings od 4th ACM Symposium on Principles of Programming Languages (POPL\u201977), pp. 238\u2013252, Los Angeles, California. ACM Press, New York (1977)","DOI":"10.1145\/512950.512973"},{"issue":"1","key":"206_CR30","doi-asserted-by":"crossref","first-page":"20","DOI":"10.1006\/inco.1996.0003","volume":"124","author":"G. C\u00e9c\u00e9","year":"1996","unstructured":"C\u00e9c\u00e9 G., Finkel A., Iyer S.P.: Unreliable channels are easier to verify than perfect channels. Inf. Comput. 124(1), 20\u201331 (1996)","journal-title":"Inf. Comput."},{"key":"206_CR31","doi-asserted-by":"crossref","unstructured":"Comon, H., Jurski, Y.: Multiple counters automata, safety analysis and Presburger arithmetic. In: Proceedings of 10th International Conference on Computer-Aided Verification (CAV\u201998). Lecture Notes in Computer Science, vol. 1427, pp. 268\u2013279. Springer, Berlin (1998)","DOI":"10.1007\/BFb0028751"},{"key":"206_CR32","doi-asserted-by":"crossref","first-page":"186","DOI":"10.1007\/BF01746527","volume":"3","author":"A. Cobham","year":"1969","unstructured":"Cobham A.: On the base-dependence of sets of numbers recognizable by finite automata. Math. Syst. Theory 3, 186\u2013192 (1969)","journal-title":"Math. Syst. Theory"},{"key":"206_CR33","doi-asserted-by":"crossref","unstructured":"Dill, D.L.: Timing assumptions and verification of finite-state concurrent systems. In: Proceedings of Automatic Verification Methods for Finite-State Systems. LNCS, vol. 407, pp. 197\u2013212. Springer, Berlin (1989)","DOI":"10.1007\/3-540-52148-8_17"},{"issue":"1\u20133","key":"206_CR34","doi-asserted-by":"crossref","first-page":"85","DOI":"10.1007\/s10703-008-0057-6","volume":"33","author":"J. Eisinger","year":"2008","unstructured":"Eisinger J., Klaedtke F.: Don\u2019t care words with an application to the automata-based approach for real addition. Formal Methods Syst. Des. 33(1\u20133), 85\u2013115 (2008)","journal-title":"Formal Methods Syst. Des."},{"key":"206_CR35","unstructured":"Fribourg, L.: A closed-form evaluation for extended timed automata. Research Report LSV-98-2, LSV (1998)"},{"key":"206_CR36","doi-asserted-by":"crossref","first-page":"27","DOI":"10.1016\/S1571-0661(05)80426-8","volume":"9","author":"A. Finkel","year":"1997","unstructured":"Finkel A., Willems B., Wolper P.: A direct symbolic approach to model checking pushdown systems. Electr. Notes Theor. Comput. Sci. 9, 27\u201337 (1997)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"206_CR37","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A.: The theory of hybrid automata. In: Proceedings of 11th Symposium on Logic in Computer Science (LICS\u201996), pp. 278\u2013292. IEEE Computer Society Press (1996)","DOI":"10.1109\/LICS.1996.561342"},{"key":"206_CR38","volume-title":"Design and Validation of Computer Protocols","author":"G. Holtzmann","year":"1991","unstructured":"Holtzmann G.: Design and Validation of Computer Protocols. Prentice Hall, New Jersey (1991)"},{"key":"206_CR39","doi-asserted-by":"crossref","unstructured":"Klarlund, N.: Progress measures for complementation of omega-automata with applications to temporal logic. In: Proceedings of 32nd Annual Symposium on Foundations of Computer Science (FOCS\u201991), pp. 358\u2013367, San Juan, Puerto Rico. IEEE (1991)","DOI":"10.1109\/SFCS.1991.185391"},{"key":"206_CR40","doi-asserted-by":"crossref","unstructured":"Klaedtke, F.: Bounds on the automata size for Presburger arithmetic. ACM Trans. Comput. Log. 9(2), 11:1\u201311:34 (2008)","DOI":"10.1145\/1342991.1342995"},{"key":"206_CR41","doi-asserted-by":"crossref","unstructured":"Kupferman, O., Vardi, M.Y.: Complementation constructions for nondeterministic automata on infinite words. In: Proceedings of 11th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201905). Lecture Notes in Computer Science, vol. 3440, pp. 206\u2013221, Edinburgh. Springer, Berlin (2005)","DOI":"10.1007\/978-3-540-31980-1_14"},{"key":"206_CR42","unstructured":"The Li\u00e8ge Automata-based Symbolic Handler (LASH). http:\/\/www.montefiore.ulg.ac.be\/~boigelot\/research\/lash\/"},{"issue":"3","key":"206_CR43","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\u2212automata. Inf. Process. Lett. 79(3), 105\u2013109 (2001)","journal-title":"Inf. Process. Lett."},{"key":"206_CR44","doi-asserted-by":"crossref","unstructured":"Legay, A.: Extrapolating (omega-)regular model checking. Int. J. Softw. Tools Technol. Transfer (2011), doi: 10.1007\/s10009-011-0209-7","DOI":"10.1007\/s10009-011-0209-7"},{"key":"206_CR45","unstructured":"Linear Integer\/Real Arithmetic solver (LIRA). http:\/\/lira.gforge.avacs.org\/"},{"key":"206_CR46","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4615-3190-6","volume-title":"Symbolic Model Checking","author":"K. McMillan","year":"1993","unstructured":"McMillan K.: Symbolic Model Checking. Kluwer Academic Publishers, Dordrecht (1993)"},{"key":"206_CR47","unstructured":"Presburger, M.: \u00dcber die Vollst\u00e4ndigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt. In Comptes Rendus du Premier Congr\u00e8s des Math\u00e9maticiens des Pays Slaves, pp. 92\u2013101, Warsaw (1929)"},{"key":"206_CR48","doi-asserted-by":"crossref","unstructured":"Safra, S.: On the complexity of \u03c9-automata. In: Proceedings of 29th Symposium on Foundations of Computer Science (FOCS\u201988), pp. 319\u2013327. IEEE Computer Society (1988)","DOI":"10.1109\/SFCS.1988.21948"},{"key":"206_CR49","volume-title":"Theory of Linear and Integer Programming","author":"A. Schrijver","year":"1986","unstructured":"Schrijver A.: Theory of Linear and Integer Programming. Wiley, New York (1986)"},{"key":"206_CR50","doi-asserted-by":"crossref","first-page":"289","DOI":"10.1007\/BF00967164","volume":"18","author":"A.L. Semenov","year":"1977","unstructured":"Semenov A.L.: Presburgerness of predicates regular in two number systems. Sib. Math. J. 18, 289\u2013299 (1977)","journal-title":"Sib. Math. J."},{"key":"206_CR51","first-page":"379","volume":"10","author":"L. Staiger","year":"1974","unstructured":"Staiger L., Wagner K.: Automatentheoretische und automatenfreie charakterisierungen topologischer klassen regul\u00e4rer folgenmengen. Elektron. Informationsverarbeitung und Kybernetik EIK 10, 379\u2013392 (1974)","journal-title":"Elektron. Informationsverarbeitung und Kybernetik EIK"},{"key":"206_CR52","doi-asserted-by":"crossref","unstructured":"Wolper, P., Boigelot, B.: An automata-theoretic approach to Presburger arithmetic constraints. In: Proceedings of 2nd International Symposium on Static Analysis (SAS\u201995). LNCS, vol. 983, pp. 21\u201332. Springer, Berlin (1995)","DOI":"10.1007\/3-540-60360-3_30"},{"key":"206_CR53","doi-asserted-by":"crossref","unstructured":"Wolper, P., Boigelot, B.: On the construction of automata from linear arithmetic constraints. In: Proceedings of 6th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201900). Lecture Notes in Computer Science, vol. 1785, pp. 1\u201319. Springer, Berlin (2000)","DOI":"10.1007\/3-540-46419-0_1"},{"key":"206_CR54","doi-asserted-by":"crossref","unstructured":"Weispfenning, V.: Mixed real-integer linear quantifier elimination. In: ISSAC: Proceedings of the ACM SIGSAM International Symposium on Symbolic and Algebraic Computation, pp. 129\u2013136. ACM Press, Vancouver (1999)","DOI":"10.1145\/309831.309888"},{"key":"206_CR55","doi-asserted-by":"crossref","unstructured":"Wilke, T.: Locally threshold testable languages of infinite words. In: Proceedings of 10th Annual Symposium on Theoretical Aspects of Computer Science (STACS\u201993). LNCS, vol. 665, pp. 607\u2013616. Springer, W\u00fcrzburg (1993)","DOI":"10.1007\/3-540-56503-5_60"}],"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-0206-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-011-0206-x\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-011-0206-x","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,7]],"date-time":"2025-03-07T05:51:57Z","timestamp":1741326717000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-011-0206-x"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,7,20]]},"references-count":55,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2012,4]]}},"alternative-id":["206"],"URL":"https:\/\/doi.org\/10.1007\/s10009-011-0206-x","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"type":"print","value":"1433-2779"},{"type":"electronic","value":"1433-2787"}],"subject":[],"published":{"date-parts":[[2011,7,20]]}}}