Topologies, continuity and bisimulations

J. M. Davoren*

*Corresponding author for this work

    Research output: Contribution to journalArticlepeer-review

    20 Citations (Scopus)

    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 de-finable hybrid dynamical systems, slightly extending and considerably simplifying the proof of a recent result of Lafierriere et al.

    Original languageEnglish
    Pages (from-to)357-381
    Number of pages25
    JournalRAIRO - Theoretical Informatics and Applications
    Volume33
    Issue number4-5
    DOIs
    Publication statusPublished - 1999

    Fingerprint

    Dive into the research topics of 'Topologies, continuity and bisimulations'. Together they form a unique fingerprint.

    Cite this