Topologies, Continuity and Bisimulations

Abstract

The notion of a bisimulation relation is of basic importance in many areas of computation theory and logic. Of late, it has come to take a particular significance in work on the formal analysis and verification of hybrid control systems, where system properties are expressible by formulas of the modal μ-calculus or weaker temporal logics. Our purpose here is to give an analysis of the concept of bisimulation, starting with the observation that the zig-zag conditions are suggestive of some form of continuity. We give a topological characterization of bisimularity for preorders, and then use the topology as a route to examining the algebraic semantics for the µ-calculus, developed in recent work of Kwiatkowska et al., and its relation to the standard set-theoretic semantics. In our setting, μ-calculus sentences evaluate as clopen sets of an Alexandroff topology, rather than as clopens of a (compact, Hausdorff) 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 first-order definable hybrid dynamical systems, slightly extending and considerably simplifying the proof of a recent result of Lafferriere et al.