Topologies, Continuity and Bisimulations

Issue		RAIRO-Theor. Inf. Appl. Volume 33, Number 4/5, July-October 1999


Page(s)		357 - 381
DOI		10.1051/ita:1999123

DOI: 10.1051/ita:1999123
Theoret. Informatics Appl. 33 (1999) 357-381

Topologies, Continuity and Bisimulations

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

Received November 2, 1998. Revised June 2, 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 $\mu$ -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 $\mu$ -calculus, developed in recent work of Kwiatkowska et al., and its relation to the standard set-theoretic semantics. In our setting, $\mu$ -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 $\mu$ -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.

Keywords and phrases: Modal logic, $\mu$ -calculus, bisimulation, set-valued maps, semi-continuity, Alexandroff topology, hybrid systems, decidability.

AMS Subject Classification: 03B45, 54C60, 93C60

What is OpenURL?

The OpenURL standard is a protocol for transmission of metadata describing the resource that you wish to access. An OpenURL link contains article metadata and directs it to the OpenURL server of your choice. The OpenURL server can provide access to the resource and also offer complementary services (specific search engine, export of references...). The OpenURL link can be generated by different means.

If your librarian has set up your subscription with an OpenURL resolver, OpenURL links appear automatically on the abstract pages.
You can define your own OpenURL resolver with your EDPS Account. In this case your choice will be given priority over that of your library.
You can use an add-on for your browser (Firefox or I.E.) to display OpenURL links on a page (see http://www.openly.com/openurlref/). You should disable this module if you wish to use the OpenURL server that you or your library have defined.