---
_id: '14778'
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 a LexRSM
    not existing even for simple terminating programs. Our contributions are twofold.
    First, we introduce a generalization of LexRSMs that 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 (grant no. 863818;
  ForM-SMArt), the Czech Science Foundation (grant no. GA21-24711S), and the European
  Union’s Horizon 2020 research and innovation program under the Marie Skłodowska-Curie
  Grant Agreement No. 665385.
article_number: '11'
article_processing_charge: Yes (via OA deal)
article_type: original
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
  full_name: Kafshdar Goharshady, Ehsan
  last_name: Kafshdar 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, Kafshdar Goharshady E, Novotný P, Zárevúcky J, Zikelic D. On
    lexicographic proof rules for probabilistic termination. <i>Formal Aspects of
    Computing</i>. 2023;35(2). doi:<a href="https://doi.org/10.1145/3585391">10.1145/3585391</a>
  apa: Chatterjee, K., Kafshdar Goharshady, E., Novotný, P., Zárevúcky, J., &#38;
    Zikelic, D. (2023). On lexicographic proof rules for probabilistic termination.
    <i>Formal Aspects of Computing</i>. Association for Computing Machinery. <a href="https://doi.org/10.1145/3585391">https://doi.org/10.1145/3585391</a>
  chicago: Chatterjee, Krishnendu, Ehsan Kafshdar Goharshady, Petr Novotný, Jiří Zárevúcky,
    and Dorde Zikelic. “On Lexicographic Proof Rules for Probabilistic Termination.”
    <i>Formal Aspects of Computing</i>. Association for Computing Machinery, 2023.
    <a href="https://doi.org/10.1145/3585391">https://doi.org/10.1145/3585391</a>.
  ieee: K. Chatterjee, E. Kafshdar Goharshady, P. Novotný, J. Zárevúcky, and D. Zikelic,
    “On lexicographic proof rules for probabilistic termination,” <i>Formal Aspects
    of Computing</i>, vol. 35, no. 2. Association for Computing Machinery, 2023.
  ista: Chatterjee K, Kafshdar Goharshady E, Novotný P, Zárevúcky J, Zikelic D. 2023.
    On lexicographic proof rules for probabilistic termination. Formal Aspects of
    Computing. 35(2), 11.
  mla: Chatterjee, Krishnendu, et al. “On Lexicographic Proof Rules for Probabilistic
    Termination.” <i>Formal Aspects of Computing</i>, vol. 35, no. 2, 11, Association
    for Computing Machinery, 2023, doi:<a href="https://doi.org/10.1145/3585391">10.1145/3585391</a>.
  short: K. Chatterjee, E. Kafshdar Goharshady, P. Novotný, J. Zárevúcky, D. Zikelic,
    Formal Aspects of Computing 35 (2023).
date_created: 2024-01-10T09:27:43Z
date_published: 2023-06-23T00:00:00Z
date_updated: 2025-07-14T09:10:10Z
day: '23'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.1145/3585391
ec_funded: 1
external_id:
  arxiv:
  - '2108.02188'
file:
- access_level: open_access
  checksum: 3bb133eeb27ec01649a9a36445d952d9
  content_type: application/pdf
  creator: dernst
  date_created: 2024-01-16T08:11:24Z
  date_updated: 2024-01-16T08:11:24Z
  file_id: '14804'
  file_name: 2023_FormalAspectsComputing_Chatterjee.pdf
  file_size: 502522
  relation: main_file
  success: 1
file_date_updated: 2024-01-16T08:11:24Z
has_accepted_license: '1'
intvolume: '        35'
issue: '2'
keyword:
- Theoretical Computer Science
- Software
language:
- iso: eng
month: '06'
oa: 1
oa_version: Published Version
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: Formal Aspects of Computing
publication_identifier:
  eissn:
  - 1433-299X
  issn:
  - 0934-5043
publication_status: published
publisher: Association for Computing Machinery
quality_controlled: '1'
related_material:
  record:
  - id: '10414'
    relation: earlier_version
    status: public
status: public
title: On lexicographic proof rules for probabilistic termination
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: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 35
year: '2023'
...