Lexicographic ranking supermartingales: an efficient approach to termination of probabilistic programs

AGRAWAL, Sheshansh, Krishnendu CHATTERJEE a Petr NOVOTNÝ. Lexicographic ranking supermartingales: an efficient approach to termination of probabilistic programs. In PACMPL (Proceedings of POPL'18). New York, NY, USA: ACM, 2018, s. "34:1--34:32", 32 s. ISSN 2475-1421.

Základní údaje

• Originální název: Lexicographic ranking supermartingales: an efficient approach to termination of probabilistic programs
• Autoři: AGRAWAL, Sheshansh, Krishnendu CHATTERJEE a Petr NOVOTNÝ.
• Vydání: New York, NY, USA, PACMPL (Proceedings of POPL'18), od s. "34:1--34:32", 32 s. 2018.
• Nakladatel: ACM

Další údaje

• Typ výsledku: Stať ve sborníku
• Utajení: není předmětem státního či obchodního tajemství
• ISSN: 2475-1421
• Klíčová slova anglicky: probabilistic termination; ranking functions; supermartingales
• Příznaky: Mezinárodní význam, Recenzováno

Anotace

Probabilistic programs extend classical imperative programs with real-valued random variables and random branching. The most basic liveness property for such programs is the termination property. The qualitative (aka almost-sure) termination problem asks whether a given program program terminates with probability 1. While ranking functions provide a sound and complete method for non-probabilistic programs, the extension of them to probabilistic programs is achieved via ranking supermartingales (RSMs). Although deep theoretical results have been established about RSMs, their application to probabilistic programs with nondeterminism has been limited only to programs of restricted control-flow structure. For non-probabilistic programs, lexicographic ranking functions provide a compositional and practical approach for termination analysis of real-world programs. In this work we introduce lexicographic RSMs and show that they present a sound method for almost-sure termination of probabilistic programs with nondeterminism. We show that lexicographic RSMs provide a tool for compositional reasoning about almost-sure termination, and for probabilistic programs with linear arithmetic they can be synthesized efficiently (in polynomial time). We also show that with additional restrictions even asymptotic bounds on expected termination time can be obtained through lexicographic RSMs. Finally, we present experimental results on benchmarks adapted from previous work to demonstrate the effectiveness of our approach.