Topologies, Continuity and Bisimulations

¹ Center for Foundations of Intelligent Systems, 626 Rhodes Hall, Cornell University, Ithaca, NY 14853, U.S.A.; e-mail: davoren@hybrid.cornell.edu
² June – Dec. 1999: Computer Sciences Laboratory, Research School of Information Sciences and Engineering, Australian National University, Canberra ACT 0200, Australia; e-mail: davoren@arp.anu.edu.au

Received: 2 November 1998
Revised: 2 June 1999

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.