Bi-Weekly Talk: Jan-Christoph Kassing: Analyzing Almost-Sure Termination of Probabilistic Term Rewriting via Innermost Almost-Sure Termination

Mittwoch, 08.02.2023, 10.30 Uhr

Ort: RWTH Aachen University, Informatikzentrum - Ahornstr. 55, Erweiterungsgebäude E3, Raum 9u10

Vortragender: Jan-Christoph Kassing

 

Abstract:

Probabilistic term rewrite systems (PTRSs) can be used to analyze probabilistic algorithms that deal with arbitrary data structures like lists, graphs, etc. We recently developed techniques to analyze innermost almost-sure termination (AST) of PTRSs, i.e., we analyze whether all rewrite sequences that follow an innermost evaluation strategy converge with probability 1. In this talk, we take a look at the difference between (full) AST and innermost AST, we show that the properties which guarantee that (full) termination and innermost termination coincide do not suffice for AST, and adjust these properties suitably. The new properties can still be automatically checked and this allows us to use all techniques and tools for innermost AST to analyze (full) AST.