---
_id: '5437'
abstract:
- lang: eng
text: "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.
\r\nThe 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.\r\nOur main
theoretical results are as follows.\r\nFirst, 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.\r\nWe have implemented
some of our algorithms and show that they present a significant speedup on standard
benchmarks. "
alternative_title:
- IST Austria Technical Report
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Rasmus
full_name: Ibsen-Jensen, Rasmus
id: 3B699956-F248-11E8-B48F-1D18A9856A87
last_name: Ibsen-Jensen
orcid: 0000-0003-4783-0389
- first_name: Andreas
full_name: Pavlogiannis, Andreas
id: 49704004-F248-11E8-B48F-1D18A9856A87
last_name: Pavlogiannis
orcid: 0000-0002-8943-0722
citation:
ama: 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-1
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-330-v2-1
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-330-v2-1.
ieee: K. Chatterjee, R. Ibsen-Jensen, and A. Pavlogiannis, *Faster algorithms
for quantitative verification in constant treewidth graphs*. IST Austria, 2015.
ista: Chatterjee K, Ibsen-Jensen R, Pavlogiannis A. 2015. Faster algorithms for
quantitative verification in constant treewidth graphs, IST Austria, 27p.
mla: 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.
short: K. Chatterjee, R. Ibsen-Jensen, A. Pavlogiannis, Faster Algorithms for Quantitative
Verification in Constant Treewidth Graphs, IST Austria, 2015.
date_created: 2018-12-12T11:39:19Z
date_published: 2015-04-27T00:00:00Z
date_updated: 2024-10-09T20:56:10Z
day: '27'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.15479/AT:IST-2015-330-v2-1
file:
- access_level: open_access
checksum: f5917c20f84018b362d385c000a2e123
content_type: application/pdf
creator: system
date_created: 2018-12-12T11:53:12Z
date_updated: 2020-07-14T12:46:54Z
file_id: '5473'
file_name: IST-2015-330-v2+1_main.pdf
file_size: 1072137
relation: main_file
file_date_updated: 2020-07-14T12:46:54Z
has_accepted_license: '1'
language:
- iso: eng
month: '04'
oa: 1
oa_version: Published Version
page: '27'
publication_identifier:
issn:
- 2664-1690
publication_status: published
publisher: IST Austria
pubrep_id: '333'
related_material:
record:
- id: '5430'
relation: earlier_version
status: public
- id: '1607'
relation: later_version
status: public
status: public
title: Faster algorithms for quantitative verification in constant treewidth graphs
type: technical_report
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2015'
...