---
_id: '6175'
abstract:
- lang: eng
  text: "We consider the problem of expected cost analysis over nondeterministic probabilistic
    programs,\r\nwhich aims at automated methods for analyzing the resource-usage
    of such programs.\r\nPrevious approaches for this problem could only handle nonnegative
    bounded costs.\r\nHowever, in many scenarios, such as queuing networks or analysis
    of cryptocurrency protocols,\r\nboth positive and negative costs are necessary
    and the costs are unbounded as well.\r\n\r\nIn this work, we present a sound and
    efficient approach to obtain polynomial bounds on the\r\nexpected accumulated
    cost of nondeterministic probabilistic programs.\r\nOur approach can handle (a)
    general positive and negative costs with bounded updates in\r\nvariables; and
    (b) nonnegative costs with general updates to variables.\r\nWe show that several
    natural examples which could not be\r\nhandled by previous approaches are captured
    in our framework.\r\n\r\nMoreover, our approach leads to an efficient polynomial-time
    algorithm, while no\r\nprevious approach for cost analysis of probabilistic programs
    could guarantee polynomial runtime.\r\nFinally, we show the effectiveness of our
    approach using experimental results on a variety of programs for which we efficiently
    synthesize tight resource-usage bounds."
article_processing_charge: No
arxiv: 1
author:
- first_name: Peixin
  full_name: Wang, Peixin
  last_name: Wang
- first_name: Hongfei
  full_name: Fu, Hongfei
  id: 3AAD03D6-F248-11E8-B48F-1D18A9856A87
  last_name: Fu
- first_name: Amir Kafshdar
  full_name: Goharshady, Amir Kafshdar
  id: 391365CE-F248-11E8-B48F-1D18A9856A87
  last_name: Goharshady
  orcid: 0000-0003-1702-6584
- first_name: Krishnendu
  full_name: Chatterjee, Krishnendu
  id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
  last_name: Chatterjee
  orcid: 0000-0002-4561-241X
- first_name: Xudong
  full_name: Qin, Xudong
  last_name: Qin
- first_name: Wenjun
  full_name: Shi, Wenjun
  last_name: Shi
citation:
  ama: '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>'
  apa: '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>'
  chicago: '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>.'
  ieee: '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.'
  ista: '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.'
  mla: '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>.'
  short: '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.'
conference:
  end_date: 2019-06-26
  location: Phoenix, AZ, United States
  name: 'PLDI: Conference on Programming Language Design and Implementation'
  start_date: 2019-06-22
date_created: 2019-03-25T10:13:25Z
date_published: 2019-06-08T00:00:00Z
date_updated: 2025-06-02T08:53:45Z
day: '08'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.1145/3314221.3314581
ec_funded: 1
external_id:
  arxiv:
  - '1902.04659'
  isi:
  - '000523190300014'
file:
- access_level: open_access
  checksum: 703a5e9b8c8587f2a44085ffd9a4db64
  content_type: application/pdf
  creator: akafshda
  date_created: 2019-03-25T10:11:22Z
  date_updated: 2020-07-14T12:47:20Z
  file_id: '6176'
  file_name: paper.pdf
  file_size: 4051066
  relation: main_file
file_date_updated: 2020-07-14T12:47:20Z
has_accepted_license: '1'
isi: 1
keyword:
- Program Cost Analysis
- Program Termination
- Probabilistic Programs
- Martingales
language:
- iso: eng
month: '06'
oa: 1
oa_version: Submitted Version
page: 204-220
project:
- _id: 25892FC0-B435-11E9-9278-68D0E5697425
  grant_number: ICT15-003
  name: Efficient Algorithms for Computer Aided Verification
- _id: 25863FF4-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: S11407
  name: Game Theory
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: S 11407_N23
  name: Rigorous Systems Engineering
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '279307'
  name: 'Quantitative Graph Games: Theory and Applications'
- _id: 266EEEC0-B435-11E9-9278-68D0E5697425
  name: Quantitative Game-theoretic Analysis of Blockchain Applications and Smart
    Contracts
publication: 'PLDI 2019: Proceedings of the 40th ACM SIGPLAN Conference on Programming
  Language Design and Implementation'
publication_status: published
publisher: Association for Computing Machinery
quality_controlled: '1'
related_material:
  record:
  - id: '5457'
    relation: earlier_version
    status: public
  - id: '8934'
    relation: dissertation_contains
    status: public
scopus_import: '1'
status: public
title: Cost analysis of nondeterministic probabilistic programs
type: conference
user_id: 4359f0d1-fa6c-11eb-b949-802e58b17ae8
year: '2019'
...