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

Wednesday, June 14, 2023, 10:30am

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

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