Patrick Cousot, Profesor, Courant Institute of Mathematical Sciences, New York University, US
We study abstraction correspondences between hybrid trajectory semantics for verification and refinement, including discretization and state-based homomorphisms, simulations, bisimulations, preservations with progress, and show that they are all Galois connections. We investigate the problematic composition of hybrid state-based abstractions.