Document Open Access Logo

A Semantics for Hybrid Iteration

Authors Sergey Goncharov, Julian Jakob, Renato Neves

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2018.22.pdf
  • Filesize: 0.59 MB
  • 17 pages

Document Identifiers

Author Details

Sergey Goncharov
  • Lehrstuhl für Theoretische Informatik, Friedrich-Alexander Universität Erlangen-Nürnberg, Germany
Julian Jakob
  • Lehrstuhl für Theoretische Informatik, Friedrich-Alexander Universität Erlangen-Nürnberg, Germany
Renato Neves
  • INESC TEC (HASLab) & University of Minho, Portugal

Funding

  • Goncharov, Sergey: Research supported by Deutsche Forschungsgemeinschaft (DFG) under project GO 2161/1-2.
  • Neves, Renato: Research supported by ERDF - European Regional Development Fund through the Operational Programme for Competitiveness and Internationalisation - COMPETE 2020 Programme and by National Funds through the Portuguese funding agency, FCT - Fundação para a Ciência e a Tecnologia within projects POCI-01-0145-FEDER-016692 and 02/SAICT/2017.

Cite As Get BibTex

Sergey Goncharov, Julian Jakob, and Renato Neves. A Semantics for Hybrid Iteration. In 29th International Conference on Concurrency Theory (CONCUR 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 118, pp. 22:1-22:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018) https://doi.org/10.4230/LIPIcs.CONCUR.2018.22

Abstract

The recently introduced notions of guarded traced (monoidal) category and guarded (pre-)iterative monad aim at unifying different instances of partial iteration whilst keeping in touch with the established theory of total iteration and preserving its merits. In this paper we use these notions and the corresponding stock of results to examine different types of iteration for hybrid computations. As a starting point we use an available notion of hybrid monad restricted to the category of sets, and modify it in order to obtain a suitable notion of guarded iteration with guardedness interpreted as progressiveness in time - we motivate this modification by our intention to capture Zeno behaviour in an arguably general and feasible way. We illustrate our results with a simple programming language for hybrid computations and interpret it over the developed semantic foundations.

Subject Classification

ACM Subject Classification
  • Theory of computation → Timed and hybrid models
Keywords
  • Elgot iteration
  • guarded iteration
  • hybrid monad
  • Zeno behaviour

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Related Versions

