VeTSS Summer School 2026 Programme

Details of talks

Counter machines and the border of effective computation

Patrick Totzke (University of Liverpool)

Abstract:

Counter Machines a la Minsky are one of the simplest computational models and a great starting point to explore the limits of effective computability and verification.

We will recall some foundational results in the theory of computation, including the undecidability of the termination problem for two-counter machines and related decision questions. These provide natural starting points to show impossibility results and complexity lower bounds.

We will survey ways to modify the model to make it less expressive and allow to recover decidability for verification questions.

This can be achieved by restricting the use of zero-tests, accepting imprecise updates to counters, allowing a single counter, or combinations thereof.

Several such models form the theoretical underpinning of automated formal verification methods in use today and we will demonstrate applications and directions for future research.

Formal Methods for Safe Reinforcement Learning

Edwin Hamel-De le Court (University of Manchester)

Abstract:

The goal of the lecture is to present the emerging relationship between Reinforcement Learning (RL) and Temporal Logic (TL). The topic is an active area of research that builds a bridge between the RL and verification communities. In a world where the safety of AI systems is becoming increasingly critical, bridging the gap between these communities is an important step towards developing safe, reliable, and trustworthy AI.

At the end of the lecture, the audience will have the basics of RL and safe RL, a good intuition of the properties expressible in Temporal Logic, and a clear overview of how to design RL algorithms with TL objectives or constraints, including methods that provide formal guarantees.