[{"dini_type":"doc-type:other","citation":{"short":"K. Chatterjee, R. Ibsen-Jensen, A. Pavlogiannis, Faster Algorithms for Quantitative Verification in Constant Treewidth Graphs, IST Austria, 2015.","ieee":"K. Chatterjee, R. Ibsen-Jensen, and A. Pavlogiannis, Faster algorithms for quantitative verification in constant treewidth graphs. IST Austria, 2015.","apa":"Chatterjee, K., Ibsen-Jensen, R., & Pavlogiannis, A. (2015). Faster algorithms for quantitative verification in constant treewidth graphs. IST Austria. https://doi.org/10.15479/AT:IST-2015-330-v2-1","mla":"Chatterjee, Krishnendu, et al. Faster Algorithms for Quantitative Verification in Constant Treewidth Graphs. IST Austria, 2015, doi:10.15479/AT:IST-2015-330-v2-1.","ista":"Chatterjee K, Ibsen-Jensen R, Pavlogiannis A. 2015. Faster algorithms for quantitative verification in constant treewidth graphs, IST Austria, 27p.","chicago":"Chatterjee, Krishnendu, Rasmus Ibsen-Jensen, and Andreas Pavlogiannis. Faster Algorithms for Quantitative Verification in Constant Treewidth Graphs. IST Austria, 2015. https://doi.org/10.15479/AT:IST-2015-330-v2-1."},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","author":[{"first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","orcid":"0000-0002-4561-241X"},{"orcid":"0000-0003-4783-0389","last_name":"Ibsen-Jensen","first_name":"Rasmus","id":"3B699956-F248-11E8-B48F-1D18A9856A87"},{"id":"49704004-F248-11E8-B48F-1D18A9856A87","first_name":"Andreas","orcid":"0000-0002-8943-0722","last_name":"Pavlogiannis"}],"has_accepted_license":"1","dc":{"description":["We consider the core algorithmic problems related to verification of systems with respect to three classical quantitative properties, namely, the mean-payoff property, the ratio property, and the minimum initial credit for energy property. \r\nThe algorithmic problem given a graph and a quantitative property asks to compute the optimal value (the infimum value over all traces) from every node of the graph. We consider graphs with constant treewidth, and it is well-known that the control-flow graphs of most programs have constant treewidth. Let $n$ denote the number of nodes of a graph, $m$ the number of edges (for constant treewidth graphs $m=O(n)$) and $W$ the largest absolute value of the weights.\r\nOur main theoretical results are as follows.\r\nFirst, for constant treewidth graphs we present an algorithm that approximates the mean-payoff value within a multiplicative factor of $\\epsilon$ in time $O(n \\cdot \\log (n/\\epsilon))$ and linear space, as compared to the classical algorithms that require quadratic time. Second, for the ratio property we present an algorithm that for constant treewidth graphs works in time $O(n \\cdot \\log (|a\\cdot b|))=O(n\\cdot\\log (n\\cdot W))$, when the output is $\\frac{a}{b}$, as compared to the previously best known algorithm with running time $O(n^2 \\cdot \\log (n\\cdot W))$. Third, for the minimum initial credit problem we show that (i)~for general graphs the problem can be solved in $O(n^2\\cdot m)$ time and the associated decision problem can be solved in $O(n\\cdot m)$ time, improving the previous known $O(n^3\\cdot m\\cdot \\log (n\\cdot W))$ and $O(n^2 \\cdot m)$ bounds, respectively; and (ii)~for constant treewidth graphs we present an algorithm that requires $O(n\\cdot \\log n)$ time, improving the previous known $O(n^4 \\cdot \\log (n \\cdot W))$ bound.\r\nWe have implemented some of our algorithms and show that they present a significant speedup on standard benchmarks. "],"identifier":["https://research-explorer.ista.ac.at/record/5437","https://research-explorer.ista.ac.at/download/5437/5473"],"relation":["info:eu-repo/semantics/altIdentifier/doi/10.15479/AT:IST-2015-330-v2-1","info:eu-repo/semantics/altIdentifier/issn/2664-1690"],"source":["Chatterjee K, Ibsen-Jensen R, Pavlogiannis A. Faster Algorithms for Quantitative Verification in Constant Treewidth Graphs. IST Austria; 2015. doi:10.15479/AT:IST-2015-330-v2-1"],"type":["info:eu-repo/semantics/other","doc-type:other","text","http://purl.org/coar/resource_type/c_1843"],"publisher":["IST Austria"],"date":["2015"],"subject":["ddc:000"],"creator":["Chatterjee, Krishnendu","Ibsen-Jensen, Rasmus","Pavlogiannis, Andreas"],"rights":["info:eu-repo/semantics/openAccess"],"language":["eng"],"title":["Faster algorithms for quantitative verification in constant treewidth graphs","IST Austria Technical Report"]},"day":"27","page":"27","uri_base":"https://research-explorer.ista.ac.at","date_created":"2018-12-12T11:39:19Z","date_published":"2015-04-27T00:00:00Z","oa":1,"date_updated":"2023-02-23T12:26:05Z","ddc":[],"creator":{"id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","login":"dernst"},"file_date_updated":"2020-07-14T12:46:54Z","department":[{"_id":"KrCh","tree":[{"_id":"ResearchGroups"},{"_id":"IST"}]}],"_id":"5437","type":"technical_report","pubrep_id":"333","status":"public","publication_status":"published","publication_identifier":{"issn":[]},"language":[{}],"file":[{"access_level":"open_access","relation":"main_file","content_type":"application/pdf","checksum":"f5917c20f84018b362d385c000a2e123","file_id":"5473","creator":"system","date_updated":"2020-07-14T12:46:54Z","file_size":1072137,"date_created":"2018-12-12T11:53:12Z","file_name":"IST-2015-330-v2+1_main.pdf"}],"related_material":{"record":[{"status":"public","id":"1607","relation":"later_version"},{"id":"5430","status":"public","relation":"earlier_version"}]},"abstract":[{"lang":"eng"}],"oa_version":"Published Version","alternative_title":[],"month":"04"}]