{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,8]],"date-time":"2025-03-08T02:10:08Z","timestamp":1741399808057,"version":"3.38.0"},"reference-count":50,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2011,8,3]],"date-time":"2011-08-03T00:00:00Z","timestamp":1312329600000},"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-0208-8","type":"journal-article","created":{"date-parts":[[2011,8,2]],"date-time":"2011-08-02T13:13:02Z","timestamp":1312290782000},"page":"145-165","source":"Crossref","is-referenced-by-count":7,"title":["Widening techniques for regular tree model checking"],"prefix":"10.1007","volume":"14","author":[{"given":"Ahmed","family":"Bouajjani","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tayssir","family":"Touili","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2011,8,3]]},"reference":[{"key":"208_CR1","doi-asserted-by":"crossref","unstructured":"Alur, R., Brayton, R.K., Henzinger, T.A., Qadeer, S., Rajamani, S.K.: Partial-order reduction in symbolic state space exploration. In: Computer Aided Verification, pp. 340\u2013351 (1997)","DOI":"10.1007\/3-540-63166-6_34"},{"key":"208_CR2","doi-asserted-by":"crossref","unstructured":"Abdulla, P., Bouajjani, A., Jonsson, B.: On-the-fly Analysis of Systems with Unbounded, Lossy Fifo Channels. In: CAV\u201998. LNCS, vol. 1427 (1998)","DOI":"10.1007\/BFb0028754"},{"key":"208_CR3","doi-asserted-by":"crossref","first-page":"134","DOI":"10.1007\/3-540-48683-6_14","volume":"1633","author":"P.A. Abdulla","year":"1999","unstructured":"Abdulla P.A., Bouajjani A., Jonsson B., Nilsson M.: Handling global conditions in parametrized system verification. Lect. Notes Comput. Sci. 1633, 134\u2013150 (1999)","journal-title":"Lect. Notes Comput. Sci."},{"key":"208_CR4","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Jonsson, B., Mahata, P., d\u2019Orso, J.: Regular tree model checking. In: Proceedings of the 14th International Conference on Computer Aided Verification. Lecture Notes in Computer Science, vol. 2404, pp. 555\u2013568 (2002)","DOI":"10.1007\/3-540-45657-0_47"},{"key":"208_CR5","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Jonsson, B., Nilsson, M., d\u2019Orso, J.: Regular model checking made simple and efficient. In: Proceedings CONCUR 2002 of the 13th International Conference on Concurrency Theory. Lecture Notes in Computer Science, vol. 2421, pp. 116\u2013130 (2002)","DOI":"10.1007\/3-540-45694-5_9"},{"key":"208_CR6","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Jonsson, B., Nilsson, M., d\u2019Orso, J.: Algorithmic improvements in regular model checking. In: Proceedings of the 15th International Conference on Computer Aided Verification. Lecture Notes in Computer Science, vol. 2725, pp. 236\u2013248 (2003)","DOI":"10.1007\/978-3-540-45069-6_25"},{"key":"208_CR7","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Legay, A., d\u2019Orso, J., Rezine, A.: Simulation-based iteration of tree transducers. In: Proceedings of TACAS\u201905 (2005)","DOI":"10.1007\/978-3-540-31980-1_3"},{"key":"208_CR8","doi-asserted-by":"crossref","unstructured":"Balland, E., Boichut, Y., Genet, T., Moreau, P.-E.: Towards an efficient implementation of tree automata completion. In: AMAST, pp. 67\u201382 (2008)","DOI":"10.1007\/978-3-540-79980-1_6"},{"key":"208_CR9","doi-asserted-by":"crossref","unstructured":"Bouajjani, A., Esparza, J., Maler, O.: Reachability Analysis of Pushdown Automata: Application to Model Checking. In: CONCUR\u201997. LNCS, vol. 1243 (1997)","DOI":"10.1007\/3-540-63141-0_10"},{"key":"208_CR10","unstructured":"Bouajjani, A., Esparza, J., Touili, T.: Reachability Analysis of Synchronised PA systems. In: INFINITY\u201904. ENTCS (2004)"},{"key":"208_CR11","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: Proceedings of TACAS\u201905 (2005)","DOI":"10.1007\/978-3-540-31980-1_2"},{"issue":"1","key":"208_CR12","doi-asserted-by":"crossref","first-page":"37","DOI":"10.1016\/j.entcs.2005.11.015","volume":"149","author":"A. Bouajjani","year":"2006","unstructured":"Bouajjani A., Habermehl P., Rogalewicz A., Vojnar T.: Abstract regular tree model checking. Electr. Notes Theor. Comput. Sci. 149(1), 37\u201348 (2006)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"208_CR13","doi-asserted-by":"crossref","unstructured":"Bouajjani, A., Habermehl, P., Vojnar, T.: Abstract regular model checking. In: CAV04. Lecture Notes in Computer Science. pp. 372\u2013386. Springer, Boston (2004)","DOI":"10.1007\/978-3-540-27813-9_29"},{"key":"208_CR14","doi-asserted-by":"crossref","unstructured":"Bouajjani, A., Jonsson, B., Nilsson, M., Touili, T.: Regular model checking. In: CAV\u201900. LNCS (2000)","DOI":"10.1007\/10722167_31"},{"key":"208_CR15","doi-asserted-by":"crossref","unstructured":"Boigelot, B., Legay, A., Wolper, P.: Iterating transducers in the large. In: Proceedings of the 15th International Conference on Computer Aided Verification. Lecture Notes in Computer Science, vol. 2725, pp. 223\u2013235 (2003)","DOI":"10.1007\/978-3-540-45069-6_24"},{"key":"208_CR16","doi-asserted-by":"crossref","unstructured":"Boigelot, B., Legay, A., Wolper, P.: Omega regular model checking. In: Proceedings TACAS \u201904 of the 10th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science. pp. 561\u2013575 (2004)","DOI":"10.1007\/978-3-540-24730-2_41"},{"key":"208_CR17","unstructured":"Bouajjani, A., Muscholl, A., Touili, T.: Permutation Rewriting and Algorithmic Verification. In: LICS\u201901. IEEE, New York (2001)"},{"key":"208_CR18","doi-asserted-by":"crossref","unstructured":"Bouajjani, A.: Languages, Rewriting systems, and Verification of Infinte-State Systems. In: ICALP\u201901. LNCS, vol. 2076 (2001) invited paper","DOI":"10.1007\/3-540-48224-5_3"},{"key":"208_CR19","doi-asserted-by":"crossref","first-page":"217","DOI":"10.1016\/S0019-9958(69)90065-5","volume":"14","author":"W.S. Brained","year":"1969","unstructured":"Brained W.S.: Tree generating regular systems. Inf. Control 14, 217\u2013231 (1969)","journal-title":"Inf. Control"},{"key":"208_CR20","doi-asserted-by":"crossref","unstructured":"Bouajjani A., Touili, T.: Extrapolating Tree Transformations. In: Proceedings of the 14th International Conference on Computer Aided Verification. Lecture Notes in Computer Science, vol. 2404, pp. 539\u2013554 (2002)","DOI":"10.1007\/3-540-45657-0_46"},{"key":"208_CR21","doi-asserted-by":"crossref","unstructured":"Bouajjani, A., Touili, T.: Reachability analysis of process rewrite systems. In: Proceedings of the 23rd International Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS\u201903). LNCS, vol. 2914 (2003)","DOI":"10.1007\/978-3-540-24597-1_7"},{"key":"208_CR22","doi-asserted-by":"crossref","unstructured":"Bouajjani, A., Touili, T.: On Computing Reachability Sets of Process Rewrite Systems. In: RTA\u201905. LNCS (2005)","DOI":"10.1007\/978-3-540-32033-3_35"},{"key":"208_CR23","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Static Determination of Dynamic Properties of Recursive Procedures. In: IFIP Conf. on Formal Description of Programming Concepts. North-Holland, Amsterdam (1977)","DOI":"10.1145\/390017.808314"},{"key":"208_CR24","doi-asserted-by":"crossref","unstructured":"Comon, H., Cortier, V., Mitchell, J.: Tree automata with one memory, set constraints and ping-pong protocols. In: ICALP\u20192001. LNCS, vol. 2076 (2001)","DOI":"10.1007\/3-540-48224-5_56"},{"key":"208_CR25","unstructured":"Comon, H., Dauchet, M., Gilleron, R., Jacquemard, F., Lugiez, D., Tison, S., Tommasi, M.: Tree automata techniques and applications. http:\/\/www.grappa.univ-lille3.fr\/tata (1997)"},{"issue":"1","key":"208_CR26","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1016\/0304-3975(94)90101-5","volume":"127","author":"J.L. Coquid","year":"1994","unstructured":"Coquid J.L., Dauchet M., Gilleron R., V\u00e1gvlgyi S.: Bottom-up tree pushdown automata and rewrite systems. Theor. Comput. Sci. 127(1), 69\u201398 (1994)","journal-title":"Theor. Comput. Sci."},{"key":"208_CR27","doi-asserted-by":"crossref","first-page":"395","DOI":"10.1007\/3-540-60218-6_30","volume":"962","author":"E.M. Clarke","year":"1995","unstructured":"Clarke E.M., Grumberg O., Jha S.: Verifying parameterised networks using abstraction and regular languages. Lect. Notes Comput. Sci. 962, 395\u2013407 (1995)","journal-title":"Lect. Notes Comput. Sci."},{"key":"208_CR28","doi-asserted-by":"crossref","unstructured":"Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: POPL\u201978. ACM, New York (1978)","DOI":"10.1145\/512760.512770"},{"key":"208_CR29","doi-asserted-by":"crossref","unstructured":"Dams, D., Lakhnech, Y., Steffen, M.: Iterating transducers. In: CAV\u201901. LNCS (2001)","DOI":"10.1007\/3-540-44585-4_27"},{"key":"208_CR30","doi-asserted-by":"crossref","unstructured":"Dauchet, M., Tison, S.: The theory of ground rewrite systems is decidable. In: Proceedings of the IEEE Conference on Logic in Computer Science (LICS), IEEE Computer Society Press, New York, pp. 242\u2013248 (1990)","DOI":"10.1109\/LICS.1990.113750"},{"key":"208_CR31","doi-asserted-by":"crossref","unstructured":"Dauchet, M., Tison, S.: The theory of ground rewrite systems is decidable. In: Proceedings of 5th IEEE Symposium on Logic in Computer Science, Philadelphia. pp. 242\u2013248 (1990)","DOI":"10.1109\/LICS.1990.113750"},{"key":"208_CR32","doi-asserted-by":"crossref","unstructured":"d\u2019Orso, J., Touili, T.: Regular hedge model checking. In: 4th IFIP International Conference on Theoretical Computer Science (TCS 2006). IFIP, vol. 209, pp. 213\u2013230. Springer, Berlin (2006)","DOI":"10.1007\/978-0-387-34735-6_19"},{"key":"208_CR33","doi-asserted-by":"crossref","unstructured":"Esparza, J., Knoop, J.: An automata-theoretic approach to interprocedural data-flow analysis. In: FOSSACS\u201999. LNCS, vol. 1578 (1999)","DOI":"10.1007\/3-540-49019-1_2"},{"key":"208_CR34","doi-asserted-by":"crossref","unstructured":"Engelfriet, J.: Bottom-up and top-down tree transformations\u2014a comparison. Math. Syst. Theory, 9(3) (1975)","DOI":"10.1007\/BF01704020"},{"key":"208_CR35","doi-asserted-by":"crossref","unstructured":"Esparza, J., Podelski, A.: Efficient algorithms for pre* and post* on interprocedural parallel flow graphs. In: Symposium on Principles of Programming Languages. pp. 1\u201311 (2000)","DOI":"10.1145\/325694.325697"},{"key":"208_CR36","doi-asserted-by":"crossref","unstructured":"Fribourg, L., Olsen, H.: Reachability sets of parametrized rings as regular languages. In: Infinity\u201997. Electronical Notes in Theoretical Computer Science, vol. 9, Elsevier, Amsterdam (1997)","DOI":"10.1016\/S1571-0661(05)80427-X"},{"key":"208_CR37","doi-asserted-by":"crossref","unstructured":"Gilleron, R., Deruyver, A.: The reachability problem for ground trs and some extensions. In: Proceedings of the International Joint Conference on Theory and Practice of Software Development (TAPSOFT\u201989). LNCS, vol. 351, pp. 227\u2013243 (1989)","DOI":"10.1007\/3-540-50939-9_135"},{"key":"208_CR38","doi-asserted-by":"crossref","unstructured":"Genet, T., Klay, F.: Rewriting for cryptographic protocol verification. In: In Proceedings of the 17th International Conference on Automated Deduction, Pittsburgh (Pen., USA). Lecture Notes in Artificial Intelligence, vol. 1831, Springer, Berlin (2000)","DOI":"10.1007\/10721959_21"},{"key":"208_CR39","doi-asserted-by":"crossref","unstructured":"Goubault-Larrecq, J.: A method for automatic cryptographic protocol verification. In: 15th IPDPS 2000 Workshops. LNCS, vol. 1800 (2000)","DOI":"10.1007\/3-540-45591-4_134"},{"key":"208_CR40","doi-asserted-by":"crossref","unstructured":"Jonsson, B., Nilsson, M.: Transitive closures of regular relations for verifying infinite-state systems. In: TACAS\u201900. LNCS (2000)","DOI":"10.1007\/3-540-46419-0_16"},{"key":"208_CR41","first-page":"424","volume-title":"Proc. CAV\u201997, LNCS, vol. 1254","author":"Y. Kesten","year":"1997","unstructured":"Kesten Y., Maler O., Marcus M., Pnueli A., Shahar E.: Symbolic model checking with rich assertional languages. In: Grumberg, O. (eds) Proc. CAV\u201997, LNCS, vol. 1254, pp. 424\u2013435. Springer, Berlin (1997)"},{"key":"208_CR42","doi-asserted-by":"crossref","unstructured":"Lugiez, D., Schnoebelen, Ph.: The regular viewpoint on PA-processes. In: Proceedings of the 9th International Conference on Concurrency Theory (CONCUR\u201998), Nice, France, September 1998. vol. 1466, pp. 50\u201366. Springer, Berlin (1998)","DOI":"10.1007\/BFb0055615"},{"key":"208_CR43","unstructured":"Mayr, R.: Decidability and Complexity of Model Checking Problems for Infinite-State Systems. Phd. thesis, TUM (1998)"},{"key":"208_CR44","unstructured":"Monniaux, D.: Abstracting cryptographic protocols with tree automata. Sci. Comput. Program. (2002)"},{"key":"208_CR45","doi-asserted-by":"crossref","unstructured":"Pnueli, A., Shahar, E.: Liveness and acceleration in parametrized verification. In: CAV\u201900. LNCS (2000)","DOI":"10.1007\/10722167_26"},{"key":"208_CR46","doi-asserted-by":"crossref","unstructured":"Touili, T.: Regular Model Checking using Widening Techniques. In: Vepas Workshop. Electronic Notes in TCS, vol. 50 (2001)","DOI":"10.1016\/S1571-0661(04)00187-2"},{"key":"208_CR47","unstructured":"Touili, T.: Analyse symbolique de syst\u00e8mes infinis bas\u00e8e sur les automates: Application \u00e0 la v\u00e8rification de syst\u00e8mes param\u00e8tr\u00e8s et dynamiques. Phd. thesis, University of Paris 7 (2003)"},{"key":"208_CR48","unstructured":"Touili, T.: Dealing with communication for dynamic multithreaded recursive programs. In: 1st VISSAS workshop (2005) Invited Paper"},{"key":"208_CR49","doi-asserted-by":"crossref","unstructured":"Touili, T.: Computing transitive closures of hedge transformations. In: VECOS. Electronic Workshops in Computing series (eWiC), British Computer Society, London (2007)","DOI":"10.14236\/ewic\/VECOS2007.7"},{"key":"208_CR50","doi-asserted-by":"crossref","unstructured":"Wolper, P., Boigelot, B.: Verifying systems with infinite but regular stae spaces. In: CAV\u201998. LNCS, vol. 1254 (1998)","DOI":"10.1007\/BFb0028736"}],"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-0208-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-011-0208-8\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-011-0208-8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,8]],"date-time":"2025-03-08T01:51:35Z","timestamp":1741398695000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-011-0208-8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,8,3]]},"references-count":50,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2012,4]]}},"alternative-id":["208"],"URL":"https:\/\/doi.org\/10.1007\/s10009-011-0208-8","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"type":"print","value":"1433-2779"},{"type":"electronic","value":"1433-2787"}],"subject":[],"published":{"date-parts":[[2011,8,3]]}}}