Document Open Access Logo

Motion Session Types for Robotic Interactions (Brave New Idea Paper)

Authors Rupak Majumdar, Marcus Pirron, Nobuko Yoshida , Damien Zufferey

PDF
Thumbnail PDF

File

LIPIcs.ECOOP.2019.28.pdf
  • Filesize: 3.43 MB
  • 27 pages

Document Identifiers

Author Details

Rupak Majumdar
  • MPI-SWS, Saarbrücken, Germany
Marcus Pirron
  • MPI-SWS, Saarbrücken, Germany
Nobuko Yoshida
  • Imperial College London, UK
Damien Zufferey
  • MPI-SWS, Saarbrücken, Germany

Funding

  • Majumdar, Rupak: DFG 389792660 https://perspicuous-computing.science, ERC Synergy Grant 610150.
  • Pirron, Marcus: DFG 389792660 https://perspicuous-computing.science, ERC Synergy Grant 610150.
  • Yoshida, Nobuko: EPSRC EP/K034413/1, EP/K011715/1, EP/L00058X/1, EP/N027833/1 and EP/N028201/1.
  • Zufferey, Damien: DFG 389792660 https://perspicuous-computing.science, ERC Synergy Grant 610150.

Cite AsGet BibTex

Rupak Majumdar, Marcus Pirron, Nobuko Yoshida, and Damien Zufferey. Motion Session Types for Robotic Interactions (Brave New Idea Paper). In 33rd European Conference on Object-Oriented Programming (ECOOP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 134, pp. 28:1-28:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
https://doi.org/10.4230/LIPIcs.ECOOP.2019.28

Abstract

Robotics applications involve programming concurrent components synchronising through messages while simultaneously executing motion primitives that control the state of the physical world. Today, these applications are typically programmed in low-level imperative programming languages which provide little support for abstraction or reasoning. We present a unifying programming model for concurrent message-passing systems that additionally control the evolution of physical state variables, together with a compositional reasoning framework based on multiparty session types. Our programming model combines message-passing concurrent processes with motion primitives. Processes represent autonomous components in a robotic assembly, such as a cart or a robotic arm, and they synchronise via discrete messages as well as via motion primitives. Continuous evolution of trajectories under the action of controllers is also modelled by motion primitives, which operate in global, physical time. We use multiparty session types as specifications to orchestrate discrete message-passing concurrency and continuous flow of trajectories. A global session type specifies the communication protocol among the components with joint motion primitives. A projection from a global type ensures that jointly executed actions at end-points are communication safe and deadlock-free, i.e., session-typed components do not get stuck. Together, these checks provide a compositional verification methodology for assemblies of robotic components with respect to concurrency invariants such as a progress property of communications as well as dynamic invariants such as absence of collision. We have implemented our core language and, through initial experiments, have shown how multiparty session types can be used to specify and compositionally verify robotic systems implemented on top of off-the-shelf and custom hardware using standard robotics application libraries.

Subject Classification

ACM Subject Classification
  • Computer systems organization → Robotics
  • Software and its engineering → Concurrent programming languages
  • Theory of computation → Process calculi
  • Theory of computation → Type theory
Keywords
  • Session Types
  • Robotics
  • Concurrent Programming
  • Motions
  • Communications
  • Multiparty Session Types
  • Deadlock Freedom

Metrics

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

References

  1. R. Alur and T.A. Henzinger. Modularity for Timed and Hybrid Systems. In CONCUR '97: Concurrency Theory, volume 1243 of LNCS, pages 74-88. Springer, 1997. Google Scholar
  2. R. Alur, T.A. Henzinger, O. Kupferman, and M.Y. Vardi. Alternating refinement relations. In CONCUR'98 Concurrency Theory, pages 163-178. Springer, 1998. Google Scholar
  3. Davide Ancona, Viviana Bono, Mario Bravetti, Joana Campos, Giuseppe Castagna, Pierre-Malo Denielou, Simon J. Gay, Nils Gesbert, Elena Giachino, Raymond Hu, Einar Broch Johnsen, Francisco Martins, Viviana Mascardi, Fabrizio Montesi, Rumyana Neykova, Nicholas Ng, Luca Padovani, Vasco T. Vasconcelos, and Nobuko Yoshida. Behavioral Types in Programming Languages. FTPL, 3(2-3):95-230, 2016. Google Scholar
  4. Gregor B. Banusic, Rupak Majumdar, Marcus Pirron, Anne-Kathrin Schmuck, and Damien Zufferey. PGCD: robot programming and verification with geometry, concurrency, and dynamics. In Xue Liu, Paulo Tabuada, Miroslav Pajic, and Linda Bushnell, editors, Proceedings of the 10th ACM/IEEE International Conference on Cyber-Physical Systems, ICCPS 2019, Montreal, QC, Canada, April 16-18, 2019, pages 57-66. ACM, 2019. URL: http://dx.doi.org/10.1145/3302509.3311052.
  5. Kerstin Bauer and Klaus Schneider. From synchronous programs to symbolic representations of hybrid systems. In Proceedings of the 13th ACM International Conference on Hybrid Systems: Computation and Control, HSCC 2010, Stockholm, Sweden, April 12-15, 2010, pages 41-50. ACM, 2010. URL: http://dx.doi.org/10.1145/1755952.1755960.
  6. Albert Benveniste, Timothy Bourke, Benoît Caillaud, Jean-Louis Colaço, Cédric Pasteur, and Marc Pouzet. Building a Hybrid Systems Modeler on Synchronous Languages Principles. Proceedings of the IEEE, 106(9):1568-1592, 2018. URL: http://dx.doi.org/10.1109/JPROC.2018.2858016.
  7. J.A. Bergstra and C.A. Middelburg. Process algebra for hybrid systems. Theoretical Computer Science, 335(2):215-280, 2005. Process Algebra. URL: http://dx.doi.org/10.1016/j.tcs.2004.04.019.
  8. Laura Bocchi, Julien Lange, and Nobuko Yoshida. Meeting Deadlines Together. In 26th International Conference on Concurrency Theory, volume 42 of LIPIcs, pages 283-296. Schloss Dagstuhl, 2015. Google Scholar
  9. Laura Bocchi, Weizhen Yang, and Nobuko Yoshida. Timed Multiparty Session Types. In 25th International Conference on Concurrency Theory, volume 8704 of LNCS, pages 419-434. Springer, 2014. Google Scholar
  10. Mario Coppo, Mariangiola Dezani-Ciancaglini, Luca Padovani, and Nobuko Yoshida. A Gentle Introduction to Multiparty Asynchronous Session Types. In SFM, volume 9104 of LNCS, pages 146-178. Springer, 2015. Google Scholar
  11. Pierre-Malo Deniélou and Nobuko Yoshida. Multiparty Session Types Meet Communicating Automata. In ESOP 2012 - European Symposium on Programming. Springer, 2012. URL: http://dx.doi.org/10.1007/978-3-642-28869-2_10.
  12. Pierre-Malo Deniélou, Nobuko Yoshida, Andi Bejleri, and Raymond Hu. Parameterised Multiparty Session Types. Logical Methods in Computer Science, 8(4), 2012. URL: http://dx.doi.org/10.2168/LMCS-8(4:6)2012.
  13. Pierre-Malo Deniélou, Nobuko Yoshida, Andi Bejleri, and Raymond Hu. Parameterised Multiparty Session Types. Logical Methods in Computer Science, 8(4), 2012. URL: http://dx.doi.org/10.2168/LMCS-8(4:6)2012.
  14. Mariangiola Dezani-Ciancaglini, Silvia Ghilezan, Svetlana Jaksic, Jovanka Pantovic, and Nobuko Yoshida. Precise subtyping for synchronous multiparty sessions. In PLACES, volume 203 of EPTCS, pages 29-43, 2015. URL: http://dx.doi.org/10.4204/EPTCS.203.3.
  15. Mariangiola Dezani-Ciancaglini, Silvia Ghilezan, Svetlana Jaksic, Jovanka Pantovic, and Nobuko Yoshida. Denotational and Operational Preciseness of Subtyping: A Roadmap. In Theory and Practice of Formal Methods: Essays Dedicated to Frank de Boer on the Occasion of His 60th Birthday, volume 9660 of LNCS, pages 155-172. Springer, 2016. Google Scholar
  16. Sicun Gao, Soonho Kong, and Edmund M. Clarke. dReal: An SMT solver for nonlinear theories over the reals. In Maria Paola Bonacina, editor, Automated Deduction - CADE-24 - 24th International Conference on Automated Deduction, Lake Placid, NY, USA, June 9-14, 2013. Proceedings, volume 7898 of Lecture Notes in Computer Science, pages 208-214. Springer, 2013. URL: http://dx.doi.org/10.1007/978-3-642-38574-2_14.
  17. Simon Gay and Antonio Ravera, editors. Behavioural Types: from Theory to Tools. River Publishers, 2017. Google Scholar
  18. Silvia Ghilezan, Svetlana Jaksic, Jovanka Pantovic, Alceste Scalas, and Nobuko Yoshida. Precise subtyping for synchronous multiparty sessions. J. Log. Algebr. Meth. Program., 104:127-173, 2019. URL: http://dx.doi.org/10.1016/j.jlamp.2018.12.002.
  19. Sehoon Ha, Stelian Coros, Alexander Alspach, James M. Bern, Joohyung Kim, and Katsu Yamane. Computational Design of Robotic Devices From High-Level Motion Specifications. IEEE Trans. Robotics, 34(5):1240-1251, 2018. URL: http://dx.doi.org/10.1109/TRO.2018.2830419.
  20. Thomas A. Henzinger. Sooner is Safer Than Later. Inf. Process. Lett., 43(3):135-141, 1992. URL: http://dx.doi.org/10.1016/0020-0190(92)90005-G.
  21. Thomas A. Henzinger. The Theory of Hybrid Automata. In Proceedings, 11th Annual IEEE Symposium on Logic in Computer Science, New Brunswick, New Jersey, USA, July 27-30, 1996, pages 278-292. IEEE Computer Society, 1996. URL: http://dx.doi.org/10.1109/LICS.1996.561342.
  22. G.J. Holzmann. The Model Checker SPIN. IEEE Trans. Software Eng., 23(5):279-295, 1997. URL: http://dx.doi.org/10.1109/32.588521.
  23. Kohei Honda. Types for Dyadic Interaction. In CONCUR'93, pages 509-523, 1993. Google Scholar
  24. Kohei Honda, Vasco T. Vasconcelos, and Makoto Kubo. Language Primitives and Type Disciplines for Structured Communication-based Programming. In ESOP, volume 1381 of LNCS, pages 22-138. Springer, 1998. URL: http://dx.doi.org/10.1007/BFb0053567.
  25. Kohei Honda, Nobuko Yoshida, and Marco Carbone. Multiparty Asynchronous Session Types. In POPL, pages 273-284. ACM Press, 2008. Google Scholar
  26. Kohei Honda, Nobuko Yoshida, and Marco Carbone. Multiparty Asynchronous Session Types. Journal of ACM, 63:1-67, 2016. Google Scholar
  27. Hans Hüttel, Ivan Lanese, Vasco T. Vasconcelos, Luís Caires, Marco Carbone, Pierre-Malo Deniélou, Dimitris Mostrous, Luca Padovani, António Ravara, Emilio Tuosto, Hugo Torres Vieira, and Gianluigi Zavattaro. Foundations of Session Types and Behavioural Contracts. ACM Comput. Surv., 49(1), 2016. URL: http://dx.doi.org/10.1145/2873052.
  28. R. Jung, D. Swasey, F. Sieczkowski, K. Svendsen, A. Turon, L. Birkedal, and D. Dreyer. Iris: Monoids and Invariants as an Orthogonal Basis for Concurrent Reasoning. In POPL 15, pages 637-650. ACM, 2015. Google Scholar
  29. Dimitrios Kouzapas and Nobuko Yoshida. Globally Governed Session Semantics. In Pedro R. D'Argenio and Hernán C. Melgratti, editors, CONCUR, volume 8052 of LNCS, pages 395-409. Springer, 2013. Google Scholar
  30. Dimitrios Kouzapas and Nobuko Yoshida. Globally Governed Session Semantics. Logical Methods in Computer Science, 10(4), 2015. Google Scholar
  31. Julien Lange, Emilio Tuosto, and Nobuko Yoshida. From communicating machines to graphical choreographies. In 42nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 221-232. ACM, 2015. Google Scholar
  32. A.M. Mehta, N. Bezzo, P. Gebhard, B. An, V. Kumar, I. Lee, and D. Rus. A Design Environment for the Rapid Specification and Fabrication of Printable Robots. Experimental Robotics, pages 435-449, 2015. Google Scholar
  33. Aaron Meurer, Christopher P. Smith, Mateusz Paprocki, Ondřej Čertík, Sergey B. Kirpichev, Matthew Rocklin, AMiT Kumar, Sergiu Ivanov, Jason K. Moore, Sartaj Singh, Thilina Rathnayake, Sean Vig, Brian E. Granger, Richard P. Muller, Francesco Bonazzi, Harsh Gupta, Shivam Vats, Fredrik Johansson, Fabian Pedregosa, Matthew J. Curry, Andy R. Terrel, Štěpán Roučka, Ashutosh Saboo, Isuru Fernando, Sumith Kulal, Robert Cimrman, and Anthony Scopatz. SymPy: symbolic computing in Python. PeerJ Computer Science, 3:e103, January 2017. URL: http://dx.doi.org/10.7717/peerj-cs.103.
  34. Rumyana Neykova, Laura Bocchi, and Nobuko Yoshida. Timed runtime monitoring for multiparty conversations. Formal Asp. Comput., 29(5):877-910, 2017. Google Scholar
  35. Pierluigi Nuzzo. Compositional Design of Cyber-Physical Systems Using Contracts. PhD thesis, EECS Department, University of California, Berkeley, August 2015. URL: http://www2.eecs.berkeley.edu/Pubs/TechRpts/2015/EECS-2015-189.html.
  36. P.W. O'Hearn. Resources, concurrency, and local reasoning. Theor. Comput. Sci., 375(1-3):271-307, 2007. URL: http://dx.doi.org/10.1016/j.tcs.2006.12.035.
  37. Benjamin C. Pierce. Types and Programming Languages. MIT Press, 2002. Google Scholar
  38. A. Platzer. Logical Analysis of Hybrid Systems - Proving Theorems for Complex Dynamics. Springer, 2010. Google Scholar
  39. K. V. S. Prasad. A Calculus of Broadcasting Systems. Sci. Comput. Program., 25(2-3):285-327, 1995. URL: http://dx.doi.org/10.1016/0167-6423(95)00017-8.
  40. Morgan Quigley, Ken Conley, Brian Gerkey, Josh Faust, Tully Foote, Jeremy Leibs, Rob Wheeler, and Andrew Y Ng. ROS: an open-source Robot Operating System. In ICRA workshop on open source software, 2009. Google Scholar
  41. W.C. Rounds and H. Song. The Phi-Calculus: A Language for Distributed Control of Reconfigurable Embedded Systems. In HSCC, pages 435-449. Springer, 2003. Google Scholar
  42. Alceste Scalas and Nobuko Yoshida. Less is More: Multiparty Session Types Revisited. Proc. ACM Program. Lang., 3(POPL):30:1-30:29, January 2019. URL: http://dx.doi.org/10.1145/3290343.
  43. Kaku Takeuchi, Kohei Honda, and Makoto Kubo. An Interaction-based Language and its Typing System. In PARLE'94, volume 817 of LNCS, pages 398-413, 1994. URL: http://dx.doi.org/10.1007/3-540-58184-7_118.
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 Imprint Privacy Contact