---
_id: '9393'
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,
    the ratio, 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 bounded treewidth—a class that contains the control flow graphs of
    most programs. Let n denote the number of nodes of a graph, m the number of edges
    (for bounded treewidth \U0001D45A=\U0001D442(\U0001D45B)) and W the largest absolute
    value of the weights. Our main theoretical results are as follows. First, for
    the minimum initial credit problem we show that (1) for general graphs the problem
    can be solved in \U0001D442(\U0001D45B2⋅\U0001D45A) time and the associated decision
    problem in \U0001D442(\U0001D45B⋅\U0001D45A) time, improving the previous known
    \U0001D442(\U0001D45B3⋅\U0001D45A⋅log(\U0001D45B⋅\U0001D44A)) and \U0001D442(\U0001D45B2⋅\U0001D45A)
    bounds, respectively; and (2) for bounded treewidth graphs we present an algorithm
    that requires \U0001D442(\U0001D45B⋅log\U0001D45B) time. Second, for bounded treewidth
    graphs we present an algorithm that approximates the mean-payoff value within
    a factor of 1+\U0001D716 in time \U0001D442(\U0001D45B⋅log(\U0001D45B/\U0001D716))
    as compared to the classical exact algorithms on general graphs that require quadratic
    time. Third, for the ratio property we present an algorithm that for bounded treewidth
    graphs works in time \U0001D442(\U0001D45B⋅log(|\U0001D44E⋅\U0001D44F|))=\U0001D442(\U0001D45B⋅log(\U0001D45B⋅\U0001D44A)),
    when the output is \U0001D44E\U0001D44F, as compared to the previously best known
    algorithm on general graphs with running time \U0001D442(\U0001D45B2⋅log(\U0001D45B⋅\U0001D44A)).
    We have implemented some of our algorithms and show that they present a significant
    speedup on standard benchmarks."
acknowledgement: 'The research was partly supported by Austrian Science Fund (FWF)
  Grant No P23499- N23, FWF NFN Grant No S11407-N23 (RiSE/SHiNE), ERC Start Grant
  (279307: Graph Games), and Microsoft faculty fellows award.'
article_processing_charge: No
article_type: original
arxiv: 1
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 bounded treewidth graphs. <i>Formal Methods in System Design</i>.
    2021;57:401-428. doi:<a href="https://doi.org/10.1007/s10703-021-00373-5">10.1007/s10703-021-00373-5</a>
  apa: Chatterjee, K., Ibsen-Jensen, R., &#38; Pavlogiannis, A. (2021). Faster algorithms
    for quantitative verification in bounded treewidth graphs. <i>Formal Methods in
    System Design</i>. Springer. <a href="https://doi.org/10.1007/s10703-021-00373-5">https://doi.org/10.1007/s10703-021-00373-5</a>
  chicago: Chatterjee, Krishnendu, Rasmus Ibsen-Jensen, and Andreas Pavlogiannis.
    “Faster Algorithms for Quantitative Verification in Bounded Treewidth Graphs.”
    <i>Formal Methods in System Design</i>. Springer, 2021. <a href="https://doi.org/10.1007/s10703-021-00373-5">https://doi.org/10.1007/s10703-021-00373-5</a>.
  ieee: K. Chatterjee, R. Ibsen-Jensen, and A. Pavlogiannis, “Faster algorithms for
    quantitative verification in bounded treewidth graphs,” <i>Formal Methods in System
    Design</i>, vol. 57. Springer, pp. 401–428, 2021.
  ista: Chatterjee K, Ibsen-Jensen R, Pavlogiannis A. 2021. Faster algorithms for
    quantitative verification in bounded treewidth graphs. Formal Methods in System
    Design. 57, 401–428.
  mla: Chatterjee, Krishnendu, et al. “Faster Algorithms for Quantitative Verification
    in Bounded Treewidth Graphs.” <i>Formal Methods in System Design</i>, vol. 57,
    Springer, 2021, pp. 401–28, doi:<a href="https://doi.org/10.1007/s10703-021-00373-5">10.1007/s10703-021-00373-5</a>.
  short: K. Chatterjee, R. Ibsen-Jensen, A. Pavlogiannis, Formal Methods in System
    Design 57 (2021) 401–428.
date_created: 2021-05-16T22:01:47Z
date_published: 2021-09-01T00:00:00Z
date_updated: 2025-04-15T07:23:30Z
day: '01'
department:
- _id: KrCh
doi: 10.1007/s10703-021-00373-5
ec_funded: 1
external_id:
  arxiv:
  - '1504.07384'
  isi:
  - '000645490300001'
intvolume: '        57'
isi: 1
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: https://arxiv.org/abs/1504.07384
month: '09'
oa: 1
oa_version: Preprint
page: 401-428
project:
- _id: 2584A770-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: P 23499-N23
  name: Modern Graph Algorithmic Techniques in Formal Verification
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: S 11407_N23
  name: Rigorous Systems Engineering
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '279307'
  name: 'Quantitative Graph Games: Theory and Applications'
- _id: 2587B514-B435-11E9-9278-68D0E5697425
  name: Microsoft Research Faculty Fellowship
publication: Formal Methods in System Design
publication_identifier:
  eissn:
  - 1572-8102
  issn:
  - 0925-9856
publication_status: published
publisher: Springer
quality_controlled: '1'
scopus_import: '1'
status: public
title: Faster algorithms for quantitative verification in bounded treewidth graphs
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 57
year: '2021'
...