  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.
