[{"citation":{"ista":"Chatterjee K, Ibsen-Jensen R, Pavlogiannis A. 2015. Faster algorithms for quantitative verification in constant treewidth graphs, IST Austria, 31p.","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-319-v1-1","ieee":"K. Chatterjee, R. Ibsen-Jensen, and A. Pavlogiannis, *Faster algorithms for quantitative verification in constant treewidth graphs*. IST Austria, 2015.","short":"K. Chatterjee, R. Ibsen-Jensen, A. Pavlogiannis, Faster Algorithms for Quantitative Verification in Constant Treewidth Graphs, IST Austria, 2015.","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-319-v1-1.","mla":"Chatterjee, Krishnendu, et al. *Faster Algorithms for Quantitative Verification in Constant Treewidth Graphs*. IST Austria, 2015, doi:10.15479/AT:IST-2015-319-v1-1."},"date_published":"2015-02-10T00:00:00Z","day":"10","dini_type":"doc-type:other","file":[{"date_updated":"2020-07-14T12:46:52Z","creator":"system","date_created":"2018-12-12T11:53:21Z","file_size":1089651,"file_id":"5482","content_type":"application/pdf","checksum":"62c6ea01e342553dcafb88a070fb1ad5","file_name":"IST-2015-319-v1+1_long.pdf","access_level":"open_access","relation":"main_file"}],"publication_status":"published","ddc":[],"publication_identifier":{"issn":[]},"pubrep_id":"319","alternative_title":[],"department":[{"_id":"KrCh","tree":[{"_id":"ResearchGroups"},{"_id":"IST"}]}],"file_date_updated":"2020-07-14T12:46:52Z","_id":"5430","oa":1,"language":[{}],"date_updated":"2021-01-12T08:02:17Z","type":"technical_report","status":"public","abstract":[{"lang":"eng"}],"month":"02","creator":{"id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","login":"dernst"},"author":[{"last_name":"Chatterjee","orcid":"0000-0002-4561-241X","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Ibsen-Jensen","orcid":"0000-0003-4783-0389","id":"3B699956-F248-11E8-B48F-1D18A9856A87","first_name":"Rasmus"},{"first_name":"Andreas","id":"49704004-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-8943-0722","last_name":"Pavlogiannis"}],"related_material":{"record":[{"id":"1607","relation":"later_version","status":"public"},{"id":"5437","relation":"later_version","status":"public"}]},"oa_version":"Published Version","dc":{"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-319-v1-1"],"date":["2015"],"type":["info:eu-repo/semantics/other","doc-type:other","text","http://purl.org/coar/resource_type/c_1843"],"identifier":["https://research-explorer.app.ist.ac.at/record/5430","https://research-explorer.app.ist.ac.at/download/5430/5482"],"title":["Faster algorithms for quantitative verification in constant treewidth graphs","IST Austria Technical Report"],"relation":["info:eu-repo/semantics/altIdentifier/doi/10.15479/AT:IST-2015-319-v1-1","info:eu-repo/semantics/altIdentifier/issn/2664-1690"],"creator":["Chatterjee, Krishnendu","Ibsen-Jensen, Rasmus","Pavlogiannis, Andreas"],"publisher":["IST Austria"],"language":["eng"],"rights":["info:eu-repo/semantics/openAccess"],"subject":["ddc:000"],"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. The 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. Our main theoretical results are as follows. First, for constant treewidth graphs we present an algorithm that approximates the mean-payoff value within a mul- tiplicative factor of ∊ in time O ( n · log( n/∊ )) 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 · log( | a · b · n | )) = O ( n · log( n · W )) , when the output is a b , as compared to the previously best known algorithm with running time O ( n 2 · log( n · W )) . Third, for the minimum initial credit problem we show that (i) for general graphs the problem can be solved in O ( n 2 · m ) time and the associated decision problem can be solved in O ( n · m ) time, improving the previous known O ( n 3 · m · log( n · W )) and O ( n 2 · m ) bounds, respectively; and (ii) for constant treewidth graphs we present an algorithm that requires O ( n · log n ) time, improving the previous known O ( n 4 · log( n · W )) bound. We have implemented some of our algorithms and show that they present a significant speedup on standard benchmarks."]},"date_created":"2018-12-12T11:39:17Z","has_accepted_license":"1","uri_base":"https://research-explorer.app.ist.ac.at","page":"31","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87"}]