Faster algorithms for quantitative verification in bounded treewidth graphs

Chatterjee K, Ibsen-Jensen R, Pavlogiannis A. 2021. Faster algorithms for quantitative verification in bounded treewidth graphs. Formal Methods in System Design.

Download
No fulltext has been uploaded. References only!

Journal Article | Epub ahead of print | English

Scopus indexed
Department
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 π‘š=𝑂(𝑛)) 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 𝑂(𝑛2β‹…π‘š) time and the associated decision problem in 𝑂(π‘›β‹…π‘š) time, improving the previous known 𝑂(𝑛3β‹…π‘šβ‹…log(π‘›β‹…π‘Š)) and 𝑂(𝑛2β‹…π‘š) bounds, respectively; and (2) for bounded treewidth graphs we present an algorithm that requires 𝑂(𝑛⋅log𝑛) time. Second, for bounded treewidth graphs we present an algorithm that approximates the mean-payoff value within a factor of 1+πœ– in time 𝑂(𝑛⋅log(𝑛/πœ–)) 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 𝑂(𝑛⋅log(|π‘Žβ‹…π‘|))=𝑂(𝑛⋅log(π‘›β‹…π‘Š)), when the output is π‘Žπ‘, as compared to the previously best known algorithm on general graphs with running time 𝑂(𝑛2β‹…log(π‘›β‹…π‘Š)). We have implemented some of our algorithms and show that they present a significant speedup on standard benchmarks.
Publishing Year
Date Published
2021-04-29
Journal Title
Formal Methods in System Design
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.
ISSN
eISSN
IST-REx-ID

Cite this

Chatterjee K, Ibsen-Jensen R, Pavlogiannis A. Faster algorithms for quantitative verification in bounded treewidth graphs. Formal Methods in System Design. 2021. doi:10.1007/s10703-021-00373-5
Chatterjee, K., Ibsen-Jensen, R., & Pavlogiannis, A. (2021). Faster algorithms for quantitative verification in bounded treewidth graphs. Formal Methods in System Design. Springer. https://doi.org/10.1007/s10703-021-00373-5
Chatterjee, Krishnendu, Rasmus Ibsen-Jensen, and Andreas Pavlogiannis. β€œFaster Algorithms for Quantitative Verification in Bounded Treewidth Graphs.” Formal Methods in System Design. Springer, 2021. https://doi.org/10.1007/s10703-021-00373-5.
K. Chatterjee, R. Ibsen-Jensen, and A. Pavlogiannis, β€œFaster algorithms for quantitative verification in bounded treewidth graphs,” Formal Methods in System Design. Springer, 2021.
Chatterjee K, Ibsen-Jensen R, Pavlogiannis A. 2021. Faster algorithms for quantitative verification in bounded treewidth graphs. Formal Methods in System Design.
Chatterjee, Krishnendu, et al. β€œFaster Algorithms for Quantitative Verification in Bounded Treewidth Graphs.” Formal Methods in System Design, Springer, 2021, doi:10.1007/s10703-021-00373-5.

Export

Marked Publications

Open Data IST Research Explorer

Search this title in

Google Scholar