Synthesis and verification of definable dynamics

Margarita Korovina

(A.P. Ershov Institute of Informatics Systems)

In this talk I will present ongoing research which is aimed at creating
a logical framework for synthesis and formal verification of definable dynamical systems.
First, we discuss the problem of finite control synthesis for definable dynamics. I will show how quantifier elimination and real algebraic geometry methods could help to solve this problem for polynomial dynamics. Then, we address reachability problem, i.e., whether trajectories of the dynamical systems reach safe/unsafe regions from initial regions. The key idea of our approach is based on computing combinatorial types of trajectories. I will show how it could be done using cylindrical cell decomposition for polynomial and Pfaffian dynamics.

Thursday 20th June 2013, 14:00
Robert Recorde Room
Department of Computer Science