## Topologies, Continuity and Bisimulations

### Description

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...[Show more]

dc.contributor.author | Davoren, Jennifer M. | |
---|---|---|

dc.date.accessioned | 2015-12-13T23:35:29Z | |

dc.date.available | 2015-12-13T23:35:29Z | |

dc.identifier.issn | 0988-3754 | |

dc.identifier.uri | http://hdl.handle.net/1885/93931 | |

dc.description.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. | |

dc.publisher | EDP Sciences | |

dc.source | Theoretical Informatics and Applications | |

dc.subject | Keywords: Boolean algebra; Computational linguistics; Formal logic; Mathematical operators; Topology; Alexandroff topology; Bisimulation relations; Lambda calculus; Computer simulation | |

dc.title | Topologies, Continuity and Bisimulations | |

dc.type | Journal article | |

local.description.notes | Imported from ARIES | |

local.description.refereed | Yes | |

local.identifier.citationvolume | 33 | |

dc.date.issued | 1999 | |

local.identifier.absfor | 080299 - Computation Theory and Mathematics not elsewhere classified | |

local.identifier.ariespublication | MigratedxPub25369 | |

local.type.status | Published Version | |

local.contributor.affiliation | Davoren, Jennifer M., College of Engineering and Computer Science, ANU | |

local.bibliographicCitation.startpage | 357 | |

local.bibliographicCitation.lastpage | 381 | |

dc.date.updated | 2015-12-12T09:40:09Z | |

local.identifier.scopusID | 2-s2.0-0033294940 | |

Collections | ANU Research Publications |

### Download

Items in Open Research are protected by copyright, with all rights reserved, unless otherwise indicated.

Updated: **19 May 2020**/
Responsible Officer: **University Librarian**/
Page Contact: **Library Systems & Web Coordinator**