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

Wednesday, February 08, 2023, 10:30am

Location: RWTH Aachen University, Department of Computer Science - Ahornstr. 55, building E3, room 9u10

Speaker: 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.