Earlier Version

# Faster algorithms for quantitative verification in constant treewidth graphs

K. Chatterjee, R. Ibsen-Jensen, A. Pavlogiannis, Faster Algorithms for Quantitative Verification in Constant Treewidth Graphs, IST Austria, 2015.

Download

IST-2015-330-v2+1_main.pdf
1.07 MB

*Technical Report*|

*Published*|

*English*

Author

Department

Series Title

IST Austria Technical Report

Abstract

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 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.
We have implemented some of our algorithms and show that they present a significant speedup on standard benchmarks.

Publishing Year

Date Published

2015-04-27

Page

27

ISSN

IST-REx-ID

### Cite this

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-1Chatterjee, 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-1Chatterjee, 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.K. Chatterjee, R. Ibsen-Jensen, and A. Pavlogiannis,

*Faster algorithms for quantitative verification in constant treewidth graphs*. IST Austria, 2015.Chatterjee K, Ibsen-Jensen R, Pavlogiannis A. 2015. Faster algorithms for quantitative verification in constant treewidth graphs, IST Austria, 27p.

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.**All files available under the following license(s):**

**Copyright Statement:**

**This Item is protected by copyright and/or related rights.**[...]

**Main File(s)**

File Name

IST-2015-330-v2+1_main.pdf
1.07 MB

Access Level

Open Access

Date Uploaded

2018-12-12

MD5 Checksum

f5917c20f84018b362d385c000a2e123

**Material in IST:**

**Later Version**

**Earlier Version**