The notion of a bisimulation relation is of basic impor- tance in many areas of computation theory and logic. Of late, it has come to take a particular signicance in work on the formal analy- sis and verication of hybrid control systems, where system properties are expressible by formulas of the modal -calculus or weaker tem- poral logics. Our purpose here is to give an analysis of the concept of bisimulation, starting with the observation that the zig-zag condi- tions are suggestive of some form of continuity. We give a topological characterization of bisimularity for preorders, and then use the topol- ogy as a route to examining the algebraic semantics for the -calculus, developed in recent work of Kwiatkowskaet al., and its relation to the standard set-theoretic semantics. In our setting, -calculus sen- tences evaluate as clopen sets of an Alexandro topology, rather than as clopens of a (compact, Hausdor) Stone topology, as arises in the Stone space representation of Boolean algebras (with operators). The paper concludes by applying the topological characterization to obtain the decidability of -calculus properties for a class of rst-order de- nable hybrid dynamical systems, slightly extending and considerably simplifying the proof of a recent result of Laerriere et al. AMS Subject Classication. 03B45, 54C60, 93C60.
['Jennifer M. Davoren']
Topologies, Continuity and Bisimulations