Topologies, Continuity and Bisimulations

J. M. Davoren

RAIRO - Theoretical Informatics and Applications (2010)

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

Abstract

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

How to cite

top

Davoren, 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
  1. 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.  
  2. S. Ambler, M.Z. Kwiatkowska and N. Measor, Duality and the completeness of the modal µ-calculus. Theoret. Comput. Sci.151 (1995) 3-27.  
  3. J.-P. Aubin and H. Frankowska, Set-Valued Analysis. Birkhäuser, Boston (1990).  
  4. 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.  
  5. J. Davoren, Modal Logics for Continuous Dynamics. Ph.D. Thesis, Department of Mathematics Cornell University (1998).  
  6. 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.  
  7. 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.  
  8. 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.  
  9. T. Henzinger, P. Kopke, A. Puri and P. Varaiya, What's decidable about hybrid automata? J. Comput. System Sci.57 (1998) 94-124.  
  10. M. Hollenberg, Logic and Bisimulation. Ph.D. Thesis, Department of Philosophy, Utrecht University (1998).  
  11. B. Jónsson and A. Tarski, Boolean algebras with operators, part i. Amer. J. Math. 73 (1951) 891-939.  
  12. D. Kozen, Results on the propositional µ-calculus. Theoret. Comput. Sci.27 (1983) 333-354.  
  13. G. Lafferriere, G. Pappas and S. Sastry, O-minimal hybrid systems. Technical Report UCB/ERL M98/29, Dept. EECS, UC Berkeley (1998).  
  14. G. Lafferriere, G. Pappas and S. Yovine, Decidable hybrid systems. Technical Report UCB/ERL M98/39, Dept. EECS, UC Berkeley (1998).  
  15. 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.  
  16. 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.  
  17. 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.  
  18. L. van den Dries, Tame Topology and O-minimal Structures. Cambridge Univ. Press, Cambridge, London Math. Soc. Lecture Note Ser.248 (1998).  
  19. I. Walukiewicz, A note on the completeness of Kozen's axiomatization of the propositonal µ-calculus. Bull. Symbolic Logic2 (1996) 349-366.  

NotesEmbed ?

top

You must be logged in to post comments.

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

Only the controls for the widget will be shown in your chosen language. Notes will be shown in their authored language.

Tells the widget how many notes to show per page. You can cycle through additional notes using the next and previous controls.

    
                

                
Note: Best practice suggests putting the JavaScript code just before the closing </body> tag.