---
_id: '10414'
abstract:
- lang: eng
  text: 'We consider the almost-sure (a.s.) termination problem for probabilistic
    programs, which are a stochastic extension of classical imperative programs. Lexicographic
    ranking functions provide a sound and practical approach for termination of non-probabilistic
    programs, and their extension to probabilistic programs is achieved via lexicographic
    ranking supermartingales (LexRSMs). However, LexRSMs introduced in the previous
    work have a limitation that impedes their automation: all of their components
    have to be non-negative in all reachable states. This might result in LexRSM not
    existing even for simple terminating programs. Our contributions are twofold:
    First, we introduce a generalization of LexRSMs which allows for some components
    to be negative. This standard feature of non-probabilistic termination proofs
    was hitherto not known to be sound in the probabilistic setting, as the soundness
    proof requires a careful analysis of the underlying stochastic process. Second,
    we present polynomial-time algorithms using our generalized LexRSMs for proving
    a.s. termination in broad classes of linear-arithmetic programs.'
acknowledgement: This research was partially supported by the ERC CoG 863818 (ForM-SMArt),
  the Czech Science Foundation grant No. GJ19-15134Y, 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: No
arxiv: 1
author:
- first_name: Krishnendu
  full_name: Chatterjee, Krishnendu
  id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
  last_name: Chatterjee
  orcid: 0000-0002-4561-241X
- first_name: Ehsan Kafshdar
  full_name: Goharshady, Ehsan Kafshdar
  last_name: Goharshady
- first_name: Petr
  full_name: Novotný, Petr
  id: 3CC3B868-F248-11E8-B48F-1D18A9856A87
  last_name: Novotný
- first_name: Jiří
  full_name: Zárevúcky, Jiří
  last_name: Zárevúcky
- 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 EK, Novotný P, Zárevúcky J, Zikelic D. On lexicographic
    proof rules for probabilistic termination. In: <i>24th International Symposium
    on Formal Methods</i>. Vol 13047. Springer Nature; 2021:619-639. doi:<a href="https://doi.org/10.1007/978-3-030-90870-6_33">10.1007/978-3-030-90870-6_33</a>'
  apa: 'Chatterjee, K., Goharshady, E. K., Novotný, P., Zárevúcky, J., &#38; Zikelic,
    D. (2021). On lexicographic proof rules for probabilistic termination. In <i>24th
    International Symposium on Formal Methods</i> (Vol. 13047, pp. 619–639). Virtual:
    Springer Nature. <a href="https://doi.org/10.1007/978-3-030-90870-6_33">https://doi.org/10.1007/978-3-030-90870-6_33</a>'
  chicago: Chatterjee, Krishnendu, Ehsan Kafshdar Goharshady, Petr Novotný, Jiří Zárevúcky,
    and Dorde Zikelic. “On Lexicographic Proof Rules for Probabilistic Termination.”
    In <i>24th International Symposium on Formal Methods</i>, 13047:619–39. Springer
    Nature, 2021. <a href="https://doi.org/10.1007/978-3-030-90870-6_33">https://doi.org/10.1007/978-3-030-90870-6_33</a>.
  ieee: K. Chatterjee, E. K. Goharshady, P. Novotný, J. Zárevúcky, and D. Zikelic,
    “On lexicographic proof rules for probabilistic termination,” in <i>24th International
    Symposium on Formal Methods</i>, Virtual, 2021, vol. 13047, pp. 619–639.
  ista: 'Chatterjee K, Goharshady EK, Novotný P, Zárevúcky J, Zikelic D. 2021. On
    lexicographic proof rules for probabilistic termination. 24th International Symposium
    on Formal Methods. FM: Formal Methods, LNCS, vol. 13047, 619–639.'
  mla: Chatterjee, Krishnendu, et al. “On Lexicographic Proof Rules for Probabilistic
    Termination.” <i>24th International Symposium on Formal Methods</i>, vol. 13047,
    Springer Nature, 2021, pp. 619–39, doi:<a href="https://doi.org/10.1007/978-3-030-90870-6_33">10.1007/978-3-030-90870-6_33</a>.
  short: K. Chatterjee, E.K. Goharshady, P. Novotný, J. Zárevúcky, D. Zikelic, in:,
    24th International Symposium on Formal Methods, Springer Nature, 2021, pp. 619–639.
conference:
  end_date: 2021-11-26
  location: Virtual
  name: 'FM: Formal Methods'
  start_date: 2021-11-20
date_created: 2021-12-05T23:01:45Z
date_published: 2021-11-10T00:00:00Z
date_updated: 2025-07-14T09:10:11Z
day: '10'
department:
- _id: KrCh
doi: 10.1007/978-3-030-90870-6_33
ec_funded: 1
external_id:
  arxiv:
  - '2108.02188'
  isi:
  - '000758218600033'
intvolume: '     13047'
isi: 1
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: https://arxiv.org/abs/2108.02188
month: '11'
oa: 1
oa_version: Preprint
page: 619-639
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: 24th International Symposium on Formal Methods
publication_identifier:
  eisbn:
  - 978-3-030-90870-6
  eissn:
  - 1611-3349
  isbn:
  - 9-783-0309-0869-0
  issn:
  - 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
related_material:
  record:
  - id: '14539'
    relation: dissertation_contains
    status: public
  - id: '14778'
    relation: later_version
    status: public
scopus_import: '1'
status: public
title: On lexicographic proof rules for probabilistic termination
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 13047
year: '2021'
...