Jiri Zárevúcky

dblp:272/9265 · DBLP profile ↗
← Back
2ranked-venue papers
0as first author
2since 2021 · last 2023
—ORCID · none

Domains — the database's venue-derived domains; a paper can count in several

Theory of computation · 2 · 2 since 2021Software engineering, systems software and programming languages · 1 · 1 since 2021
YearPublicationVenuePosition
2023 On Lexicographic Proof Rules for Probabilistic Termination
abstract
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.
Krishnendu Chatterjee, Ehsan Kafshdar Goharshady, Petr Novotný 0001, Jiri Zárevúcky, Dorde Zikelic
Formal Aspects Comput.4
2021 On Lexicographic Proof Rules for Probabilistic Termination
Krishnendu Chatterjee, Ehsan Kafshdar Goharshady, Petr Novotný 0001, Jiri Zárevúcky, Dorde Zikelic
FM4