Quantitative bounds on resource usage of probabilistic programs

Cost analysis, also known as resource usage analysis, is the task of finding bounds on the total cost of a program and is a well-studied problem in static analysis. In this work, we consider two classical quantitative problems in cost analysis for probabilistic programs. The first problem is to find...

Full description

Saved in:
Bibliographic Details
Main Authors: CHATTERJEE, Krishnendu, GOHARSHADY, Amir Kafshdar, MEGGENDORFER, Tobias, ZIKELIC, Dorde
Format: text
Language:English
Published: Institutional Knowledge at Singapore Management University 2026
Subjects:
Online Access:https://ink.library.smu.edu.sg/sis_research/9073
https://ink.library.smu.edu.sg/context/sis_research/article/10076/viewcontent/3649824.pdf
Tags: Add Tag
No Tags, Be the first to tag this record!
Institution: Singapore Management University
Language: English
id sg-smu-ink.sis_research-10076
record_format dspace
spelling sg-smu-ink.sis_research-100762024-08-01T15:22:08Z Quantitative bounds on resource usage of probabilistic programs CHATTERJEE, Krishnendu GOHARSHADY, Amir Kafshdar MEGGENDORFER, Tobias ZIKELIC, Dorde Cost analysis, also known as resource usage analysis, is the task of finding bounds on the total cost of a program and is a well-studied problem in static analysis. In this work, we consider two classical quantitative problems in cost analysis for probabilistic programs. The first problem is to find a bound on the expected total cost of the program. This is a natural measure for the resource usage of the program and can also be directly applied to average-case runtime analysis. The second problem asks for a tail bound, i.e. ‍given a threshold t the goal is to find a probability bound p such that ℙ[total cost ≥ t] ≤ p. Intuitively, given a threshold t on the resource, the problem is to find the likelihood that the total cost exceeds this threshold.First, for expectation bounds, a major obstacle in previous works on cost analysis is that they can handle only non-negative costs or bounded variable updates. In contrast, we provide a new variant of the standard notion of cost martingales, that allows us to find expectation bounds for a class of programs with general positive or negative costs and no restriction on the variable updates. More specifically, our approach is applicable as long as there is a lower bound on the total cost incurred along every path.Second, for tail bounds, all previous methods are limited to programs in which the expected total cost is finite. In contrast, we present a novel approach, based on a combination of our martingale-based method for expectation bounds with a quantitative safety analysis, to obtain a solution to the tail bound problem that is applicable even to programs with infinite expected cost. Specifically, this allows us to obtain runtime tail bounds for programs that do not terminate almost-surely.In summary, we provide a novel combination of martingale-based cost analysis and quantitative safety analysis that is able to find expectation and tail cost bounds for probabilistic programs, without the restrictions of non-negative costs, bounded updates, or finiteness of the expected total cost. Finally, we provide experimental results showcasing that our approach can solve instances that were beyond the reach of previous methods. 2026-05-01T07:00:00Z text application/pdf https://ink.library.smu.edu.sg/sis_research/9073 info:doi/10.1145/3649824 https://ink.library.smu.edu.sg/context/sis_research/article/10076/viewcontent/3649824.pdf http://creativecommons.org/licenses/by-nc-nd/4.0/ Research Collection School Of Computing and Information Systems eng Institutional Knowledge at Singapore Management University Probabilistic Programming Static Analysis Quantitative Bounds Cost Analysis Martingales Programming Languages and Compilers
institution Singapore Management University
building SMU Libraries
continent Asia
country Singapore
Singapore
content_provider SMU Libraries
collection InK@SMU
language English
topic Probabilistic Programming
Static Analysis
Quantitative Bounds
Cost Analysis
Martingales
Programming Languages and Compilers
spellingShingle Probabilistic Programming
Static Analysis
Quantitative Bounds
Cost Analysis
Martingales
Programming Languages and Compilers
CHATTERJEE, Krishnendu
GOHARSHADY, Amir Kafshdar
MEGGENDORFER, Tobias
ZIKELIC, Dorde
Quantitative bounds on resource usage of probabilistic programs
description Cost analysis, also known as resource usage analysis, is the task of finding bounds on the total cost of a program and is a well-studied problem in static analysis. In this work, we consider two classical quantitative problems in cost analysis for probabilistic programs. The first problem is to find a bound on the expected total cost of the program. This is a natural measure for the resource usage of the program and can also be directly applied to average-case runtime analysis. The second problem asks for a tail bound, i.e. ‍given a threshold t the goal is to find a probability bound p such that ℙ[total cost ≥ t] ≤ p. Intuitively, given a threshold t on the resource, the problem is to find the likelihood that the total cost exceeds this threshold.First, for expectation bounds, a major obstacle in previous works on cost analysis is that they can handle only non-negative costs or bounded variable updates. In contrast, we provide a new variant of the standard notion of cost martingales, that allows us to find expectation bounds for a class of programs with general positive or negative costs and no restriction on the variable updates. More specifically, our approach is applicable as long as there is a lower bound on the total cost incurred along every path.Second, for tail bounds, all previous methods are limited to programs in which the expected total cost is finite. In contrast, we present a novel approach, based on a combination of our martingale-based method for expectation bounds with a quantitative safety analysis, to obtain a solution to the tail bound problem that is applicable even to programs with infinite expected cost. Specifically, this allows us to obtain runtime tail bounds for programs that do not terminate almost-surely.In summary, we provide a novel combination of martingale-based cost analysis and quantitative safety analysis that is able to find expectation and tail cost bounds for probabilistic programs, without the restrictions of non-negative costs, bounded updates, or finiteness of the expected total cost. Finally, we provide experimental results showcasing that our approach can solve instances that were beyond the reach of previous methods.
format text
author CHATTERJEE, Krishnendu
GOHARSHADY, Amir Kafshdar
MEGGENDORFER, Tobias
ZIKELIC, Dorde
author_facet CHATTERJEE, Krishnendu
GOHARSHADY, Amir Kafshdar
MEGGENDORFER, Tobias
ZIKELIC, Dorde
author_sort CHATTERJEE, Krishnendu
title Quantitative bounds on resource usage of probabilistic programs
title_short Quantitative bounds on resource usage of probabilistic programs
title_full Quantitative bounds on resource usage of probabilistic programs
title_fullStr Quantitative bounds on resource usage of probabilistic programs
title_full_unstemmed Quantitative bounds on resource usage of probabilistic programs
title_sort quantitative bounds on resource usage of probabilistic programs
publisher Institutional Knowledge at Singapore Management University
publishDate 2026
url https://ink.library.smu.edu.sg/sis_research/9073
https://ink.library.smu.edu.sg/context/sis_research/article/10076/viewcontent/3649824.pdf
_version_ 1814047724140494848