Skip navigation
Skip navigation

Topologies, Continuity and Bisimulations

Davoren, Jennifer M.

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.authorDavoren, Jennifer M.
dc.date.accessioned2015-12-13T23:35:29Z
dc.date.available2015-12-13T23:35:29Z
dc.identifier.issn0988-3754
dc.identifier.urihttp://hdl.handle.net/1885/93931
dc.description.abstractThe 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.publisherEDP Sciences
dc.sourceTheoretical Informatics and Applications
dc.subjectKeywords: Boolean algebra; Computational linguistics; Formal logic; Mathematical operators; Topology; Alexandroff topology; Bisimulation relations; Lambda calculus; Computer simulation
dc.titleTopologies, Continuity and Bisimulations
dc.typeJournal article
local.description.notesImported from ARIES
local.description.refereedYes
local.identifier.citationvolume33
dc.date.issued1999
local.identifier.absfor080299 - Computation Theory and Mathematics not elsewhere classified
local.identifier.ariespublicationMigratedxPub25369
local.type.statusPublished Version
local.contributor.affiliationDavoren, Jennifer M., College of Engineering and Computer Science, ANU
local.bibliographicCitation.startpage357
local.bibliographicCitation.lastpage381
dc.date.updated2015-12-12T09:40:09Z
local.identifier.scopusID2-s2.0-0033294940
CollectionsANU Research Publications

Download

There are no files associated with this item.


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