TY - GEN

T1 - Quantitative Verification on Product Graphs of Small Treewidth

AU - Chatterjee, Krishnendu

AU - Ibsen-Jensen, Rasmus

AU - Pavlogiannis, Andreas

PY - 2021

Y1 - 2021

N2 - 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. Our 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
4). Since the output has size Θ(n
4), our algorithm is optimal (up to polylog factors). Second, given a mean-payoff objective, we present an O(n
3)-time algorithm for deciding whether the value of a starting state is non-negative, improving the previously known O(n
4) bound. Third, given an initial credit for energy objective, we present an O(n
5)-time algorithm for computing the minimum initial credit for all nodes of G, improving the previously known O(n
8) 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
-λ).

AB - 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. Our 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
4). Since the output has size Θ(n
4), our algorithm is optimal (up to polylog factors). Second, given a mean-payoff objective, we present an O(n
3)-time algorithm for deciding whether the value of a starting state is non-negative, improving the previously known O(n
4) bound. Third, given an initial credit for energy objective, we present an O(n
5)-time algorithm for computing the minimum initial credit for all nodes of G, improving the previously known O(n
8) 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
-λ).

KW - Algebraic paths

KW - Graph algorithms

KW - Initial credit for energy

KW - Mean-payoff

U2 - 10.4230/LIPIcs.FSTTCS.2021.42

DO - 10.4230/LIPIcs.FSTTCS.2021.42

M3 - Article in proceedings

SN - 978-3-95977-215-0

VL - ´

T3 - Leibniz International Proceedings in Informatics

SP - 42:1-42:23

BT - 41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2021)

ER -