Faster algorithms for quantitative verification in constant treewidth graphs
IST Austria Technical Report
published
Krishnendu
Chatterjee
author 2E5DCA20-F248-11E8-B48F-1D18A9856A870000-0002-4561-241X
Rasmus
Ibsen-Jensen
author 3B699956-F248-11E8-B48F-1D18A9856A87
Andreas
Pavlogiannis
author 49704004-F248-11E8-B48F-1D18A9856A87
KrCh
department
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.
/download/5430/5482/IST-2015-319-v1+1_long.pdf
application/pdfno
IST Austria2015
eng
2664-169010.15479/AT:IST-2015-319-v1-1
31
/record/5437 /record/1607
Chatterjee, Krishnendu, et al. <i>Faster Algorithms for Quantitative Verification in Constant Treewidth Graphs</i>. IST Austria, 2015, doi:<a href="https://doi.org/10.15479/AT:IST-2015-319-v1-1">10.15479/AT:IST-2015-319-v1-1</a>.
Chatterjee, Krishnendu, Rasmus Ibsen-Jensen, and Andreas Pavlogiannis. <i>Faster Algorithms for Quantitative Verification in Constant Treewidth Graphs</i>. IST Austria, 2015. <a href="https://doi.org/10.15479/AT:IST-2015-319-v1-1">https://doi.org/10.15479/AT:IST-2015-319-v1-1</a>.
K. Chatterjee, R. Ibsen-Jensen, A. Pavlogiannis, Faster Algorithms for Quantitative Verification in Constant Treewidth Graphs, IST Austria, 2015.
Chatterjee, K., Ibsen-Jensen, R., & Pavlogiannis, A. (2015). <i>Faster algorithms for quantitative verification in constant treewidth graphs</i>. IST Austria. <a href="https://doi.org/10.15479/AT:IST-2015-319-v1-1">https://doi.org/10.15479/AT:IST-2015-319-v1-1</a>
K. Chatterjee, R. Ibsen-Jensen, and A. Pavlogiannis, <i>Faster algorithms for quantitative verification in constant treewidth graphs</i>. IST Austria, 2015.
Chatterjee K, Ibsen-Jensen R, Pavlogiannis A. <i>Faster Algorithms for Quantitative Verification in Constant Treewidth Graphs</i>. IST Austria; 2015. doi:<a href="https://doi.org/10.15479/AT:IST-2015-319-v1-1">10.15479/AT:IST-2015-319-v1-1</a>
Chatterjee K, Ibsen-Jensen R, Pavlogiannis A. 2015. Faster algorithms for quantitative verification in constant treewidth graphs, IST Austria, 31p.
54302018-12-12T11:39:17Z2020-01-21T13:18:09Z