A wide range of fundamental systems verification tasks, such as liveness and safety verification for stochastic or quantum automata, can be modelled as instances of the general problem of deciding whether a point escapes a set under the action of a given semigroup.

Theoretical computer scientists traditionally study such problems from a symbolic algebraic perspective: all data is assumed to be provided by exact symbolic means, for example in terms of exact algebraic numbers. In this framework, questions of the above kind become undecidable very quickly. For example, threshold problems for stochastic automata are undecidable in general, and threshold problems for quantum automata are decidable if and only if the inequality with the threshold is taken to be strict. Further, real-world systems are in general not known exactly, but only to some fixed finite accuracy.

In this talk, I will advocate for the study of verification problems such as the above from the perspective of effective topology and second-order computability, where we model the input data as points in effective topological spaces. This allows us to naturally model systems that are known only to finite accuracy. Regarding decidability, we will have to make concessions: if an input lies on the boundary of a decision problem, it is trivially impossible for any second-order algorithm to make a correct decision in finite time. The natural question to ask is hence whether there exists a sound decision procedure that halts on the entire complement of the boundary. On the positive side, excluding the boundary instances will often naturally yield a large set of instances where problems of interest do become decidable.

I will give a sound decision method for the problem of detecting whether a given point in an effectively locally compact space escapes given a set under a given action of a compactly generated topological semigroup. I will show that this method is complete (in the sense of halting on the complement of the boundary instances) when the space is either (weakly) locally contractible or totally disconnected. I will further give examples of effectively locally compact spaces where there exists a complete method, but my “generic” method fails to be complete, and examples where there is no complete decision method at all.