{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T07:25:20Z","timestamp":1740122720860,"version":"3.37.3"},"reference-count":50,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2021,4,29]],"date-time":"2021-04-29T00:00:00Z","timestamp":1619654400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2021,4,29]],"date-time":"2021-04-29T00:00:00Z","timestamp":1619654400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/501100002428","name":"Austrian Science Fund","doi-asserted-by":"publisher","award":["P23499-N23","S11407-N23"],"award-info":[{"award-number":["P23499-N23","S11407-N23"]}],"id":[{"id":"10.13039\/501100002428","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","award":["279307"],"award-info":[{"award-number":["279307"]}],"id":[{"id":"10.13039\/501100000781","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100004318","name":"Microsoft","doi-asserted-by":"publisher","award":["Faculty Fellows Award"],"award-info":[{"award-number":["Faculty Fellows Award"]}],"id":[{"id":"10.13039\/100004318","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2021,9]]},"DOI":"10.1007\/s10703-021-00373-5","type":"journal-article","created":{"date-parts":[[2021,4,29]],"date-time":"2021-04-29T16:02:31Z","timestamp":1619712151000},"page":"401-428","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Faster algorithms for quantitative verification in bounded treewidth graphs"],"prefix":"10.1007","volume":"57","author":[{"given":"Krishnendu","family":"Chatterjee","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Rasmus","family":"Ibsen-Jensen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andreas","family":"Pavlogiannis","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2021,4,29]]},"reference":[{"key":"373_CR1","series-title":"LNCS","first-page":"15","volume-title":"ICALP","author":"S Almagor","year":"2013","unstructured":"Almagor S, Boker U, Kupferman O (2013) Formalizing and reasoning about quality. ICALP. LNCS. Springer, New York, pp 15\u201327"},{"key":"373_CR2","doi-asserted-by":"crossref","unstructured":"Alur R, D\u2019Antoni L, Deshmukh JV, Raghothaman M, Yuan Y (2013) Regular functions and cost register automata. In: LICS, pp 13\u201322","DOI":"10.1109\/LICS.2013.65"},{"key":"373_CR3","doi-asserted-by":"crossref","unstructured":"Blackburn SM, Garner R, Hoffmann C, Khang AM, McKinley KS, Bentzur R, Diwan A, Feinberg D, Frampton D, Guyer SZ, Hirzel M, Hosking A, Jump M, Lee H, Moss JEB, Phansalkar A, Stefanovi\u0107 D, VanDrunen T, von Dincklage D, Wiedermann B (2006) The DaCapo benchmarks: Java benchmarking development and analysis. In: OOPSLA. ACM, pp 169\u2013190","DOI":"10.1145\/1167515.1167488"},{"issue":"3\u20134","key":"373_CR4","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/s00236-013-0191-5","volume":"51","author":"R Bloem","year":"2014","unstructured":"Bloem R, Chatterjee K, Greimel K, Henzinger TA, Hofferek G, Jobstmann B, K\u00f6nighofer B, K\u00f6nighofer R (2014) Synthesizing robust systems. Acta Inf 51(3\u20134):193\u2013220","journal-title":"Acta Inf"},{"key":"373_CR5","doi-asserted-by":"crossref","unstructured":"Blumensath A, Colcombet T, Kuperberg D, Parys P, Vanden Boom M (2014) Two-way cost automata and cost logics over infinite trees. In: CSL-LICS, pp 16:1\u201316:9","DOI":"10.1145\/2603088.2603104"},{"key":"373_CR6","unstructured":"Bodlaender HL (1993) A tourist guide through treewidth. Acta Cybern"},{"key":"373_CR7","doi-asserted-by":"crossref","unstructured":"Bodlaender H (2005) Discovering treewidth. In: SOFSEM: theory and practice of computer science. LNCS. Springer","DOI":"10.1007\/978-3-540-30577-4_1"},{"key":"373_CR8","doi-asserted-by":"crossref","unstructured":"Bodlaender H, Hagerup T (1995) Parallel algorithms with optimal speedup for bounded treewidth. In: ICALP. LNCS. Springer","DOI":"10.1007\/3-540-60084-1_80"},{"issue":"2","key":"373_CR9","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1145\/2579819","volume":"15","author":"B Bollig","year":"2014","unstructured":"Bollig B, Gastin P, Monmege B, Zeitoun M (2014) Pebble weighted automata and weighted logics. ACM Trans Comput Log 15(2):15","journal-title":"ACM Trans Comput Log"},{"key":"373_CR10","doi-asserted-by":"crossref","unstructured":"Bouyer P, Fahrenberg U, Larsen KG, Markey N, Srba J (2008) Infinite runs in weighted timed automata with energy constraints. In: FORMATS. LNCS, vol 5215. Springer, pp 33\u201347","DOI":"10.1007\/978-3-540-85778-5_4"},{"key":"373_CR11","doi-asserted-by":"crossref","unstructured":"Bouyer P, Markey N, Matteplackel RM (2014) Averaging in LTL. CONCUR. LNCS. Springer, pp 266\u2013280","DOI":"10.1007\/978-3-662-44584-6_19"},{"key":"373_CR12","unstructured":"Brosius D. Java agent for memory measurements. https:\/\/github.com\/jbellis\/jamm"},{"key":"373_CR13","doi-asserted-by":"crossref","unstructured":"Burns SM (1991) Performance analysis and optimization of asynchronous circuits. Technical report","DOI":"10.21236\/ADA447734"},{"key":"373_CR14","doi-asserted-by":"crossref","unstructured":"Cerny P, Henzinger TA, Radhakrishna A (2013) Quantitative abstraction refinement. In: POPL. ACM, pp 115\u2013128","DOI":"10.1145\/2480359.2429085"},{"key":"373_CR15","doi-asserted-by":"crossref","unstructured":"Chatterjee K, Lacki J (2013) Faster algorithms for Markov decision processes with low treewidth. In: CAV. LNCS. Springer","DOI":"10.1007\/978-3-642-39799-8_36"},{"key":"373_CR16","doi-asserted-by":"crossref","unstructured":"Chatterjee K, Doyen L, Henzinger TA (2010) Quantitative languages. Trans Comput Log","DOI":"10.1145\/1805950.1805953"},{"key":"373_CR17","doi-asserted-by":"crossref","unstructured":"Chatterjee K, Ibsen-Jensen R, Pavlogiannis A (2015) Faster algorithms for quantitative verification in bounded treewidth graphs. In: CAV, pp 140\u2013157","DOI":"10.1007\/978-3-319-21690-4_9"},{"key":"373_CR18","doi-asserted-by":"crossref","unstructured":"Chatterjee K, Goharshady AK, Ibsen-Jensen R, Pavlogiannis A (2016) Algorithms for algebraic path properties in concurrent systems of constant treewidth components. In: POPL, pp 733\u2013747","DOI":"10.1145\/2914770.2837624"},{"key":"373_CR19","doi-asserted-by":"crossref","unstructured":"Chatterjee K, Henzinger M, Krinninger S, Loitzenbauer V, Raskin MA (2014) Approximating the minimum cycle mean. Theor Comput Sci","DOI":"10.1016\/j.tcs.2014.06.031"},{"key":"373_CR20","doi-asserted-by":"crossref","unstructured":"Chatterjee K, Ibsen-Jensen R, Pavlogiannis A, Goyal P (2015) Faster algorithms for algebraic path properties in recursive state machines with constant treewidth. In: POPL. ACM","DOI":"10.1145\/2676726.2676979"},{"key":"373_CR21","doi-asserted-by":"crossref","unstructured":"Chatterjee K, Pavlogiannis A, Velner Y (2015) Quantitative interprocedural analysis. In: POPL, pp 539\u2013551","DOI":"10.1145\/2775051.2676968"},{"key":"373_CR22","doi-asserted-by":"crossref","unstructured":"Chaudhuri S, Zaroliagis CD (1995) Shortest paths in digraphs of small treewidth. Sequential algorithms, algorithmica, part I","DOI":"10.1007\/3-540-60084-1_78"},{"key":"373_CR23","doi-asserted-by":"crossref","unstructured":"Colcombet T, L\u00f6ding C (2010) Regular cost functions over finite trees. In: LICS, pp 70\u201379","DOI":"10.1109\/LICS.2010.36"},{"key":"373_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 (1990) The monadic second-order logic of graphs. I. Recognizable sets of finite graphs. Inf Comput 85:12\u201375","journal-title":"Inf Comput"},{"key":"373_CR25","unstructured":"DIMACS implementation challenges. http:\/\/dimacs.rutgers.edu\/Challenges\/"},{"key":"373_CR26","doi-asserted-by":"publisher","first-page":"889","DOI":"10.1109\/43.728912","volume":"17","author":"A Dasdan","year":"1998","unstructured":"Dasdan A, Gupta R (1998) Faster maximum and minimum mean cycle algorithms for system-performance analysis. IEEE Trans Comput Aided Des Integr Circuits Syst 17:889\u2013899","journal-title":"IEEE Trans Comput Aided Des Integr Circuits Syst"},{"key":"373_CR27","unstructured":"Dasdan A, Irani SS, Gupta RK (1998) An experimental study of minimum mean cycle algorithms. Technical report"},{"key":"373_CR28","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 (2009) Handbook of weighted automata. Springer, New York"},{"key":"373_CR29","doi-asserted-by":"publisher","first-page":"44","DOI":"10.1016\/j.ic.2012.10.001","volume":"220","author":"M Droste","year":"2012","unstructured":"Droste M, Meinecke I (2012) Weighted automata and weighted MSO logics for average and long-time behaviors. Inf Comput 220:44\u201359","journal-title":"Inf Comput"},{"key":"373_CR30","doi-asserted-by":"crossref","unstructured":"Elberfeld M, Jakoby A, Tantau T (2010) Logspace versions of the theorems of Bodlaender and Courcelle. In: FOCS. IEEE Computer Society","DOI":"10.1109\/FOCS.2010.21"},{"key":"373_CR31","doi-asserted-by":"publisher","first-page":"132","DOI":"10.1007\/978-3-642-32940-1_11","volume-title":"CONCUR 2012-concurrency theory","author":"E Filiot","year":"2012","unstructured":"Filiot E, Gentilini R, Raskin JF (2012) Quantitative languages defined by functional automata. In: Koutny M, Ulidowski I (eds) CONCUR 2012-concurrency theory. Springer, Berlin, pp 132\u2013146"},{"key":"373_CR32","doi-asserted-by":"publisher","first-page":"112","DOI":"10.1007\/978-3-642-19835-9_11","volume-title":"Tools and algorithms for the construction and analysis of systems","author":"V Forejt","year":"2011","unstructured":"Forejt V, Kwiatkowska M, Norman G, Parker D, Qu H (2011) Quantitative multi-objective verification for probabilistic systems. In: Abdulla PA, Leino KRM (eds) Tools and algorithms for the construction and analysis of systems. Springer, Berlin, pp 112\u2013127"},{"key":"373_CR33","doi-asserted-by":"crossref","unstructured":"Gustedt J, Mhle O, Telle J (2002) The treewidth of java programs. In: Algorithm engineering and experiments. LNCS. Springer","DOI":"10.1007\/3-540-45643-0_7"},{"key":"373_CR34","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/BF01917434","volume":"8","author":"R Halin","year":"1976","unstructured":"Halin R (1976) S-functions for graphs. J Geom 8:171\u2013186","journal-title":"J Geom"},{"key":"373_CR35","doi-asserted-by":"publisher","first-page":"567","DOI":"10.1002\/net.3230230607","volume":"23","author":"M Hartmann","year":"1993","unstructured":"Hartmann M, Orlin JB (1993) Finding minimum cost to time ratio cycles with small integral transit times. Networks 23:567\u2013574","journal-title":"Networks"},{"key":"373_CR36","doi-asserted-by":"crossref","unstructured":"Henzinger TA, Otop J (2013) From model checking to model measuring. In: CONCUR. LNCS. Springer, pp 273\u2013287","DOI":"10.1007\/978-3-642-40184-8_20"},{"key":"373_CR37","doi-asserted-by":"publisher","first-page":"309","DOI":"10.1016\/0012-365X(78)90011-0","volume":"23","author":"RM Karp","year":"1978","unstructured":"Karp RM (1978) A characterization of the minimum cycle mean in a digraph. Discrete Math 23:309\u2013311","journal-title":"Discrete Math"},{"key":"373_CR38","doi-asserted-by":"crossref","unstructured":"Kreutzer S, Riveros C (2013) Quantitative monadic second-order logic. In: Proceedings of the 2013 28th annual ACM\/IEEE symposium on logic in computer science. LICS \u201913. IEEE Computer Society, New York, pp 113\u2013122","DOI":"10.1109\/LICS.2013.16"},{"issue":"1","key":"373_CR39","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1016\/S0020-0190(02)00455-6","volume":"86","author":"S Kwek","year":"2003","unstructured":"Kwek S, Mehlhorn K (2003) Optimal search for rationals. Inf Process Lett 86(1):23\u201326","journal-title":"Inf Process Lett"},{"key":"373_CR40","volume-title":"Combinatorial optimization: networks and matroids","author":"E Lawler","year":"1976","unstructured":"Lawler E (1976) Combinatorial optimization: networks and matroids. Saunders College Publishing, Philadelphia"},{"key":"373_CR41","unstructured":"Madani O (2002) Polynomial value iteration algorithms for deterministic MDPs. In: UAI. Morgan Kaufmann Publishers"},{"key":"373_CR42","doi-asserted-by":"crossref","unstructured":"Obdrz\u00e1lek J (2003) Fast mu-calculus model checking when tree-width is bounded. In: CAV. LNCS. Springer","DOI":"10.1007\/978-3-540-45069-6_7"},{"key":"373_CR43","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1007\/BF01586040","volume":"54","author":"JB Orlin","year":"1992","unstructured":"Orlin JB, Ahuja RK (1992) New scaling algorithms for the assignment and minimum mean cycle problems. Math Program 54:41\u201356","journal-title":"Math Program"},{"key":"373_CR44","doi-asserted-by":"crossref","unstructured":"Papadimitriou CH (1979) Efficient search for rationals. In: IPL, pp 1\u20134","DOI":"10.1016\/0020-0190(79)90079-6"},{"key":"373_CR45","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1016\/0095-8956(84)90013-3","volume":"36","author":"N Robertson","year":"1984","unstructured":"Robertson N, Seymour P (1984) Graph minors. III. Planar tree-width. J Combin Theory Ser B 36:49\u201364","journal-title":"J Combin Theory Ser B"},{"key":"373_CR46","doi-asserted-by":"publisher","first-page":"309","DOI":"10.1016\/0196-6774(86)90023-4","volume":"7","author":"N Robertson","year":"1986","unstructured":"Robertson N, Seymour P (1986) Graph minors. II. Algorithmic aspects of tree-width. J Algorithms 7:309\u2013322","journal-title":"J Algorithms"},{"key":"373_CR47","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1137\/0201010","volume":"1","author":"R Tarjan","year":"1972","unstructured":"Tarjan R (1972) Depth-first search and linear graph algorithms. SIAM J Comput 1:146\u2013160","journal-title":"SIAM J Comput"},{"key":"373_CR48","doi-asserted-by":"publisher","first-page":"159","DOI":"10.1006\/inco.1997.2697","volume":"142","author":"M Thorup","year":"1998","unstructured":"Thorup M (1998) All structured programs have small tree width and good register allocation. Inf Comput 142:159\u2013181","journal-title":"Inf Comput"},{"key":"373_CR49","unstructured":"Vall\u00e9e-Rai R, Co P, Gagnon E, Hendren L, Lam P, Sundaresan V (1999) Soot\u2014a java bytecode optimization framework. In: CASCON \u201999. IBM Press"},{"key":"373_CR50","doi-asserted-by":"crossref","unstructured":"Velner Y (2012) The complexity of mean-payoff automaton expression. In: ICALP. LNCS. Springer","DOI":"10.1007\/978-3-642-31585-5_36"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-021-00373-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10703-021-00373-5\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-021-00373-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,12,1]],"date-time":"2021-12-01T12:10:32Z","timestamp":1638360632000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10703-021-00373-5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,4,29]]},"references-count":50,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2021,9]]}},"alternative-id":["373"],"URL":"https:\/\/doi.org\/10.1007\/s10703-021-00373-5","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"type":"print","value":"0925-9856"},{"type":"electronic","value":"1572-8102"}],"subject":[],"published":{"date-parts":[[2021,4,29]]},"assertion":[{"value":"23 September 2015","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"8 April 2021","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"29 April 2021","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}