---
res:
bibo_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 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.@eng
bibo_authorlist:
- foaf_Person:
foaf_givenName: Krishnendu
foaf_name: Chatterjee, Krishnendu
foaf_surname: Chatterjee
foaf_workInfoHomepage: http://www.librecat.org/personId=2E5DCA20-F248-11E8-B48F-1D18A9856A87
orcid: 0000-0002-4561-241X
- foaf_Person:
foaf_givenName: Rasmus
foaf_name: Ibsen-Jensen, Rasmus
foaf_surname: Ibsen-Jensen
foaf_workInfoHomepage: http://www.librecat.org/personId=3B699956-F248-11E8-B48F-1D18A9856A87
- foaf_Person:
foaf_givenName: Andreas
foaf_name: Pavlogiannis, Andreas
foaf_surname: Pavlogiannis
foaf_workInfoHomepage: http://www.librecat.org/personId=49704004-F248-11E8-B48F-1D18A9856A87
bibo_doi: 10.15479/AT:IST-2015-319-v1-1
dct_date: 2015^xs_gYear
dct_isPartOf:
- http://id.crossref.org/issn/2664-1690
dct_language: eng
dct_publisher: IST Austria@
dct_title: Faster algorithms for quantitative verification in constant treewidth
graphs@
...