Faster algorithms for quantitative verification in bounded treewidth graphs



Chatterjee, Krishnendu, Ibsen-Jensen, Rasmus ORCID: 0000-0003-4783-0389 and Pavlogiannis, Andreas
(2021) Faster algorithms for quantitative verification in bounded treewidth graphs. Formal Methods in System Design, 57 (3). pp. 401-428.

Access the full-text of this item by clicking on the Open Access link.

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 m= O(n)) 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 O(n2· m) time and the associated decision problem in O(n· m) time, improving the previous known O(n3· m· log (n· W)) and O(n2· m) bounds, respectively; and (2) for bounded treewidth graphs we present an algorithm that requires O(n· log n) time. Second, for bounded treewidth graphs we present an algorithm that approximates the mean-payoff value within a factor of 1 + ϵ in time O(n· log (n/ ϵ)) 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 O(n· log (| a· b|)) = O(n· log (n· W)) , when the output is ab, as compared to the previously best known algorithm on general graphs with running time O(n2· log (n· W)). We have implemented some of our algorithms and show that they present a significant speedup on standard benchmarks.

Item Type: Article
Uncontrolled Keywords: Quantitative verification, Minimum mean cycle, Minimum ratio cycle, Constant treewidth graphs, Initial credit for energy
Divisions: Faculty of Science and Engineering > School of Electrical Engineering, Electronics and Computer Science
Depositing User: Symplectic Admin
Date Deposited: 28 May 2021 07:34
Last Modified: 24 Nov 2023 11:51
DOI: 10.1007/s10703-021-00373-5
Open Access URL: https://arxiv.org/pdf/1504.07384.pdf
Related URLs:
URI: https://livrepository.liverpool.ac.uk/id/eprint/3124228