---
_id: '1194'
abstract:
- lang: eng
  text: 'Termination is one of the basic liveness properties, and we study the termination
    problem for probabilistic programs with real-valued variables. Previous works
    focused on the qualitative problem that asks whether an input program terminates
    with probability~1 (almost-sure termination). A powerful approach for this qualitative
    problem is the notion of ranking supermartingales with respect to a given set
    of invariants. The quantitative problem (probabilistic termination) asks for bounds
    on the termination probability. A fundamental and conceptual drawback of the existing
    approaches to address probabilistic termination is that even though the supermartingales
    consider the probabilistic behavior of the programs, the invariants are obtained
    completely ignoring the probabilistic aspect. In this work we address the probabilistic
    termination problem for linear-arithmetic probabilistic programs with nondeterminism.
    We define the notion of {\em stochastic invariants}, which are constraints along
    with a probability bound that the constraints hold. We introduce a concept of
    {\em repulsing supermartingales}. First, we show that repulsing supermartingales
    can be used to obtain bounds on the probability of the stochastic invariants.
    Second, we show the effectiveness of repulsing supermartingales in the following
    three ways: (1)~With a combination of ranking and repulsing supermartingales we
    can compute lower bounds on the probability of termination; (2)~repulsing supermartingales
    provide witnesses for refutation of almost-sure termination; and (3)~with a combination
    of ranking and repulsing supermartingales we can establish persistence properties
    of probabilistic programs. We also present results on related computational problems
    and an experimental evaluation of our approach on academic examples. '
alternative_title:
- ACM SIGPLAN Notices
article_processing_charge: No
author:
- first_name: Krishnendu
  full_name: Chatterjee, Krishnendu
  id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
  last_name: Chatterjee
  orcid: 0000-0002-4561-241X
- first_name: Petr
  full_name: Novotny, Petr
  id: 3CC3B868-F248-11E8-B48F-1D18A9856A87
  last_name: Novotny
- first_name: Djordje
  full_name: Zikelic, Djordje
  last_name: Zikelic
citation:
  ama: 'Chatterjee K, Novotný P, Zikelic D. Stochastic invariants for probabilistic
    termination. In: Vol 52. ACM; 2017:145-160. doi:<a href="https://doi.org/10.1145/3009837.3009873">10.1145/3009837.3009873</a>'
  apa: 'Chatterjee, K., Novotný, P., &#38; Zikelic, D. (2017). Stochastic invariants
    for probabilistic termination (Vol. 52, pp. 145–160). Presented at the POPL: Principles
    of Programming Languages, Paris, France: ACM. <a href="https://doi.org/10.1145/3009837.3009873">https://doi.org/10.1145/3009837.3009873</a>'
  chicago: Chatterjee, Krishnendu, Petr Novotný, and Djordje Zikelic. “Stochastic
    Invariants for Probabilistic Termination,” 52:145–60. ACM, 2017. <a href="https://doi.org/10.1145/3009837.3009873">https://doi.org/10.1145/3009837.3009873</a>.
  ieee: 'K. Chatterjee, P. Novotný, and D. Zikelic, “Stochastic invariants for probabilistic
    termination,” presented at the POPL: Principles of Programming Languages, Paris,
    France, 2017, vol. 52, no. 1, pp. 145–160.'
  ista: 'Chatterjee K, Novotný P, Zikelic D. 2017. Stochastic invariants for probabilistic
    termination. POPL: Principles of Programming Languages, ACM SIGPLAN Notices, vol.
    52, 145–160.'
  mla: Chatterjee, Krishnendu, et al. <i>Stochastic Invariants for Probabilistic Termination</i>.
    Vol. 52, no. 1, ACM, 2017, pp. 145–60, doi:<a href="https://doi.org/10.1145/3009837.3009873">10.1145/3009837.3009873</a>.
  short: K. Chatterjee, P. Novotný, D. Zikelic, in:, ACM, 2017, pp. 145–160.
conference:
  end_date: 2017-01-21
  location: Paris, France
  name: 'POPL: Principles of Programming Languages'
  start_date: 2017-01-15
date_created: 2018-12-11T11:50:39Z
date_published: 2017-01-01T00:00:00Z
date_updated: 2025-07-14T09:09:58Z
day: '01'
department:
- _id: KrCh
doi: 10.1145/3009837.3009873
ec_funded: 1
external_id:
  isi:
  - '000408311200013'
intvolume: '        52'
isi: 1
issue: '1'
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: https://arxiv.org/abs/1611.01063
month: '01'
oa: 1
oa_version: Submitted Version
page: 145 - 160
project:
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: S 11407_N23
  name: Rigorous Systems Engineering
- _id: 25F5A88A-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: S11402-N23
  name: Moderne Concurrency Paradigms
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '279307'
  name: 'Quantitative Graph Games: Theory and Applications'
- _id: 25681D80-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '291734'
  name: International IST Postdoc Fellowship Programme
publication_identifier:
  issn:
  - '07308566'
publication_status: published
publisher: ACM
publist_id: '6157'
quality_controlled: '1'
related_material:
  record:
  - id: '14539'
    relation: dissertation_contains
    status: public
scopus_import: '1'
status: public
title: Stochastic invariants for probabilistic termination
type: conference
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
volume: 52
year: '2017'
...