On properties of ω-automata using simulation distances

It is interesting to study properties of abstract metric spaces. Here we define metrics on the set of finite state automata A (over a fixed set of transition symbols Σ), and study their properties. We define simulation games on automata with a finite Σ, but we later move on to more general automata, where Σ is treated as a metric space itself. We then consider the original case and construct midpoints.