Bi-Weekly Talk: Eleanore Meyer: Termination Analysis of Simple Randomised Linear Programs

Mittwoch, 14.06.2023, 10.30 Uhr

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

Vortragende: Eleanore Meyer

 

Abstract:

It is well known that the question whether a given program terminates universally is undecidable in general.
However, in recent years, many results have shown the decidability of this question if one restricts the class of programs considered to so-called linear/affine loops.
Such programs consist of a single while-loop with a linear/affine guard and a deterministic linear/affine update as the body.

In this talk, we aim to transfer these results to the setting of randomised linear loops.
Such a loop consists of two different linear updates.
In each iteration of the loop one of the two updates is then selected according to the outcome of a coin flip.
To keep the analysis tractable we limit ourselves to commuting updates.
Additionally, we will require that both updates are diagonalisable.

This is work-in-progress.