In many contexts it is important that a given system will eventually
reach a certain goal (e.g., the goal that a train eventually stops when the
brakes are switched on). Verification of such properties is often done on the
basis of so-called ranking functions (in some contexts also called Lyapunov
functions)
We have a special algorithm for computing such functions (in fact, one of
world-wide only two completely automatic algorithms in the area). The topic of the thesis would be to apply
this algorithm to new problem classes with a similar structure (e.g., termination of
term-rewrite systems, Lyapunov functions of hybrid systems, functions that prove that certain
states in dynamical systems are not reachable, program verification), and to adapt the
algorithm to specific area.
