{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,28]],"date-time":"2025-03-28T08:45:23Z","timestamp":1743151523563,"version":"3.40.3"},"publisher-location":"Cham","reference-count":44,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319216898"},{"type":"electronic","value":"9783319216904"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-21690-4_9","type":"book-chapter","created":{"date-parts":[[2015,7,15]],"date-time":"2015-07-15T02:08:27Z","timestamp":1436926107000},"page":"140-157","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["Faster Algorithms for Quantitative Verification in Constant Treewidth Graphs"],"prefix":"10.1007","author":[{"given":"Krishnendu","family":"Chatterjee","sequence":"first","affiliation":[]},{"given":"Rasmus","family":"Ibsen-Jensen","sequence":"additional","affiliation":[]},{"given":"Andreas","family":"Pavlogiannis","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,7,16]]},"reference":[{"key":"9_CR1","unstructured":"DIMACS implementation challenges. \n                      http:\/\/dimacs.rutgers.edu\/Challenges\/"},{"key":"9_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1007\/978-3-642-39212-2_3","volume-title":"Automata, Languages, and Programming","author":"S Almagor","year":"2013","unstructured":"Almagor, S., Boker, U., Kupferman, O.: Formalizing and reasoning about quality. In: Fomin, F.V., Freivalds, R., Kwiatkowska, M., Peleg, D. (eds.) ICALP 2013, Part II. LNCS, vol. 7966, pp. 15\u201327. Springer, Heidelberg (2013)"},{"key":"9_CR3","doi-asserted-by":"crossref","unstructured":"Blackburn, S.M., Garner, R., Hoffmann, C., Khang, A.M., McKinley, K.S., Bentzur, R., Diwan, A., Feinberg, D., Frampton, D., Guyer, S.Z., Hirzel, M., Hosking, A., Jump, M., Lee, H., Moss, J.E.B., Phansalkar, A., Stefanovi\u0107, D., VanDrunen, T., von Dincklage, D., Wiedermann, B.: The DaCapo benchmarks: Java benchmarking development and analysis. In: OOPSLA. ACM (2006)","DOI":"10.1145\/1167473.1167488"},{"key":"9_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"140","DOI":"10.1007\/978-3-642-02658-4_14","volume-title":"Computer Aided Verification","author":"R Bloem","year":"2009","unstructured":"Bloem, R., Chatterjee, K., Henzinger, T.A., Jobstmann, B.: Better quality in synthesis through quantitative objectives. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 140\u2013156. Springer, Heidelberg (2009)"},{"key":"9_CR5","doi-asserted-by":"crossref","unstructured":"Bloem, R., Greimel, K., Henzinger, T.A., Jobstmann, B.: Synthesizing robust systems. In: FMCAD (2009)","DOI":"10.1109\/FMCAD.2009.5351139"},{"key":"9_CR6","first-page":"1","volume":"11","author":"HL Bodlaender","year":"1993","unstructured":"Bodlaender, H.L.: A tourist guide through treewidth. Acta Cybern. 11, 1\u201322 (1993)","journal-title":"Acta Cybern."},{"key":"9_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-30577-4_1","volume-title":"SOFSEM 2005: Theory and Practice of Computer Science","author":"HL Bodlaender","year":"2005","unstructured":"Bodlaender, H.L.: Discovering treewidth. In: Vojt\u00e1\u0161, P., Bielikov\u00e1, M., Charron-Bost, B., S\u00fdkora, O. (eds.) SOFSEM 2005. LNCS, vol. 3381, pp. 1\u201316. Springer, Heidelberg (2005)"},{"key":"9_CR8","series-title":"Lecture Notes in Computer Science","volume-title":"Automata, Languages and Programming","author":"H Bodlaender","year":"1995","unstructured":"Bodlaender, H., Hagerup, T.: Parallel algorithms with optimal speedup for bounded treewidth. In: F\u00fcl\u00f6p, Z. (ed.) ICALP 1995. LNCS, vol. 944. Springer, Heidelberg (1995)"},{"key":"9_CR9","doi-asserted-by":"crossref","unstructured":"Boker, U., Chatterjee, K., Henzinger, T.A., Kupferman, O.: Temporal specifications with accumulative values. In: LICS (2011)","DOI":"10.1109\/LICS.2011.33"},{"key":"9_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1007\/978-3-540-85778-5_4","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"P Bouyer","year":"2008","unstructured":"Bouyer, P., Fahrenberg, U., Larsen, K.G., Markey, N., Srba, J.: Infinite runs in weighted timed automata with energy constraints. In: Cassez, F., Jard, C. (eds.) FORMATS 2008. LNCS, vol. 5215, pp. 33\u201347. Springer, Heidelberg (2008)"},{"key":"9_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"266","DOI":"10.1007\/978-3-662-44584-6_19","volume-title":"CONCUR 2014 \u2013 Concurrency Theory","author":"P Bouyer","year":"2014","unstructured":"Bouyer, P., Markey, N., Matteplackel, R.M.: Averaging in LTL. In: Baldan, P., Gorla, D. (eds.) CONCUR 2014. LNCS, vol. 8704, pp. 266\u2013280. Springer, Heidelberg (2014)"},{"key":"9_CR12","doi-asserted-by":"crossref","unstructured":"Burns, S.M.: Performance analysis and optimization of asynchronous circuits. Technical report (1991)","DOI":"10.21236\/ADA447732"},{"key":"9_CR13","doi-asserted-by":"crossref","unstructured":"Cerny, P., Henzinger, T.A., Radhakrishna, A.: Quantitative abstraction refinement. In: POPL. ACM (2013)","DOI":"10.1145\/2429069.2429085"},{"key":"9_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"543","DOI":"10.1007\/978-3-642-39799-8_36","volume-title":"Computer Aided Verification","author":"K Chatterjee","year":"2013","unstructured":"Chatterjee, K., \u0141\u0105cki, J.: Faster algorithms for markov decision processes with low treewidth. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 543\u2013558. Springer, Heidelberg (2013)"},{"key":"9_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1007\/978-3-642-15375-4_19","volume-title":"CONCUR 2010 - Concurrency Theory","author":"K Chatterjee","year":"2010","unstructured":"Chatterjee, K., Doyen, L., Edelsbrunner, H., Henzinger, T.A., Rannou, P.: Mean-payoff automaton expressions. In: Gastin, P., Laroussinie, F. (eds.) CONCUR 2010. LNCS, vol. 6269, pp. 269\u2013283. Springer, Heidelberg (2010)"},{"key":"9_CR16","doi-asserted-by":"crossref","unstructured":"Chatterjee, K., Doyen, L., Henzinger, T.A.: Expressiveness and closure properties for quantitative languages. LMCS (2010)","DOI":"10.2168\/LMCS-6(3:10)2010"},{"key":"9_CR17","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1805950.1805953","volume":"11","author":"K Chatterjee","year":"2010","unstructured":"Chatterjee, K., Doyen, L., Henzinger, T.A.: Quantitative languages. Trans. Comput. Log. 11, 1\u201338 (2010)","journal-title":"Trans. Comput. Log."},{"key":"9_CR18","doi-asserted-by":"crossref","unstructured":"Chatterjee, K., Goyal, P., Ibsen-Jensen, R., Pavlogiannis, A.: Faster algorithms for algebraic path properties in recursive state machines with constant treewidth. In: POPL (2015)","DOI":"10.1145\/2676726.2676979"},{"key":"9_CR19","doi-asserted-by":"publisher","first-page":"104","DOI":"10.1016\/j.tcs.2014.06.031","volume":"547","author":"K Chatterjee","year":"2014","unstructured":"Chatterjee, K., Henzinger, M., Krinninger, S., Loitzenbauer, V., Raskin, M.A.: Approximating the minimum cycle mean. Theor. Comput. Sci 547, 104\u2013116 (2014)","journal-title":"Theor. Comput. Sci"},{"key":"9_CR20","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2699430","volume":"62","author":"K Chatterjee","year":"2014","unstructured":"Chatterjee, K., Henzinger, T.A., Jobstmann, B., Singh, R.: Measuring and synthesizing systems in probabilistic environments. JACM 62, 1\u201334 (2014)","journal-title":"JACM"},{"key":"9_CR21","doi-asserted-by":"crossref","unstructured":"Chatterjee, K., Henzinger, T.A., Otop, J.: Nested weighted automata. Technical report, IST Austria (2014)","DOI":"10.1109\/LICS.2015.72"},{"key":"9_CR22","unstructured":"Chatterjee, K., Ibsen-Jensen, R., Pavlogiannis, A.: Faster algorithms for quantitative verification in constant treewidth graphs. Technical report. \n                      http:\/\/arxiv.org\/abs\/1504.07384"},{"key":"9_CR23","doi-asserted-by":"crossref","unstructured":"Chatterjee, K., Velner, Y.: Mean-payoff pushdown games. In: LICS. IEEE Computer Society (2012)","DOI":"10.1109\/LICS.2012.30"},{"key":"9_CR24","doi-asserted-by":"publisher","first-page":"12","DOI":"10.1016\/0890-5401(90)90043-H","volume":"85","author":"B Courcelle","year":"1990","unstructured":"Courcelle, B.: The monadic second-order logic of graphs. I. Recognizable sets of finite graphs. Inf. Comput. 85, 12\u201375 (1990)","journal-title":"Inf. Comput."},{"key":"9_CR25","doi-asserted-by":"publisher","first-page":"889","DOI":"10.1109\/43.728912","volume":"17","author":"A Dasdan","year":"1998","unstructured":"Dasdan, A., Gupta, R.: Faster maximum and minimum mean cycle algorithms for system-performance analysis. IEEE Trans. Comput.-Aided Des. Integr. Circ. Syst. 17, 889\u2013899 (1998)","journal-title":"IEEE Trans. Comput.-Aided Des. Integr. Circ. Syst."},{"key":"9_CR26","unstructured":"Dasdan, A., Irani, S.S., Gupta, R.K.: An experimental study of minimum mean cycle algorithms. Technical report (1998)"},{"key":"9_CR27","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-01492-5","volume-title":"Handbook of Weighted Automata","author":"M Droste","year":"2009","unstructured":"Droste, M., Kuich, W., Vogler, H.: Handbook of Weighted Automata. Springer, Heidelberg (2009)"},{"key":"9_CR28","first-page":"45","volume":"220","author":"M Droste","year":"2012","unstructured":"Droste, M., Meinecke, I.: Weighted automata and weighted MSO logics for average and long-time behaviors. Inf. Comput. 220, 45\u201359 (2012)","journal-title":"Inf. Comput."},{"key":"9_CR29","doi-asserted-by":"crossref","unstructured":"Elberfeld, M., Jakoby, A., Tantau, T.: Logspace versions of the theorems of Bodlaender and Courcelle. In: FOCS. IEEE Computer Society (2010)","DOI":"10.1109\/FOCS.2010.21"},{"key":"9_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"86","DOI":"10.1007\/3-540-45643-0_7","volume-title":"Algorithm Engineering and Experiments","author":"J Gustedt","year":"2002","unstructured":"Gustedt, J., M\u00e6hle, O.A., Telle, J.A.: The treewidth of java programs. In: Mount, D.M., Stein, C. (eds.) ALENEX 2002. LNCS, vol. 2409, pp. 86\u201397. Springer, Heidelberg (2002)"},{"key":"9_CR31","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/BF01917434","volume":"8","author":"R Halin","year":"1976","unstructured":"Halin, R.: S-functions for graphs. J. Geom. 8, 171\u2013186 (1976)","journal-title":"J. Geom."},{"key":"9_CR32","doi-asserted-by":"publisher","first-page":"567","DOI":"10.1002\/net.3230230607","volume":"23","author":"M Hartmann","year":"1993","unstructured":"Hartmann, M., Orlin, J.B.: Finding minimum cost to time ratio cycles with small integral transit times. Networks 23, 567\u2013574 (1993)","journal-title":"Networks"},{"key":"9_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"273","DOI":"10.1007\/978-3-642-40184-8_20","volume-title":"CONCUR 2013 \u2013 Concurrency Theory","author":"TA Henzinger","year":"2013","unstructured":"Henzinger, T.A., Otop, J.: From model checking to model measuring. In: D\u2019Argenio, P.R., Melgratti, H. (eds.) CONCUR 2013 \u2013 Concurrency Theory. LNCS, vol. 8052, pp. 273\u2013287. Springer, Heidelberg (2013)"},{"key":"9_CR34","doi-asserted-by":"publisher","first-page":"309","DOI":"10.1016\/0012-365X(78)90011-0","volume":"23","author":"RM Karp","year":"1978","unstructured":"Karp, R.M.: A characterization of the minimum cycle mean in a digraph. Discrete Math. 23, 309\u2013311 (1978)","journal-title":"Discrete Math."},{"key":"9_CR35","volume-title":"Combinatorial Optimization: Networks and Matroids","author":"E Lawler","year":"1976","unstructured":"Lawler, E.: Combinatorial Optimization: Networks and Matroids. Saunders College Publishing, Fort Worth (1976)"},{"key":"9_CR36","unstructured":"Madani, O.: Polynomial value iteration algorithms for deterministic MDPs. In: UAI. Morgan Kaufmann Publishers (2002)"},{"key":"9_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"80","DOI":"10.1007\/978-3-540-45069-6_7","volume-title":"Computer Aided Verification","author":"J Obdr\u017e\u00e1lek","year":"2003","unstructured":"Obdr\u017e\u00e1lek, J.: Fast Mu-calculus model checking when tree-width is bounded. In: Hunt Jr, W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 80\u201392. Springer, Heidelberg (2003)"},{"key":"9_CR38","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1007\/BF01586040","volume":"54","author":"JB Orlin","year":"1992","unstructured":"Orlin, J.B., Ahuja, R.K.: New scaling algorithms for the assignment and minimum mean cycle problems. Math. Program. 54, 41\u201356 (1992)","journal-title":"Math. Program."},{"key":"9_CR39","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0020-0190(79)90079-6","volume":"8","author":"CH Papadimitriou","year":"1979","unstructured":"Papadimitriou, C.H.: Efficient search for rationals. IPL 8, 1\u20134 (1979)","journal-title":"IPL"},{"key":"9_CR40","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1016\/0095-8956(84)90013-3","volume":"39","author":"N Robertson","year":"1984","unstructured":"Robertson, N., Seymour, P.: Graph minors. III. Planar tree-width. J. Comb. Theor. Ser. B 39, 49\u201364 (1984)","journal-title":"J. Comb. Theor. Ser. B"},{"key":"9_CR41","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1137\/0201010","volume":"1","author":"R Tarjan","year":"1972","unstructured":"Tarjan, R.: Depth-first search and linear graph algorithms. SIAM J. Comput. 1, 146\u2013160 (1972)","journal-title":"SIAM J. Comput."},{"key":"9_CR42","doi-asserted-by":"publisher","first-page":"159","DOI":"10.1006\/inco.1997.2697","volume":"142","author":"M Thorup","year":"1998","unstructured":"Thorup, M.: All structured programs have small tree width and good register allocation. Inf. Comput. 142, 159\u2013181 (1998)","journal-title":"Inf. Comput."},{"key":"9_CR43","unstructured":"Vall\u00e9e-Rai, R. Co, P., Gagnon, E., Hendren, L., Lam, P., Sundaresan, V.: Soot - a java bytecode optimization framework. In: CASCON 1999. IBM Press (1999)"},{"key":"9_CR44","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"390","DOI":"10.1007\/978-3-642-31585-5_36","volume-title":"Automata, Languages, and Programming","author":"Y Velner","year":"2012","unstructured":"Velner, Y.: The complexity of mean-payoff automaton expression. In: Czumaj, A., Mehlhorn, K., Pitts, A., Wattenhofer, R. (eds.) ICALP 2012, Part II. LNCS, vol. 7392, pp. 390\u2013402. Springer, Heidelberg (2012)"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-21690-4_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,7,22]],"date-time":"2019-07-22T20:04:50Z","timestamp":1563825890000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-21690-4_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319216898","9783319216904"],"references-count":44,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-21690-4_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"16 July 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}