Skip to main content

Topological semantics for hybrid systems

  • Conference paper
  • First Online:
Logical Foundations of Computer Science (LFCS 1997)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 1234))

Included in the following conference series:

  • 123 Accesses

Abstract

This procedure for strengthening correctness to correctness relative to small changes in any interesting parameters can be extended to apply to any hybrid systems language, with slight changes in primitive relations. The key idea is that the physical systems are dynamical systems equipped with topologies on state spaces, that finite automata have to work relative to finite space quotient topologies, and that one needs to respect observational equivalence to get correctness proofs that allow small variations, which means using Intuitionistic deductions.

Supported in part by the Russian Foundation for Basic Research, grant No. 96-01-01135, and by INTAS grant No. 94-2412.

American Association of University Women (AAUW) Educational Foundation 1996–97 International Fellow.

Research supported by ARO under the MURI program “Integrated Approach to Intelligent Systems”, grant number DAA H04-96-1-0341.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Raymond Balbes and Philip Dwinger, Distributive Lattices (University of Missouri Press, Columbia, 1974).

    Google Scholar 

  2. Michael Branicky, “Topology of Hybrid Systems”, Proceedings of the 32nd IEEE Conference on Decision and Control (IEEE Computer Society Press, Los Alamitos, 1993), Vol. 3, 2309–2314.

    Google Scholar 

  3. Dirk van Dalen, “Intuitionistic Logic”, in D. Gabbbay and F. Guenthner (eds.), Handbook of Philosophical Logic, Volume III: Alternatives to Classical Logic (D. Reidel, Dordrecht, 1986), 225–339.

    Google Scholar 

  4. Michael Dummett, Elements of Intuitionism (Clarendon Press, Oxford, 1977).

    Google Scholar 

  5. Michael P. Fourman and Dana S. Scott, “Sheaves and Logic”, in M. P. Fourman, C. J. Mulvey and D. S. Scott (eds.), Applications of Sheaves, Proceedings of the Research Symposium on Applications of Sheaf Theory to Logic, Algebra and Analysis, Durham, England, July 9–21, 1977; Springer Lecture Notes in Mathematics 753 (Springer-Verlag, Berlin 1979), 302–401.

    Google Scholar 

  6. Xiaolin Ge, Wolf Kohn, Anil Nerode, and Jeffrey B. Remmel, “Hybrid Systems: Chattering Approximations to Relaxed Controls”, in R. Alur, T. A. Henzinger, E. D. Sontag (eds.), Hybrid Systems III, Lecture Notes in Computer Science 1066 (Springer-Verlag, Berlin, 1996), 76–100.

    Google Scholar 

  7. Wolf Kohn, John James and Anil Nerode, “The Declarative Approach to the Design of Robust Control Systems”, Proceedings of the IEEE Symposium on Computer-Aided Control System Design 1996 (CACSD '96), 26–31.

    Google Scholar 

  8. Wolf Kohn, John James, Anil Nerode, Jeffrey B. Remmel and Benjamin Cummings, “A New Approach to Generating Finite-State Control Programs for Hybrid Systems”, Proceedings of the 13th Triennial World Congress of the International Federation of Automatic Control (IFAC) 1996 (Pergamon Press, 1996), 461–466.

    Google Scholar 

  9. Wolf Kohn, Anil Nerode and Jeffrey B. Remmel, “Hybrid Systems as Finsler Manifolds: Finite State Control as Approximation to Connections”, in P. Antsaklis, W. Kohn, A. Nerode and S. Sastry (eds.), Hybrid Systems II, Lecture Notes in Computer Science 999 (Springer-Verlag, Berlin, 1995), 294–321.

    Google Scholar 

  10. Wolf Kohn, Anil Nerode and Jeffrey B. Remmel, “Continualization: A Hybrid Systems Control Technique for Computing”, Proceedings of 1996 IMACS Conference on Computation Engineering in Systems Applications (CEAS '96).

    Google Scholar 

  11. Wolf Kohn, Anil Nerode and Jeffrey B. Remmel, “Feedback Derivations: Near Optimal Controls for Hybrid Systems”, Proceedings of the 1996 IMACS conference on Computation Engineering in Systems Applications (CESA '96), 517–521.

    Google Scholar 

  12. Wolf Kohn, Anil Nerode, Jeffrey B. Remmel and Alexander Yakhnis, “Viability in Hybrid Systems”, Theoretical Computer Science 138 (1995) 141–168.

    Google Scholar 

  13. Wolf Kohn, Jeffrey B. Remmel, Anil Nerode, “Scalable Data and Sensor Fusion via Multiple Agent Hybrid Systems”, IEEE Transactions on Automatic Control, special issue on Hybrid Systems, to appear 1997.

    Google Scholar 

  14. Wolf Kohn, Jeffrey B. Remmel, Anil Nerode, John James, “Multiple Agent Hybrid Control for Manufacturing Systems”, Proceedings of the 11th IEEE International Symposium on Intelligent Control (IEEE, New York 1996), 348–353.

    Google Scholar 

  15. John W. Lloyd, Foundations of Logic Programming, 2nd edition (Springer-Verlag, Berlin 1987).

    Google Scholar 

  16. Anil Nerode, “Some Stone Spaces and Recursion Theory”, Duke Mathematical Journal 26 (1959) 397–406.

    Google Scholar 

  17. Anil Nerode, “Some Lectures on Intuitionistic Logic”, in P. Odifreddi (ed.), Logic and Computer Science, Lecture Notes in Mathematics 1429 (Springer-Verlag, Berlin, 1990), 12–59.

    Google Scholar 

  18. Anil Nerode and Wolf Kohn, “Models for Hybrid Systems: Automata, Topologies, Controllability, Observability”, in R. Grossman, A. Nerode, A. Ravn and H. Rischel (eds.), Hybrid Systems, Springer Lecture Notes in Computer Science 736 (Springer-Verlag, Berlin, 1993), 297–316.

    Google Scholar 

  19. Anil Nerode and Wolf Kohn, “Multiple Agent Hybrid Control Architecture”, in R. Grossman, A. Nerode, A. Ravn and H. Rischel (eds.), Hybrid Systems, Springer Lecture Notes in Computer Science 736 (Springer-Verlag, Berlin, 1993), 317–356.

    Google Scholar 

  20. Helena Rasiowa and Roman Sikorski, The Mathematics of Metamathematics, Polska Akademia Nauk Monografie Matematyczne, Tom 41 (Państwowe Wydawnictwo Naukowe, Warsaw, 1963).

    Google Scholar 

  21. Richard Statman, “Intuitionistic Propositional Logic is Polynomial Space Complete”, Theoretical Computer Science 9 (1979) 67–72.

    Google Scholar 

  22. Alfred Tarski, “Der Aussagenkalkül und die Topologie”, Fundamental Mathematicae 31 (1938) 103–134. Reprinted (and translated by J. H. Woodger) as “Sentential Calculus and Topology”, in A. Tarski, Logic, Semantics, Metamathematics (Oxford University Press, 1956), 421–454.

    Google Scholar 

Download references

Author information

Authors and Affiliations

Authors

Editor information

Sergei Adian Anil Nerode

Rights and permissions

Reprints and permissions

Copyright information

© 1997 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Artemov, S., Davoren, J., Nerode, A. (1997). Topological semantics for hybrid systems. In: Adian, S., Nerode, A. (eds) Logical Foundations of Computer Science. LFCS 1997. Lecture Notes in Computer Science, vol 1234. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-63045-7_1

Download citation

  • DOI: https://doi.org/10.1007/3-540-63045-7_1

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-63045-6

  • Online ISBN: 978-3-540-69065-8

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics