# Topologies, Continuity and Bisimulations

RAIRO - Theoretical Informatics and Applications (2010)

- Volume: 33, Issue: 4-5, page 357-381
- ISSN: 0988-3754

## Access Full Article

top## Abstract

top## How to cite

topDavoren, J. M.. "Topologies, Continuity and Bisimulations." RAIRO - Theoretical Informatics and Applications 33.4-5 (2010): 357-381. <http://eudml.org/doc/222075>.

@article{Davoren2010,

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.
},

author = {Davoren, J. M.},

journal = {RAIRO - Theoretical Informatics and Applications},

keywords = {Modal logic; μ-calculus; bisimulation; set-valued maps; semi-continuity;
Alexandroff topology; hybrid systems; decidability.; modal -calculus; bisimulation relation; formal analysis and verification of hybrid control systems; algebraic semantics; Alexandroff topology; decidability; first-order definable hybrid dynamical systems},

language = {eng},

month = {3},

number = {4-5},

pages = {357-381},

publisher = {EDP Sciences},

title = {Topologies, Continuity and Bisimulations},

url = {http://eudml.org/doc/222075},

volume = {33},

year = {2010},

}

TY - JOUR

AU - Davoren, J. M.

TI - Topologies, Continuity and Bisimulations

JO - RAIRO - Theoretical Informatics and Applications

DA - 2010/3//

PB - EDP Sciences

VL - 33

IS - 4-5

SP - 357

EP - 381

AB -
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.

LA - eng

KW - Modal logic; μ-calculus; bisimulation; set-valued maps; semi-continuity;
Alexandroff topology; hybrid systems; decidability.; modal -calculus; bisimulation relation; formal analysis and verification of hybrid control systems; algebraic semantics; Alexandroff topology; decidability; first-order definable hybrid dynamical systems

UR - http://eudml.org/doc/222075

ER -

## References

top- R. Alur, C. Courcoubetis, N. Halbwachs, T. Henzinger, P.-H. Ho, X. Nicollin, A. Olivero, J. Sifakis and S. Yovine, The algorithmic analysis of hybrid systems. Theoret. Comput. Sci.138 (1995) 3-34. Zbl0823.68067
- S. Ambler, M.Z. Kwiatkowska and N. Measor, Duality and the completeness of the modal µ-calculus. Theoret. Comput. Sci.151 (1995) 3-27. Zbl0872.03010
- J.-P. Aubin and H. Frankowska, Set-Valued Analysis. Birkhäuser, Boston (1990). Zbl0713.49021
- M. Bonsangue and M. Kwiatkowska, Reinterpreting the modal µ-calculus, A. Ponse, M. de Rijke and Y. Venema, Eds., Modal Logic and Process Algebra. CLSI Publications, Stanford (1995) 65-83.
- J. Davoren, Modal Logics for Continuous Dynamics. Ph.D. Thesis, Department of Mathematics Cornell University (1998).
- J.M. Davoren, On hybrid systems and the modal µ-calculus, P. Antsaklis, W. Kohn, M. Lemmon, A. Nerode and S. Sastry, Eds., Hybrid Systems V. Springer-Verlag, Berlin, Lecture Notes in Comput. Sci.1567 (1999) 38-69. Zbl0928.93027
- C. Daws, A. Olivero, S. Tripakis and S. Yovine, The tool KRONOS, R. Alur, T. Henzinger and E.D. Sontag, Eds., Hybrid Systems III. Springer-Verlag, Berlin, Lecture Notes in Comput. Sci.1066 (1996) 208-219.
- T. Henzinger, The theory of hybrid automata, in Proc. of 11th Annual IEEE Symposium on Logic in Computer Science (LICS'96). IEEE Computer Society Press (1996) 278-292. Zbl0959.68073
- T. Henzinger, P. Kopke, A. Puri and P. Varaiya, What's decidable about hybrid automata? J. Comput. System Sci.57 (1998) 94-124. Zbl0920.68091
- M. Hollenberg, Logic and Bisimulation. Ph.D. Thesis, Department of Philosophy, Utrecht University (1998). Zbl0954.03022
- B. Jónsson and A. Tarski, Boolean algebras with operators, part i. Amer. J. Math. 73 (1951) 891-939. Zbl0045.31505
- D. Kozen, Results on the propositional µ-calculus. Theoret. Comput. Sci.27 (1983) 333-354. Zbl0553.03007
- G. Lafferriere, G. Pappas and S. Sastry, O-minimal hybrid systems. Technical Report UCB/ERL M98/29, Dept. EECS, UC Berkeley (1998). Zbl1059.68073
- G. Lafferriere, G. Pappas and S. Yovine, Decidable hybrid systems. Technical Report UCB/ERL M98/39, Dept. EECS, UC Berkeley (1998). Zbl0926.93036
- A. Nerode and W. Kohn, Models for hybrid systems: Automata, topologies, controllability, observability, R. Grossman, A. Nerode, A. Ravn and H. Rischel, Eds., Hybrid Systems. Springer-Verlag, Berlin, Lecture Notes in Comput. Sci.736 (1993) 297-316.
- M.B. Smyth, Topology, S. Abramsky, D. Gabbay and T. Maibaum, Eds. Oxford University Press, Clarendon Press, Oxford, Handb. Log. Comput. Sci. 1 (1992) 641-761.
- C. Stirling, Modal and temporal logics, S. Abramsky, D. Gabbay and T. Maibaum, Eds. Oxford University Press, Clarendon Press, Oxford, Handb. Log. Comput. Sci. 2 (1992) 477-563.
- L. van den Dries, Tame Topology and O-minimal Structures. Cambridge Univ. Press, Cambridge, London Math. Soc. Lecture Note Ser.248 (1998). Zbl0953.03045
- I. Walukiewicz, A note on the completeness of Kozen's axiomatization of the propositonal µ-calculus. Bull. Symbolic Logic2 (1996) 349-366. Zbl0868.03010

## NotesEmbed ?

topTo embed these notes on your page include the following JavaScript code on your page where you want the notes to appear.