References

  1. Rajeev Alur. Principles of Cyber-Physical Systems. MIT Press, 2015. Google Scholar
  2. Aaron Ames, Alessandro Abate, and Shankar Sastry. Sufficient conditions for the existence of zeno behavior. In CDC-ECC'05: Decision and Control and European Control Conference, 44th IEEE Conference, Seville, Spain, December, 2005, pages 696-701. IEEE, 2005. Google Scholar
  3. Aristotle. Physics. Oxford University Press, 2008. Google Scholar
  4. Steve Awodey. Category Theory. Oxford University Press, Inc., New York, NY, USA, 2nd edition, 2010. Google Scholar
  5. Stephen Bloom and Zoltán Ésik. Iteration theories: the equational logic of iterative processes. Springer, 1993. Google Scholar
  6. Filippo Bonchi, Paweł Sobociński, and Fabio Zanasi. A categorical semantics of signal flow graphs. In Paolo Baldan and Daniele Gorla, editors, CONCUR 2014 - Concurrency Theory, pages 435-450, Berlin, Heidelberg, 2014. Springer Berlin Heidelberg. Google Scholar
  7. Filippo Bonchi, Pawel Sobocinski, and Fabio Zanasi. The calculus of signal flow diagrams I: linear relations on streams. Inf. Comput., 252:2-29, 2017. Google Scholar
  8. Zhou Chaochen, Wang Ji, and Anders P. Ravn. A formal description of hybrid systems. In Rajeev Alur, Thomas A. Henzinger, and Eduardo D. Sontag, editors, Hybrid Systems III, volume 1066 of Lecture Notes in Computer Science, pages 511-530. Springer Berlin Heidelberg, 1996. Google Scholar
  9. Fredrik Dahlqvist and Renato Neves. Compositional semantics for new paradigms: probabilistic, hybrid and beyond. arXiv preprint arXiv:1804.04145, 2018. Google Scholar
  10. Calvin Elgot. Monadic computation and iterative algebraic theories. In H.E. Rose and J.C. Shepherdson, editors, Logic Colloquium 1973, volume 80 of Studies in Logic and the Foundations of Mathematics, pages 175-230. Elsevier, 1975. Google Scholar
  11. Ryszard Engelking. General topology, volume 6 of Sigma Series in Pure Mathematics. Heldermann Verlag, Berlin, 1989. Translated from the Polish by the author. Google Scholar
  12. R. Goebel, J.P. Hespanha, A.R. Teel, C. Cai, and R. G. Sanfelice. Hybrid systems: generalized solutions and robust stability. In Proc. 6th IFAC Symposium in Nonlinear Control Systems, page 1endash12, 2004. Google Scholar
  13. Sergey Goncharov, Julian Jakob, and Renato Neves. A semantics for hybrid iteration. arXiv, 2018. URL: http://arxiv.org/abs/1807.01053.
  14. Sergey Goncharov, Christoph Rauch, and Lutz Schröder. Unguarded recursion on coinductive resumptions. In Mathematical Foundations of Programming Semantics, MFPS 2015, volume 319 of ENTCS, pages 183-198. Elsevier, 2015. Google Scholar
  15. Sergey Goncharov and Lutz Schröder. Guarded traced categories. In Christel Baier and Ugo Dal Lago, editors, Proc. 21th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2018), LNCS. Springer, 2018. Google Scholar
  16. Sergey Goncharov, Lutz Schröder, Christoph Rauch, and Maciej Piróg. Unifying guarded and unguarded iteration. In Javier Esparza and Andrzej Murawski, editors, Foundations of Software Science and Computation Structures, FoSSaCS 2017, volume 10203 of LNCS, pages 517-533. Springer, 2017. Google Scholar
  17. Thomas A. Henzinger. The theory of hybrid automata. In LICS96': Logic in Computer Science, 11th Annual Symposium, New Jersey, USA, July 27-30, 1996, pages 278-292. IEEE, 1996. Google Scholar
  18. Peter Höfner. Algebraic calculi for hybrid systems. PhD thesis, University of Augsburg, 2009. URL: http://opus.bibliothek.uni-augsburg.de/volltexte/2010/1481/.
  19. Peter Höfner and Bernhard Möller. Fixing Zeno gaps. Theoretical Computer Science, 412(28):3303-3322, 2011. Festschrift in Honour of Jan Bergstra. Google Scholar
  20. Christoph Lüth and Neil Ghani. Composing monads using coproducts. In M. Wand and S. L. Peyton Jones, editors, ICFP'02: Functional Programming, 7th ACM SIGPLAN International Conference, pages 133-144. ACM, 2002. Google Scholar
  21. Saunders Mac Lane. Categories for the Working Mathematician. Springer, 1971. Google Scholar
  22. Stefan Milius. Completely iterative algebras and completely iterative monads. Inf. Comput., 196(1):1-41, 2005. Google Scholar
  23. Eugenio Moggi. A modular approach to denotational semantics. In Category Theory and Computer Science, CTCS 1991, volume 530 of LNCS, pages 138-139. Springer, 1991. Google Scholar
  24. Katsunori Nakamura and Akira Fusaoka. On transfinite hybrid automata. In Manfred Morari and Lothar Thiele, editors, Hybrid Systems: Computation and Control, pages 495-510, Berlin, Heidelberg, 2005. Springer Berlin Heidelberg. Google Scholar
  25. Renato Neves. Hybrid programs. PhD thesis, Minho University, 2018. Google Scholar
  26. Renato Neves, Luis S. Barbosa, Dirk Hofmann, and Manuel A. Martins. Continuity as a computational effect. Journal of Logical and Algebraic Methods in Programming, 85(5, Part 2):1057-1085, 2016. Articles dedicated to Prof. J. N. Oliveira on the occasion of his 60th birthday. Google Scholar
  27. Lawrence Perko. Differential equations and dynamical systems, volume 7. Springer Science &Business Media, 2013. Google Scholar
  28. André Platzer. Logical Analysis of Hybrid Systems: Proving Theorems for Complex Dynamics. Springer, Heidelberg, 2010. Google Scholar
  29. Alex Simpson and Gordon Plotkin. Complete axioms for categorical fixed-point operators. In Logic in Computer Science, LICS 2000, pages 30-41, 2000. Google Scholar
  30. Kohei Suenaga and Ichiro Hasuo. Programming with infinitesimals: A while-language for hybrid system modeling. In International Colloquium on Automata, Languages, and Programming, pages 392-403. Springer, 2011. Google Scholar
  31. Paulo Tabuada. Verification and Control of Hybrid Systems - A Symbolic Approach. Springer, 2009. Google Scholar
  32. Hans Witsenhausen. A class of hybrid-state continuous-time dynamic systems. IEEE Transactions on Automatic Control, 11(2):161-167, 1966. Google Scholar
  33. Jun Zhang, Karl Henrik Johansson, John Lygeros, and Shankar Sastry. Zeno hybrid systems. International Journal of Robust and Nonlinear Control, 11(5):435-451, 2001. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact