Decidability, Topological Semantics and Completeness for S4