---
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,
    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.@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
    orcid: 0000-0003-4783-0389
  - foaf_Person:
      foaf_givenName: Andreas
      foaf_name: Pavlogiannis, Andreas
      foaf_surname: Pavlogiannis
      foaf_workInfoHomepage: http://www.librecat.org/personId=49704004-F248-11E8-B48F-1D18A9856A87
    orcid: 0000-0002-8943-0722
  bibo_doi: 10.1007/s10703-021-00373-5
  bibo_volume: 57
  dct_date: 2021^xs_gYear
  dct_identifier:
  - UT:000645490300001
  dct_isPartOf:
  - http://id.crossref.org/issn/0925-9856
  - http://id.crossref.org/issn/1572-8102
  dct_language: eng
  dct_publisher: Springer@
  dct_title: Faster algorithms for quantitative verification in bounded treewidth
    graphs@
...