{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,6]],"date-time":"2026-10-06T14:15:13Z","timestamp":1791296113204,"version":"4.1.0"},"reference-count":48,"publisher":"Association for Computing Machinery (ACM)","issue":"4","content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Program. Lang. Syst."],"published-print":{"date-parts":[[2005,7]]},"abstract":"<jats:p>\n            Recursive state machines (RSMs) enhance the power of ordinary state machines by allowing vertices to correspond either to ordinary states or to potentially recursive invocations of other state machines. RSMs can model the control flow in sequential imperative programs containing recursive procedure calls. They can be viewed as a visual notation extending Statecharts-like hierarchical state machines, where concurrency is disallowed but recursion is allowed. They are also related to various models of pushdown systems studied in the verification and program analysis communities.After introducing RSMs and comparing their expressiveness with other models, we focus on whether verification can be efficiently performed for RSMs. Our first goal is to examine the verification of linear time properties of RSMs. We begin this study by dealing with two key components for algorithmic analysis and model checking, namely, reachability (Is a target state reachable from initial states?) and cycle detection (Is there a reachable cycle containing an accepting state?). We show that both these problems can be solved in time\n            <jats:italic>O<\/jats:italic>\n            (\n            <jats:italic>n<\/jats:italic>\n            \u03b8\n            <jats:sup>2<\/jats:sup>\n            ) and space\n            <jats:italic>O<\/jats:italic>\n            (\n            <jats:italic>n<\/jats:italic>\n            \u03b8), where\n            <jats:italic>n<\/jats:italic>\n            is the size of the recursive machine and \u03b8 is the maximum, over all component state machines, of the minimum of the number of entries and the number of exits of each component. From this, we easily derive algorithms for linear time temporal logic model checking with the same complexity in the model. We then turn to properties in the branching time logic CTL*, and again demonstrate a bound linear in the size of the state machine, but only for the case of RSMs with a single exit node.\n          <\/jats:p>","DOI":"10.1145\/1075382.1075387","type":"journal-article","created":{"date-parts":[[2005,8,3]],"date-time":"2005-08-03T08:30:55Z","timestamp":1123057855000},"page":"786-818","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":159,"title":["Analysis of recursive state machines"],"prefix":"10.1145","volume":"27","author":[{"given":"Rajeev","family":"Alur","sequence":"first","affiliation":[{"name":"University of Pennsylvania, Philadelphia, PA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Michael","family":"Benedikt","sequence":"additional","affiliation":[{"name":"Bell Laboratories, Lisle, IL"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Kousha","family":"Etessami","sequence":"additional","affiliation":[{"name":"University of Edinburgh, Scotland, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Patrice","family":"Godefroid","sequence":"additional","affiliation":[{"name":"Bell Laboratories, Lisle, IL"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Thomas","family":"Reps","sequence":"additional","affiliation":[{"name":"University of Wisconsin, Madison, WI"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Mihalis","family":"Yannakakis","sequence":"additional","affiliation":[{"name":"Columbia University, New York, NY"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2005,7]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"crossref","unstructured":"Alur R. Etessami K. and \n      Madhusudan P\n  . \n  2004\n  . A temporal logic of nested calls and returns. In Proceedings of the 10th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'04) volume \n  2988\n   of \n  LNCS pages \n  467\n  --\n  481\n  . \n  Springer\n  .]]  Alur R. Etessami K. and Madhusudan P. 2004. A temporal logic of nested calls and returns. In Proceedings of the 10th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'04) volume 2988 of LNCS pages 467--481. Springer.]]","DOI":"10.1007\/978-3-540-24730-2_35"},{"key":"e_1_2_1_2_1","first-page":"207","volume-title":"CAV","author":"Alur R.","year":"2001","unstructured":"Alur , R. , Etessami , K. , and Yannakakis , M . 2001. Analysis of recursive state machines . In CAV 2001 , pages 207 -- 220 .]] Alur, R., Etessami, K., and Yannakakis, M. 2001. Analysis of recursive state machines. In CAV 2001, pages 207--220.]]"},{"key":"e_1_2_1_3_1","doi-asserted-by":"crossref","unstructured":"Alur R. Torre S. L. and \n      Madhusudan P\n  . \n  2003\n  a. Modular strategies for recursive game graphs. \n  In Proceedings of TACAS volume \n  2619\n   of \n  LNCS pages \n  363\n  --\n  378\n  .]]   Alur R. Torre S. L. and Madhusudan P. 2003a. Modular strategies for recursive game graphs. In Proceedings of TACAS volume 2619 of LNCS pages 363--378.]]","DOI":"10.1007\/3-540-36577-X_26"},{"key":"e_1_2_1_4_1","doi-asserted-by":"crossref","unstructured":"Alur R. Torre S. L. and \n      Madhusudan P\n  . \n  2003\n  b. Modular strategies for infinite games on recursive graphs. \n  In Proceedings of CAV\n  '03 volume \n  2725\n   of \n  LNCS pages \n  67\n  --\n  79\n  .]]  Alur R. Torre S. L. and Madhusudan P. 2003b. Modular strategies for infinite games on recursive graphs. In Proceedings of CAV'03 volume 2725 of LNCS pages 67--79.]]","DOI":"10.1007\/978-3-540-45069-6_6"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/503502.503503"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)90266-6"},{"key":"e_1_2_1_7_1","series-title":"LNCS","first-page":"113","volume-title":"Bebop: A symbolic model checker for boolean programs. In SPIN '2000","author":"Ball T.","year":"2000","unstructured":"Ball , T. and Rajamani , S . 2000 . Bebop: A symbolic model checker for boolean programs. In SPIN '2000 , volume 1885 of LNCS , pages 113 -- 130 .]] Ball, T. and Rajamani, S. 2000. Bebop: A symbolic model checker for boolean programs. In SPIN '2000, volume 1885 of LNCS, pages 113--130.]]"},{"key":"e_1_2_1_8_1","first-page":"652","volume-title":"ICALP'2001","author":"Benedikt M.","unstructured":"Benedikt , M. , Godefroid , P. , and Reps , T . 2001. Model checking of unrestricted hierarchical state machines . In ICALP'2001 , pages 652 -- 666 .]] Benedikt, M., Godefroid, P., and Reps, T. 2001. Model checking of unrestricted hierarchical state machines. In ICALP'2001, pages 652--666.]]"},{"key":"e_1_2_1_9_1","unstructured":"Booch G. Jacobson J. and Rumbaugh J. 1997. The Unified Modeling Language User Guide. Addison Wesley.]]   Booch G. Jacobson J. and Rumbaugh J. 1997. The Unified Modeling Language User Guide. Addison Wesley.]]"},{"key":"e_1_2_1_10_1","first-page":"135","volume-title":"CONCUR'97","author":"Bouajjani A.","unstructured":"Bouajjani , A. , Esparza , J. , and Maler , O . 1997. Reachability analysis of pushdown automata: Applications to model checking . In CONCUR'97 , pages 135 -- 150 .]] Bouajjani, A., Esparza, J., and Maler, O. 1997. Reachability analysis of pushdown automata: Applications to model checking. In CONCUR'97, pages 135--150.]]"},{"key":"e_1_2_1_11_1","first-page":"62","volume-title":"POPL '03","author":"Bouajjani A.","unstructured":"Bouajjani , A. , Esparza , J. , and Touili , T . 2003. A generic approach to the static analysis of concurrent programs with procedures . In POPL '03 , pages 62 -- 73 .]] 10.1145\/604131.604137 Bouajjani, A., Esparza, J., and Touili, T. 2003. A generic approach to the static analysis of concurrent programs with procedures. In POPL '03, pages 62--73.]] 10.1145\/604131.604137"},{"key":"e_1_2_1_12_1","doi-asserted-by":"crossref","unstructured":"Balakrishnan G.\n     and \n      Reps T\n  . \n  2004\n  . Analyzing memory accesses in x86 executables. In Proceedings of the International Conference on Compiler Construction (CC'04) volume \n  2985\n   of \n  LNCS pages \n  5\n  --\n  23\n  . \n  Springer\n  .]]  Balakrishnan G. and Reps T. 2004. Analyzing memory accesses in x86 executables. In Proceedings of the International Conference on Compiler Construction (CC'04) volume 2985 of LNCS pages 5--23. Springer.]]","DOI":"10.1007\/978-3-540-24723-4_2"},{"key":"e_1_2_1_13_1","first-page":"122","volume-title":"CONCUR '92","author":"Burkart O.","unstructured":"Burkart , O. and Steffen , B . 1992. Model checking and context-free processes . In CONCUR '92 , pages 122 -- 137 .]] Burkart, O. and Steffen, B. 1992. Model checking and context-free processes. In CONCUR '92, pages 122--137.]]"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(99)00034-1"},{"key":"e_1_2_1_15_1","first-page":"109","volume-title":"Proceedings of the 10th Static Analysis Symposium","author":"Chatterjee K.","unstructured":"Chatterjee , K. , Ma , D. , Majumdar , R. , Zhao , T. , Henzinger , T. A. , and Palsberg , J . 2003. Stack size analysis for interrupt-driven programs . In Proceedings of the 10th Static Analysis Symposium , pages 109 -- 126 .]] Chatterjee, K., Ma, D., Majumdar, R., Zhao, T., Henzinger, T. A., and Palsberg, J. 2003. Stack size analysis for interrupt-driven programs. In Proceedings of the 10th Static Analysis Symposium, pages 109--126.]]"},{"key":"e_1_2_1_16_1","volume-title":"Proceedings of the Conference on Computer and Communication Section.]] 10","author":"Chen H.","unstructured":"Chen , H. and Wagner , D . 2002. MOPS: An infrastructure for examining security properties of software . In Proceedings of the Conference on Computer and Communication Section.]] 10 .1145\/586110.586142 Chen, H. and Wagner, D. 2002. MOPS: An infrastructure for examining security properties of software. In Proceedings of the Conference on Computer and Communication Section.]] 10.1145\/586110.586142"},{"key":"e_1_2_1_17_1","first-page":"237","volume-title":"IFIP Conference on Formal Description of Programming Concepts, St-Andrews, N.B., CA, E.J. Neuhold (Ed.)","author":"Cousot P.","unstructured":"Cousot , P. and Cousot , R . 1977. Static determination of dynamic properties of recursive procedures . In IFIP Conference on Formal Description of Programming Concepts, St-Andrews, N.B., CA, E.J. Neuhold (Ed.) , pages 237 -- 277 , St-Andrews, N.B., Canada.]] Cousot, P. and Cousot, R. 1977. Static determination of dynamic properties of recursive procedures. In IFIP Conference on Formal Description of Programming Concepts, St-Andrews, N.B., CA, E.J. Neuhold (Ed.), pages 237--277, St-Andrews, N.B., Canada.]]"},{"key":"e_1_2_1_18_1","doi-asserted-by":"crossref","unstructured":"Caucal B. and Monfort R. 1990. On the transition graphs of automata and grammars. In Graph Theoretic Concepts in Computer Science Springer LNCS 484 pages 311--337.]]   Caucal B. and Monfort R. 1990. On the transition graphs of automata and grammars. In Graph Theoretic Concepts in Computer Science Springer LNCS 484 pages 311--337.]]","DOI":"10.1007\/3-540-53832-1_51"},{"key":"e_1_2_1_19_1","volume-title":"Handbook of Theoretical Computer Science","author":"Emerson A.","unstructured":"Emerson , A. 1990. Modal and temporal logic . In Handbook of Theoretical Computer Science , Volume B, pages 995-- 1072 , MIT Press .]] Emerson, A. 1990. Modal and temporal logic. In Handbook of Theoretical Computer Science, Volume B, pages 995--1072, MIT Press.]]"},{"key":"e_1_2_1_20_1","first-page":"267","volume-title":"LICS 98","author":"Emerson A.","unstructured":"Emerson , A. and Lei , C . 1986. Efficient model-checking in fragments of the propositional mu-calculus . In LICS 98 , pages 267 -- 278 .]] Emerson, A. and Lei, C. 1986. Efficient model-checking in fragments of the propositional mu-calculus. In LICS 98, pages 267--278.]]"},{"key":"e_1_2_1_21_1","doi-asserted-by":"crossref","unstructured":"Esparza J. Hansel D. Rossmanith P. and \n      Schwoon S\n  . \n  2000\n  . Efficient algorithms for model checking pushdown systems. In Computer Aided Verification 12th International Conference volume \n  1855\n   of \n  LNCS pages \n  232\n  --\n  247\n  . \n  Springer\n  .]]   Esparza J. Hansel D. Rossmanith P. and Schwoon S. 2000. Efficient algorithms for model checking pushdown systems. In Computer Aided Verification 12th International Conference volume 1855 of LNCS pages 232--247. Springer.]]","DOI":"10.1007\/10722167_20"},{"key":"e_1_2_1_22_1","doi-asserted-by":"crossref","first-page":"282","DOI":"10.1007\/978-3-540-24622-0_23","volume-title":"5th International Conference on Verification, Model Checking, and Abstract Interpretation","volume":"2937","author":"Etessami K.","year":"2004","unstructured":"Etessami , K. 2004 . Analysis of recursive game graphs using data flow equations . In 5th International Conference on Verification, Model Checking, and Abstract Interpretation , volume 2937 of LNCS, pages 282 -- 296 . Springer.]] Etessami, K. 2004. Analysis of recursive game graphs using data flow equations. In 5th International Conference on Verification, Model Checking, and Abstract Interpretation, volume 2937 of LNCS, pages 282--296. Springer.]]"},{"key":"e_1_2_1_23_1","doi-asserted-by":"crossref","unstructured":"Finkel A. Willems B. and \n      Wolper P\n  . \n  1997\n  . A direct symbolic approach to model checking pushdown systems. In Infinity'97 \n  Workshop volume \n  9\n   of \n  Electronic Notes in Theoretical Computer Science\n  .]]  Finkel A. Willems B. and Wolper P. 1997. A direct symbolic approach to model checking pushdown systems. In Infinity'97 Workshop volume 9 of Electronic Notes in Theoretical Computer Science.]]","DOI":"10.1016\/S1571-0661(05)80426-8"},{"key":"e_1_2_1_24_1","unstructured":"GrammaTech Inc. 2000. CodeSurfer System. \u201chttp:\/\/www.grammatech.com\/products\/ codesurfer\/\u201d.]]  GrammaTech Inc. 2000. CodeSurfer System. \u201chttp:\/\/www.grammatech.com\/products\/ codesurfer\/\u201d.]]"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(87)90035-9"},{"key":"e_1_2_1_26_1","first-page":"342","volume-title":"Proceedings of Logic in Computer Science","author":"Heintze N.","year":"1997","unstructured":"Heintze , N. and McAllester , D. A. 1997 . On the cubic bottleneck in subtyping and flow analysis . In Proceedings of Logic in Computer Science , pages 342 -- 351 .]] Heintze, N. and McAllester, D. A. 1997. On the cubic bottleneck in subtyping and flow analysis. In Proceedings of Logic in Computer Science, pages 342--351.]]"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/77606.77608"},{"key":"e_1_2_1_28_1","unstructured":"Horwitz S. Reps T. Bricker T. and Rosay G. 1997. Wisconsin Program-Slicing Tool. \u201chttp:\/\/www.cs.wisc.edu\/wpis\/slicing_tool\/\u201d.]]  Horwitz S. Reps T. Bricker T. and Rosay G. 1997. Wisconsin Program-Slicing Tool. \u201chttp:\/\/www.cs.wisc.edu\/wpis\/slicing_tool\/\u201d.]]"},{"key":"e_1_2_1_29_1","first-page":"11","volume-title":"Proceedings of the 2nd ACM Symposium on Foundation of Software Engineering","author":"Horwitz S.","year":"1931","unstructured":"Horwitz , S. , Reps , T. , Sagiv , M. , and Rosay , G . 1994. Speeding up slicing . In Proceedings of the 2nd ACM Symposium on Foundation of Software Engineering , pages 11 -- 20 .]] 10.1145\/ 1931 73.195287 Horwitz, S., Reps, T., Sagiv, M., and Rosay, G. 1994. Speeding up slicing. In Proceedings of the 2nd ACM Symposium on Foundation of Software Engineering, pages 11--20.]] 10.1145\/193173.195287"},{"key":"e_1_2_1_30_1","first-page":"47","volume-title":"Proceedings of the 8th Internatinal Conference on Compiler Construction","author":"Melski D.","unstructured":"Melski , D. and Reps , T . 1999. Interprocedural path profiling . In Proceedings of the 8th Internatinal Conference on Compiler Construction , pages 47 -- 62 .]] Melski, D. and Reps, T. 1999. Interprocedural path profiling. In Proceedings of the 8th Internatinal Conference on Compiler Construction, pages 47--62.]]"},{"key":"e_1_2_1_31_1","doi-asserted-by":"crossref","unstructured":"Melski D. and Reps T. 2000. Interconvertibility of a class of set constraints and context-free-language reachability. Theoret. Comput. Sci. 248(1--2) 29--98.]] 10.1016\/S0304-3975(00)00049-9   Melski D. and Reps T. 2000. Interconvertibility of a class of set constraints and context-free-language reachability. Theoret. Comput. Sci. 248(1--2) 29--98.]] 10.1016\/S0304-3975(00)00049-9","DOI":"10.1016\/S0304-3975(00)00049-9"},{"key":"e_1_2_1_32_1","doi-asserted-by":"crossref","unstructured":"Reps T. 1998. Program analysis via graph reachability. Info. Soft. Tech. 40(11--12) 701--726.]]  Reps T. 1998. Program analysis via graph reachability. Info. Soft. Tech. 40(11--12) 701--726.]]","DOI":"10.1016\/S0950-5849(98)00093-7"},{"key":"e_1_2_1_33_1","first-page":"49","volume-title":"POPL","author":"Reps T.","year":"1994","unstructured":"Reps , T. , Horwitz , S. , and Sagiv , S . 1995. Precise interprocedural dataflow analysis via graph reachability . In POPL , pages 49 -- 61 .]] 10.1145\/ 1994 48.199462 Reps, T., Horwitz, S., and Sagiv, S. 1995. Precise interprocedural dataflow analysis via graph reachability. In POPL, pages 49--61.]] 10.1145\/199448.199462"},{"key":"e_1_2_1_34_1","first-page":"41","volume-title":"Proceedings of the 3rd ACM Symposium on Foundation of Software Engineering","author":"Reps T.","unstructured":"Reps , T. and Rosay , G . 1995. Precise interprocedural chopping . In Proceedings of the 3rd ACM Symposium on Foundation of Software Engineering , pages 41 -- 52 .]] 10.1145\/222124.222138 Reps, T. and Rosay, G. 1995. Precise interprocedural chopping. In Proceedings of the 3rd ACM Symposium on Foundation of Software Engineering, pages 41--52.]] 10.1145\/222124.222138"},{"key":"e_1_2_1_35_1","first-page":"189","volume-title":"Proceedings of the 10th Static Analysis Symposium","author":"Reps T.","unstructured":"Reps , T. , Schwoon , S. , and Jha , S . 2003. Weighted pushdown systems and their application to interprocedural dataflow analysis . In Proceedings of the 10th Static Analysis Symposium , pages 189 -- 213 .]] Reps, T., Schwoon, S., and Jha, S. 2003. Weighted pushdown systems and their application to interprocedural dataflow analysis. In Proceedings of the 10th Static Analysis Symposium, pages 189--213.]]"},{"key":"e_1_2_1_36_1","doi-asserted-by":"crossref","unstructured":"Sagiv M. Reps T. and Horwitz S. 1996. Precise interprocedural dataflow analysis with applications to constant propagation. Theoret. Comput. Sci. 167(1--2) 131--170.]] 10.1016\/0304-3975(96)00072-2   Sagiv M. Reps T. and Horwitz S. 1996. Precise interprocedural dataflow analysis with applications to constant propagation. Theoret. Comput. Sci. 167(1--2) 131--170.]] 10.1016\/0304-3975(96)00072-2","DOI":"10.1016\/0304-3975(96)00072-2"},{"key":"e_1_2_1_37_1","unstructured":"Schwoon S. 2002. Moped System. \u201chttp:\/\/www.fmi.uni-stuttgart.de\/szs\/tools\/moped\/\u201d.]]  Schwoon S. 2002. Moped System. \u201chttp:\/\/www.fmi.uni-stuttgart.de\/szs\/tools\/moped\/\u201d.]]"},{"key":"e_1_2_1_38_1","unstructured":"Schwoon S. Reps T. and Jha S. 2003. Weighted PDS Library. \u201chttp:\/\/www.fmi. uni-stuttgart.de\/szs\/tools\/wpds\/\u201d.]]  Schwoon S. Reps T. and Jha S. 2003. Weighted PDS Library. \u201chttp:\/\/www.fmi. uni-stuttgart.de\/szs\/tools\/wpds\/\u201d.]]"},{"key":"e_1_2_1_39_1","first-page":"202","volume-title":"Proceedings of the 16th Computer Section Foundations Workshop","author":"Schwoon S.","unstructured":"Schwoon , S. , Jha , S. , Reps , T. , and Stubblebine , S . 2003. On generalized authorization problems . In Proceedings of the 16th Computer Section Foundations Workshop , pages 202 -- 218 .]] Schwoon, S., Jha, S., Reps, T., and Stubblebine, S. 2003. On generalized authorization problems. In Proceedings of the 16th Computer Section Foundations Workshop, pages 202--218.]]"},{"key":"e_1_2_1_40_1","doi-asserted-by":"crossref","unstructured":"Ball T. and Rajamani S. 2000. SLAM Toolkit. \u201chttp:\/\/research.microsoft.com\/slam\/\u201d.]]  Ball T. and Rajamani S. 2000. SLAM Toolkit. \u201chttp:\/\/research.microsoft.com\/slam\/\u201d.]]","DOI":"10.1007\/3-540-44585-4_25"},{"key":"e_1_2_1_41_1","volume-title":"Prentice-Hall","author":"Sharir M.","unstructured":"Sharir , M. and Pnueli , A . 1981. Two approaches to interprocedural data flow analysis. In Program Flow Analysis: Theory and Applications, S.S. Muchnick and N.D. Jones (eds.) , Prentice-Hall , Englewood Cliffs, NJ, pages 189--234.]] Sharir, M. and Pnueli, A. 1981. Two approaches to interprocedural data flow analysis. In Program Flow Analysis: Theory and Applications, S.S. Muchnick and N.D. Jones (eds.), Prentice-Hall, Englewood Cliffs, NJ, pages 189--234.]]"},{"key":"e_1_2_1_42_1","volume-title":"Principles of Database and Knowledge-base systems","author":"Ullman J. D.","unstructured":"Ullman , J. D. 1988. Principles of Database and Knowledge-base systems . Computer Science Press .]] Ullman, J. D. 1988. Principles of Database and Knowledge-base systems. Computer Science Press.]]"},{"key":"e_1_2_1_43_1","doi-asserted-by":"crossref","first-page":"308","DOI":"10.1016\/S0022-0000(75)80046-8","article-title":"General context-free recognition in less than cubic time","volume":"10","author":"Valiant L. G.","year":"1975","unstructured":"Valiant , L. G. 1975 . General context-free recognition in less than cubic time . J. Comput. Syst. Sci. 10 , 308 -- 315 .]] Valiant, L. G. 1975. General context-free recognition in less than cubic time. J. Comput. Syst. Sci. 10, 308--315.]]","journal-title":"J. Comput. Syst. Sci."},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(86)90026-7"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.2000.2894"},{"key":"e_1_2_1_46_1","first-page":"230","volume-title":"Proceedings of the 9th ACM Symposium on Principles of Database Systems","author":"Yannakakis M.","year":"1990","unstructured":"Yannakakis , M. 1990 . Graph-theoretic methods in database theory . In Proceedings of the 9th ACM Symposium on Principles of Database Systems , pages 230 -- 242 .]] 10.1145\/298514.298576 Yannakakis, M. 1990. Graph-theoretic methods in database theory. In Proceedings of the 9th ACM Symposium on Principles of Database Systems, pages 230--242.]] 10.1145\/298514.298576"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/355598.362773"},{"key":"e_1_2_1_48_1","volume-title":"2004. A C++ Library for Weighted Pushdown Systems","unstructured":"WPDS++ : 2004. A C++ Library for Weighted Pushdown Systems , University of Wisconsin.]] WPDS++: 2004. A C++ Library for Weighted Pushdown Systems, University of Wisconsin.]]"}],"container-title":["ACM Transactions on Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1075382.1075387","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,12,28]],"date-time":"2022-12-28T15:27:14Z","timestamp":1672241234000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1075382.1075387"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005,7]]},"references-count":48,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2005,7]]}},"alternative-id":["10.1145\/1075382.1075387"],"URL":"https:\/\/doi.org\/10.1145\/1075382.1075387","relation":{},"ISSN":["0164-0925","1558-4593"],"issn-type":[{"value":"0164-0925","type":"print"},{"value":"1558-4593","type":"electronic"}],"subject":[],"published":{"date-parts":[[2005,7]]},"assertion":[{"value":"2005-07-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}