Issue |
RAIRO-Theor. Inf. Appl.
Volume 33, Number 4-5, July October 1999
|
|
---|---|---|
Page(s) | 357 - 381 | |
DOI | https://doi.org/10.1051/ita:1999123 | |
Published online | 15 August 2002 |
Topologies, Continuity and Bisimulations
1
Center for Foundations of Intelligent Systems,
626 Rhodes Hall, Cornell University,
Ithaca, NY 14853, U.S.A.; e-mail: davoren@hybrid.cornell.edu
2
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
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
Current usage metrics show cumulative count of Article Views (full-text article views including HTML views, PDF and ePub downloads, according to the available data) and Abstracts Views on Vision4Press platform.
Data correspond to usage on the plateform after 2015. The current usage metrics is available 48-96 hours after online publication and is updated daily on week days.
Initial download of the metrics may take a while.