---
res:
bibo_abstract:
- "Product graphs arise naturally in formal verification and program analysis. For
example, the analysis of two concurrent threads requires the product of two component
control-flow graphs, and for language inclusion of deterministic automata the
product of two automata is constructed. In many cases, the component graphs have
constant treewidth, e.g., when the input contains control-flow graphs of programs.
We consider the algorithmic analysis of products of two constant-treewidth graphs
with respect to three classic specification languages, namely, (a) algebraic properties,
(b) mean-payoff properties, and (c) initial credit for energy properties.\r\nOur
main contributions are as follows. Consider a graph G that is the product of two
constant-treewidth graphs of size n each. First, given an idempotent semiring,
we present an algorithm that computes the semiring transitive closure of G in
time Õ(n⁴). Since the output has size Θ(n⁴), our algorithm is optimal (up to
polylog factors). Second, given a mean-payoff objective, we present an O(n³)-time
algorithm for deciding whether the value of a starting state is non-negative,
improving the previously known O(n⁴) bound. Third, given an initial credit for
energy objective, we present an O(n⁵)-time algorithm for computing the minimum
initial credit for all nodes of G, improving the previously known O(n⁸) bound.
At the heart of our approach lies an algorithm for the efficient construction
of strongly-balanced tree decompositions of constant-treewidth graphs. Given a
constant-treewidth graph G' of n nodes and a positive integer λ, our algorithm
constructs a binary tree decomposition of G' of width O(λ) with the property that
the size of each subtree decreases geometrically with rate (1/2 + 2^{-λ}).@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.4230/LIPIcs.FSTTCS.2021.42
bibo_volume: 213
dct_date: 2021^xs_gYear
dct_isPartOf:
- http://id.crossref.org/issn/1868-8969
- http://id.crossref.org/issn/978-3-9597-7215-0
dct_language: eng
dct_publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik@
dct_title: Quantitative verification on product graphs of small treewidth@
...