Tuesday, 15 April 2025

We are at the 41st British Colloquium for Theoretical Computer Science at Strathclyde University (Glasgow)

Swansea Theory Group at BCTCS 2025
BCTCS 2025 at Strathclyde University, Glasgow
Marek Jezinski, Alec Critten, Harry Bryant and Olga Petrovska are currently attending the 41st British Colloquium for Theoretical Computer Science at Strathclyde University, Glasgow.

Marek gave a talk on "Creating Synthetic Test Data for Rail Design Tools", Alec gave a talk on "Developing user propagators for graph-based SMT reasoning", and Harry gave a talk on "Proof Checking for SMT-solving and its application in the Railway Domain."

Olga, who is also BCTCS' Treasurer, will contribute to the education session with her talk on "The Art of Teaching Theory Across Diverse Backgrounds."



Thursday, 3 April 2025

On Threshold Problems for Orbits of Semigroup Actions by Eike

Today Eike Neumann will give a talk on Threshold Problems for Orbits of Semigroup Actions as a part of our theory seminar series.

Abstract:
Consider the following computational problem: Given a real function g on a space X, a compactly generated semi-group S acting on X, and a point x in X, is g positive on every point of the orbit of x under S?

This generalises a large number of widely studied problems, such as safety and liveness verification for discrete-time dynamical systems (corresponding to semi-groups with a single generator), threshold problems for stochastic (corresponding stochastic matrices acting on probability distributions) or quantum automata (corresponding to unitary operators acting on Hilbert spaces) and more.

When the objects above are presented via rational or algebraic data, the associated problems quickly become undecidable or very sensitive to the problem formulation. For example, threshold problems for stochastic automata are undecidable in general, and threshold problems for quantum automata are decidable if and only if they are formulated using strict inequality.

I will consider the above problem in its general form from the computable analysis perspective, replacing decidability with maximal partial decidability. I will give a sound algorithm that partially decides the problem over effectively locally compact spaces. I will show that the algorithm is complete when the space is zero-dimensional or locally contractible, and give some examples of spaces where the algorithm is not complete but the problem is maximally partially decidable and spaces where the problem is not maximally partially decidable at all.

We are at the 41st British Colloquium for Theoretical Computer Science at Strathclyde University (Glasgow)

BCTCS 2025 at Strathclyde University, Glasgow Marek Jezinski, Alec Critten, Harry Bryant and Olga Petrovska are currently attending the 41st...