Topologies, Continuity and Bisimulations
Center for Foundations of Intelligent Systems,
626 Rhodes Hall, Cornell University,
Ithaca, NY 14853, U.S.A.; e-mail: firstname.lastname@example.org
2 June – Dec. 1999: Computer Sciences Laboratory, Research School of Information Sciences and Engineering, Australian National University, Canberra ACT 0200, Australia; e-mail: email@example.com
Revised: 2 June 1999
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.
Mathematics Subject Classification: 03B45 / 54C60 / 93C60
Key words: Modal logic / μ-calculus / bisimulation / set-valued maps / semi-continuity / Alexandroff topology / hybrid systems / decidability.
© EDP Sciences, 1999