---
_id: '12000'
abstract:
- lang: eng
  text: "We consider the quantitative problem of obtaining lower-bounds on the probability
    of termination of a given non-deterministic probabilistic program. Specifically,
    given a non-termination threshold p∈[0,1], we aim for certificates proving that
    the program terminates with probability at least 1−p. The basic idea of our approach
    is to find a terminating stochastic invariant, i.e. a subset SI of program states
    such that (i) the probability of the program ever leaving SI is no more than p,
    and (ii) almost-surely, the program either leaves SI or terminates.\r\n\r\nWhile
    stochastic invariants are already well-known, we provide the first proof that
    the idea above is not only sound, but also complete for quantitative termination
    analysis. We then introduce a novel sound and complete characterization of stochastic
    invariants that enables template-based approaches for easy synthesis of quantitative
    termination certificates, especially in affine or polynomial forms. Finally, by
    combining this idea with the existing martingale-based methods that are relatively
    complete for qualitative termination analysis, we obtain the first automated,
    sound, and relatively complete algorithm for quantitative termination analysis.
    Notably, our completeness guarantees for quantitative termination analysis are
    as strong as the best-known methods for the qualitative variant.\r\n\r\nOur prototype
    implementation demonstrates the effectiveness of our approach on various probabilistic
    programs. We also demonstrate that our algorithm certifies lower bounds on termination
    probability for probabilistic programs that are beyond the reach of previous methods."
acknowledgement: This research was partially supported by the ERC CoG 863818 (ForM-SMArt),
  the HKUST-Kaisa Joint Research Institute Project Grant HKJRI3A-055, the HKUST Startup
  Grant R9272 and the European Union’s Horizon 2020 research and innovation programme
  under the Marie Skłodowska-Curie Grant Agreement No. 665385.
alternative_title:
- LNCS
article_processing_charge: Yes (in subscription journal)
author:
- first_name: Krishnendu
  full_name: Chatterjee, Krishnendu
  id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
  last_name: Chatterjee
  orcid: 0000-0002-4561-241X
- 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: Tobias
  full_name: Meggendorfer, Tobias
  id: b21b0c15-30a2-11eb-80dc-f13ca25802e1
  last_name: Meggendorfer
  orcid: 0000-0002-1712-2165
- first_name: Dorde
  full_name: Zikelic, Dorde
  id: 294AA7A6-F248-11E8-B48F-1D18A9856A87
  last_name: Zikelic
  orcid: 0000-0002-4681-1699
citation:
  ama: 'Chatterjee K, Goharshady AK, Meggendorfer T, Zikelic D. Sound and complete
    certificates for auantitative termination analysis of probabilistic programs.
    In: <i>Proceedings of the 34th International Conference on Computer Aided Verification</i>.
    Vol 13371. Springer; 2022:55-78. doi:<a href="https://doi.org/10.1007/978-3-031-13185-1_4">10.1007/978-3-031-13185-1_4</a>'
  apa: 'Chatterjee, K., Goharshady, A. K., Meggendorfer, T., &#38; Zikelic, D. (2022).
    Sound and complete certificates for auantitative termination analysis of probabilistic
    programs. In <i>Proceedings of the 34th International Conference on Computer Aided
    Verification</i> (Vol. 13371, pp. 55–78). Haifa, Israel: Springer. <a href="https://doi.org/10.1007/978-3-031-13185-1_4">https://doi.org/10.1007/978-3-031-13185-1_4</a>'
  chicago: Chatterjee, Krishnendu, Amir Kafshdar Goharshady, Tobias Meggendorfer,
    and Dorde Zikelic. “Sound and Complete Certificates for Auantitative Termination
    Analysis of Probabilistic Programs.” In <i>Proceedings of the 34th International
    Conference on Computer Aided Verification</i>, 13371:55–78. Springer, 2022. <a
    href="https://doi.org/10.1007/978-3-031-13185-1_4">https://doi.org/10.1007/978-3-031-13185-1_4</a>.
  ieee: K. Chatterjee, A. K. Goharshady, T. Meggendorfer, and D. Zikelic, “Sound and complete
    certificates for auantitative termination analysis of probabilistic programs,”
    in <i>Proceedings of the 34th International Conference on Computer Aided Verification</i>,
    Haifa, Israel, 2022, vol. 13371, pp. 55–78.
  ista: 'Chatterjee K, Goharshady AK, Meggendorfer T, Zikelic D. 2022. Sound and complete
    certificates for auantitative termination analysis of probabilistic programs.
    Proceedings of the 34th International Conference on Computer Aided Verification.
    CAV: Computer Aided Verification, LNCS, vol. 13371, 55–78.'
  mla: Chatterjee, Krishnendu, et al. “Sound and Complete Certificates for Auantitative
    Termination Analysis of Probabilistic Programs.” <i>Proceedings of the 34th International
    Conference on Computer Aided Verification</i>, vol. 13371, Springer, 2022, pp.
    55–78, doi:<a href="https://doi.org/10.1007/978-3-031-13185-1_4">10.1007/978-3-031-13185-1_4</a>.
  short: K. Chatterjee, A.K. Goharshady, T. Meggendorfer, D. Zikelic, in:, Proceedings
    of the 34th International Conference on Computer Aided Verification, Springer,
    2022, pp. 55–78.
conference:
  end_date: 2022-08-10
  location: Haifa, Israel
  name: 'CAV: Computer Aided Verification'
  start_date: 2022-08-07
date_created: 2022-08-28T22:02:02Z
date_published: 2022-08-07T00:00:00Z
date_updated: 2025-07-14T09:09:58Z
day: '07'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.1007/978-3-031-13185-1_4
ec_funded: 1
external_id:
  isi:
  - '000870304500004'
file:
- access_level: open_access
  checksum: 24e0f810ec52735a90ade95198bc641d
  content_type: application/pdf
  creator: alisjak
  date_created: 2022-08-29T09:17:01Z
  date_updated: 2022-08-29T09:17:01Z
  file_id: '12003'
  file_name: 2022_LNCS_Chatterjee.pdf
  file_size: 505094
  relation: main_file
  success: 1
file_date_updated: 2022-08-29T09:17:01Z
has_accepted_license: '1'
intvolume: '     13371'
isi: 1
language:
- iso: eng
month: '08'
oa: 1
oa_version: Published Version
page: 55-78
project:
- _id: 0599E47C-7A3F-11EA-A408-12923DDC885E
  call_identifier: H2020
  grant_number: '863818'
  name: 'Formal Methods for Stochastic Models: Algorithms and Applications'
- _id: 2564DBCA-B435-11E9-9278-68D0E5697425
  call_identifier: H2020
  grant_number: '665385'
  name: International IST Doctoral Program
publication: Proceedings of the 34th International Conference on Computer Aided Verification
publication_identifier:
  eissn:
  - 1611-3349
  isbn:
  - '9783031131844'
  issn:
  - 0302-9743
publication_status: published
publisher: Springer
quality_controlled: '1'
related_material:
  record:
  - id: '14539'
    relation: dissertation_contains
    status: public
scopus_import: '1'
status: public
title: Sound and complete certificates for auantitative termination analysis of probabilistic
  programs
tmp:
  image: /images/cc_by.png
  legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
  name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
  short: CC BY (4.0)
type: conference
user_id: 4359f0d1-fa6c-11eb-b949-802e58b17ae8
volume: 13371
year: '2022'
...