conference paper published yes Peixin Wang author Hongfei Fu author 3AAD03D6-F248-11E8-B48F-1D18A9856A87 Amir Kafshdar Goharshady author 391365CE-F248-11E8-B48F-1D18A9856A870000-0003-1702-6584 Krishnendu Chatterjee author 2E5DCA20-F248-11E8-B48F-1D18A9856A870000-0002-4561-241X Xudong Qin author Wenjun Shi author KrCh department PLDI: Conference on Programming Language Design and Implementation Efficient Algorithms for Computer Aided Verification project Game Theory project Rigorous Systems Engineering project Quantitative Graph Games: Theory and Applications project Quantitative Game-theoretic Analysis of Blockchain Applications and Smart Contracts project We consider the problem of expected cost analysis over nondeterministic probabilistic programs, which aims at automated methods for analyzing the resource-usage of such programs. Previous approaches for this problem could only handle nonnegative bounded costs. However, in many scenarios, such as queuing networks or analysis of cryptocurrency protocols, both positive and negative costs are necessary and the costs are unbounded as well. In this work, we present a sound and efficient approach to obtain polynomial bounds on the expected accumulated cost of nondeterministic probabilistic programs. Our approach can handle (a) general positive and negative costs with bounded updates in variables; and (b) nonnegative costs with general updates to variables. We show that several natural examples which could not be handled by previous approaches are captured in our framework. Moreover, our approach leads to an efficient polynomial-time algorithm, while no previous approach for cost analysis of probabilistic programs could guarantee polynomial runtime. Finally, we show the effectiveness of our approach using experimental results on a variety of programs for which we efficiently synthesize tight resource-usage bounds. https://research-explorer.ista.ac.at/download/6175/6176/paper.pdf application/pdfno Association for Computing Machinery2019Phoenix, AZ, United States eng Program Cost AnalysisProgram TerminationProbabilistic ProgramsMartingales 1902.04659 00052319030001410.1145/3314221.3314581 204-220 https://research-explorer.ista.ac.at/record/5457 https://research-explorer.ista.ac.at/record/8934 Wang P, Fu H, Goharshady AK, Chatterjee K, Qin X, Shi W. 2019. Cost analysis of nondeterministic probabilistic programs. PLDI 2019: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation. PLDI: Conference on Programming Language Design and Implementation, 204–220. Wang, Peixin, Hongfei Fu, Amir Kafshdar Goharshady, Krishnendu Chatterjee, Xudong Qin, and Wenjun Shi. “Cost Analysis of Nondeterministic Probabilistic Programs.” In <i>PLDI 2019: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation</i>, 204–20. Association for Computing Machinery, 2019. <a href="https://doi.org/10.1145/3314221.3314581">https://doi.org/10.1145/3314221.3314581</a>. P. Wang, H. Fu, A.K. Goharshady, K. Chatterjee, X. Qin, W. Shi, in:, PLDI 2019: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, Association for Computing Machinery, 2019, pp. 204–220. Wang P, Fu H, Goharshady AK, Chatterjee K, Qin X, Shi W. Cost analysis of nondeterministic probabilistic programs. In: <i>PLDI 2019: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation</i>. Association for Computing Machinery; 2019:204-220. doi:<a href="https://doi.org/10.1145/3314221.3314581">10.1145/3314221.3314581</a> Wang, P., Fu, H., Goharshady, A. K., Chatterjee, K., Qin, X., &#38; Shi, W. (2019). Cost analysis of nondeterministic probabilistic programs. In <i>PLDI 2019: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation</i> (pp. 204–220). Phoenix, AZ, United States: Association for Computing Machinery. <a href="https://doi.org/10.1145/3314221.3314581">https://doi.org/10.1145/3314221.3314581</a> Wang, Peixin, et al. “Cost Analysis of Nondeterministic Probabilistic Programs.” <i>PLDI 2019: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation</i>, Association for Computing Machinery, 2019, pp. 204–20, doi:<a href="https://doi.org/10.1145/3314221.3314581">10.1145/3314221.3314581</a>. P. Wang, H. Fu, A. K. Goharshady, K. Chatterjee, X. Qin, and W. Shi, “Cost analysis of nondeterministic probabilistic programs,” in <i>PLDI 2019: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation</i>, Phoenix, AZ, United States, 2019, pp. 204–220. 61752019-03-25T10:13:25Z2026-09-12T22:31:05Z