×

zbMATH — the first resource for mathematics

Formal composition of hybrid systems. (English) Zbl 1448.18005
This paper aims to construct a physically-grounded compositional framework for hybrid system synthesis, particularly targeted at applications in robotics. Compositionality lies at the heart of language in general [M. Werning et al., The Oxford handbook of compositionality. Oxford Handbooks in Linguistics (2012)], its formalization underlying much of computer science [J. van Leeuwen (ed.), Formal models and semantics. Handbook of theoretical computer science. Vol. B. Amsterdam etc.: Elsevier (1990; Zbl 0714.68001)]. The formalism in this paper is inspired by three distinct notions of behavioral composition, namely, sequential composition, hierarchical composition and parallel composition. The paper formalizes a useful subset of each of these three motivating concepts by using category theory which is particularly effective in description of composition and abstraction. What is more significant, the Curry-Howard correspondence enables one to transfer the categorical results in this paper to the setting of functional programming. Although connections to robotic behavioral programming are not explored in this paper, developing more physically grounded analogues of existing formal approaches to motion planning in use of linear-time temporal logic and functional reactive programming are involved in the authors’ long-term ambitions. Similarly, the construction of exponential objects for hybrid systems categories, which is a inevitable step in constructing a full-fledged functional programming language for hybrid systems is not addressed, presumably requiring more careful consideration. This paper is the first step in this long journey, the main contribution being the investigation of a series of categories of hybrid systems that are both mathematically rigorous and also loyal to the way that robotics engineers usually approach model development. This paper was inspired by E. Lerman’s elegant definition of a category of hybrid systems and semiconjugacies (loosely speaking, execution-preserving maps) in [A category of hybrid systems”, Preprint, arXiv:1612.01950].
Since robotics applications inevitably incur sudden transitions between dynamics and state spaces cosequent upon the making and breaking of different contacts with different portions of the environment, this paper must depart from classical theory to embrace a notion of hybrid dynamical systems. The authors are primarily interested in a formalism focused on non-blocking and deterministic [E. Lerman and J. Schmidt, “Networks of hybrid open systems”, Preprint, arXiv:1908.10447] executions, which are hybrid versions of existence and uniqueness in classical dynamical systems theory.
Sequential composition formalizes notions of pre-image back-chaining [T. Lozano-Perez et al., “Automatic synthesis of fine-motion strategies for robots”, Int. J. Robot. Res. 3, No. 1, 3–24 (1984)], earning wide attention in robotics as corresponding to broadly useful event-based concatenation of behavior over time. The authors formulates a notion of directed hybrid system, a system in which a generic execution flows from a domain subsystem to a codomain subsystem, providing a basis for modeling simple robotic behaviors as directed hybrid systems of specified initial and final interfaces available for linking behaviors to achieve more complex behaviors. It is shown that there exists a double category of hybrid systems where directed systems are the horizontal morphisms and semiconjugacies form the vertical morphisms, providing a setting for exploring both model abstraction together with sequential composition.
Hierarchical composition has a still older pedigree, based on the folklore dynamical systems collapse of dimension concept, deeply engrained in the literature. The authors formalize the notion of a template-anchor pair of hybrid systems. In dynamical systems theory, a template is a low degree of freedom, idealized model of a physical system, while an anchor corresponding to such a template is a high degree of freedom, more realistic model of the same system. A template-anchor pair consists of an embedding of a template model as an attracting, invariant subsystem of a corresponding anchor model. As long as trajectories in the anchor converge to the template sufficiently promptly, the dynamics of the template gives a good approximation for the dynamics of the anchor. In the continuous setting, template-anchor pairs are of a splendid and well-established theory [J. Eldering et al., Nonlinearity 31, No. 9, 4202–4245 (2018; Zbl 1396.37035)]. Unfortunately, mismatches between resets in templates and anchors complicate the theory in the hybrid setting. To address these complications, the authors introduce formal subdivisions of hybrid systems, namely, semiconjugacies abiding by a fiber product property for execution, allowing one to add formal resets to template systems. The authors then define a template-anchor pair as a span for which the left leg is a template, the roof is a subdivision of the template, and the right morphism embeds this subdivision into the anchor as an attracting, invariant subsystem, hierachical composition corresponding to composing spans by taking a fiber product of subdivisions over a system that is both an anchor for a simpler template and a template for a more complicated anchor.
Parallel composition, which is a simultaneous operation of distinct behaviors of the same body, has only relatively recently been achieved in an empirically reliable form suitable to highly energetic mechanisms [M. H. Raibert, Legged robots that balance. Cambridge: MIT Press (1986)] with a corresponding mathematical theory only burgeoning recently [A. De and D. E. Koditschek, “Parallel composition of templates for tail-energized planar hopping”, in: IEEE International Conference on Robotics and Automation (ICRA), 4562–4569 (2015746); “Vertical hopper compositions for preflexive and feedback-stabilized quadrupedal bounding, pacing, pronking, and trotting”, Int. J. Robot. Res. 37, No. 7, 743–778 (2018)] inspired by the challenges of circumventing destabilizing cross-talk [D. E. Whitney, “Why mechanical design cannot be like VLSI design”, Res. Eng. Design 8, 125–138 (1996)]. As a first attempt at parallel composition, this paper concentrates on combining decoupled hybrid systems, showing that the category of hybrid systems is cartesian. A similar result is obtained in [arXiv:1908.10447], where more complex coupled systems are explored using interconnection maps. This paper is interested in connections between parallel composition and the other two forms of composition under consideration.
This review is concluded with a criticism against the authors’ references. The authors refers to a paper, e.g., simply as [JBK 16] in the text, which presumably points to \begin{align*} & \text{Aaron M. Johnson, Samuel A. Burden, and Daniel E. Koditschek},\\ & \text{ A hybrid systems model for simple manipulation and self-manipulation systems,}\\ & \text{The International Journal of Robotics Research }\boldsymbol{35}\text{ (2016), no.11, 1354-1392.} \end{align*} in References, which is highly irritating and cumbersome to find out. Why did they hesitate to write in the References as follows. \begin{align*} \text{\lbrack JBK16]} & \text{ Aaron M. Johnson, Samuel A. Burden, and Daniel E. Koditschek},\\ & \text{A hybrid systems model for simple manipulation and self-manipulation systems, }\\ & \text{The International Journal of Robotics Research }\boldsymbol{35}\text{ (2016), no.11, 1354-1392.} \end{align*}

MSC:
18B20 Categories of machines, automata
18N10 2-categories, bicategories, double categories
PDF BibTeX XML Cite
Full Text: Link
References:
[1] Omur Arslan and Daniel E. Koditschek,Sensor-based reactive navigation in unknown convex sphere worlds, The International Journal of Robotics Research (2018), 0278364918796267.
[2] Luisa Albasini, Nicoletta Sabadini, and Robert FC Walters,Cospans and spans of graphs: a categorical algebra for the sequential and parallel composition of discrete systems, arXiv:0909.4136, 2009.
[3] N. A. Bernstein,The coordination and regulation of movements, Pergamon Press, 1967.
[4] R. R. Burridge, A. A. Rizzi, and D. E. Koditschek,Sequential composition of dynamically dexterous robot behaviors, The International Journal of Robotics Research18(1999), no. 6, 534-555.
[5] Michael Barr and Charles Wells,Category theory for computing science, vol. 49, Prentice Hall New York, 1990. · Zbl 0714.18001
[6] Charles C. Conley,Isolated invariant sets and the Morse index, no. 38, American Mathematical Soc., 1978. · Zbl 0397.34056
[7] A. De and D. E. Koditschek,Parallel composition of templates for tail-energized planar hopping, 2015 IEEE International Conference on Robotics and Automation (ICRA), May 2015, p. 4562-4569.
[8] Avik De and Daniel E. Koditschek,Vertical hopper compositions for preflexive and feedback-stabilized quadrupedal bounding, pacing, pronking, and trotting, The International Journal of Robotics Research37(2018), no. 7, 743-778.
[9] Charles Ehresmann,Cat´egories structur´ees, Annales scientifiques de l’´Ecole Normale Sup´erieure, vol. 80, 1963, pp. 349-426.
[10] Jaap Eldering, Matthew Kvalheim, and Shai Revzen,Global linearization and fiber bundle structure of invariant manifolds, Nonlinearity31(2018), no. 9, 4202-4245. · Zbl 1396.37035
[11] Robert Full and Daniel Koditschek,Templates and anchors: Neuromechanical hypotheses of legged locomotion on land, J. of Experimental Biology202(1999), no. 23, 3325-3332.
[12] Richard E. Fikes and Nils J. Nilsson,Strips: A new approach to the application of theorem proving to problem solving, Artificial intelligence2(1971), no. 3-4, 189-208. · Zbl 0234.68036
[13] Marco Grandis and Robert Par´e,Limits in double categories, Cahiers de topologie et g´eom´etrie diff´erentielle cat´egoriques40(1999), no. 3, 162-220.
[14] Rafal Goebel, Ricardo G Sanfelice, and Andrew R Teel,Hybrid dynamical systems, IEEE control systems magazine29(2009), no. 2, 28-93. · Zbl 1395.93001
[15] Paul Hudak, Antony Courtney, Henrik Nilsson, and John Peterson,Arrows, robots, and functional reactive programming, International School on Advanced Functional Programming, Springer, 2002, pp. 159-187.
[16] P. Holmes, R. J. Full, D. E. Koditschek, and J. Guckenheimer,The dynamics of legged locomotion: Models, analyses, and challenges, SIAM Review48(2006), no. 2, 207-304. · Zbl 1100.34002
[17] Esfandiar Haghverdi, Paulo Tabuada, and George J. Pappas,Bisimulation relations for dynamical, control, and hybrid systems, Theoretical Computer Science342(2005), no. 2-3, 229-261. · Zbl 1077.68062
[18] Mike Hurley,Attractors: persistence, and density of their basins, Transactions of the American Mathematical Society269(1982), no. 1, 247-271. · Zbl 0494.58023
[19] Aaron M. Johnson, Samuel A. Burden, and Daniel E. Koditschek,A hybrid systems model for simple manipulation and self-manipulation systems, The International Journal of Robotics Research35(2016), no. 11, 1354-1392.
[20] 1680J. CULBERTSON, P. GUSTAFSON, D.E. KODITSCHEK, AND P.F. STILLER
[21] Andr´e Joyal, Mogens Nielsen, and Glynn Winskel,Bisimulation from open maps, Information and Computation127(1996), no. 2, 164-185. · Zbl 0856.68067
[22] Hadas Kress-Gazit, Georgios E Fainekos, and George J Pappas,Temporal-logic-based reactive mission and motion planning, IEEE transactions on robotics25(2009), no. 6, 1370-1381. · Zbl 1158.93369
[23] Anders Kock,Synthetic differential geometry, vol. 333, Cambridge University Press, 2006. · Zbl 1091.51002
[24] D. E. Koditschek,The application of total energy as a Lyapunov function for mechanical control systems, Dynamics and Control of Multibody Systems, vol. 97, AMS, 1989, pp. 131-157. · Zbl 0692.70029
[25] Matthew Kvalheim and Shai Revzen,Reverse-engineering invariant manifolds with asymptotic phase, arXiv:1608.08442, Aug 2016. · Zbl 1396.37035
[26] Piergiulio Katis, Nicoletta Sabadini, and Robert FC Walters,Span (graph): A categorical algebra of transition systems, International Conference on Algebraic Methodology and Software Technology, Springer, 1997, pp. 307-321. · Zbl 0885.18004
[27] Joseph P. LaSalle,Stability theory for ordinary differential equations, Journal of Differential Equations4(1968), no. 1, 57-65. · Zbl 0159.12002
[28] Steven Michael LaValle,Planning algorithms, Cambridge university press, 2006. · Zbl 1100.68108
[29] Jan V. Leeuwen,Handbook of theoretical computer science: Formal models and semantics, MIT Press, 1990. · Zbl 0714.68001
[30] John M. Lee,Introduction to Smooth Manifolds, Graduate Texts in Mathematics, no. 218, Springer, 2003.
[31] Eugene Lerman,A category of hybrid systems, arXiv:1612.01950v1, 2016.
[32] John Lygeros, Karl Henrik Johansson, Slobodan N Simic, Jun Zhang, and Shankar S Sastry,Dynamical properties of hybrid automata, IEEE Transactions on automatic control48(2003), no. 1, 2-17. · Zbl 1364.93503
[33] John Lygeros, Karl Henrik Johansson, Shankar Sastry, and Magnus Egerstedt,On the existence of executions of hybrid automata, Proceedings of the 38th IEEE Conference on Decision and Control (Cat. No. 99CH36304), vol. 3, IEEE, 1999, pp. 2249-2254.
[34] T. Lozano-Perez, M. T. Mason, and R. H. Taylor,Automatic synthesis of fine-motion strategies for robots, The International Journal of Robotics Research3(1984), no. 1, 3-24.
[35] Fosco Loregian and Emily Riehl,Categorical notions of fibration, Expositiones Mathematicae (2019).
[36] EugeneLermanandJamesSchmidt,Networksofhybridopensystems, arXiv:1908.10447v1, 2019.
[37] C. Mead and L. Conway,Introduction to VLSI systems, Addison-Wesley Reading, MA, 1980.
[38] C. Mead,Analog and neural systems, Addison-Wesley Boston, 1989. · Zbl 0715.68002
[39] John Milnor,On the concept of attractor: Correction and remarks, Communications in Mathematical Physics102(1985), no. 3, 517-519. · Zbl 0602.58030
[40] J. W. Milnor,Attractor, Scholarpedia1(2006), no. 11, 1815, revision #186525. · Zbl 0595.58028
[41] Ieke Moerdijk and Gonzalo E Reyes,Models for smooth infinitesimal analysis, Springer Science & Business Media, 2013. · Zbl 0715.18001
[42] Kiisa Nishikawa, Andrew A. Biewener, Peter Aerts, Anna N. Ahn, Hillel J. Chiel, Monica A. Daley, Thomas L. Daniel, Robert J. Full, Melina E. Hale, Tyson L. Hedrick, and et al.,Neuromechanics: an integrative approach for understanding motor control, Integrative and Comparative Biology47(2007), no. 1, 16-54.
[43] M. H. Raibert,Legged robots that balance, Cambridge: MIT Press, 1986. · Zbl 0709.70504
[44] Emily Riehl,Category theory in context, Courier Dover Publications, 2017. · Zbl 1348.18001
[45] Alfred A. Rizzi and Daniel E. Koditschek,Further progress in robot juggling: Solvable mirror laws, proceedings of the 1994 IEEE international conference on Robotics and Automation, IEEE, 1994, pp. 2935-2940.
[46] Michael A. Shulman,Constructing symmetric monoidal bicategories, arXiv:1004.0993, 2010.
[47] Slobodan N. Simic, Karl H. Johansson, John Lygeros, and Shankar Sastry,Structural stability of hybrid systems, 2001 European Control Conference (ECC), IEEE, 2001, pp. 3858-3863. · Zbl 0963.93044
[48] Slobodan N. Simi´c, Karl Henrik Johansson, Shankar Sastry, and John Lygeros,Towards a geometric theory of hybrid systems, International Workshop on Hybrid Systems: Computation and Control, Springer, 2000, pp. 421-436. · Zbl 0963.93044
[49] U. Saranli, W. J. Schwind, and D. E. Koditschek,Toward the control of a multi-jointed, monoped runner, Robotics and Automation, 1998. Proceedings. 1998 IEEE International Conference on, vol. 3, IEEE, 1998, p. 2676-2682.
[50] 1682J. CULBERTSON, P. GUSTAFSON, D.E. KODITSCHEK, AND P.F. STILLER
[51] Steven Strogatz,Nonlinear dynamics and chaos: with applications to physics, biology, chemistry and engineering, Perseus, 1994. · Zbl 1343.37001
[52] D. E. Whitney,Why mechanical design cannot be like VLSI design, Research in Engineering Design8(1996), no. 3, 125-138.
[53] Markus Werning, Wolfram Hinzen, and Edouard Machery,The oxford handbook of compositionality, Oxford Handbooks in Linguistic, 2012.
[54] Guang-Zhong Yang, Jim Bellingham, Pierre E. Dupont, Peer Fischer, Luciano Floridi, Robert Full, Neil Jacobstein, Vijay Kumar, Marcia McNutt, Robert Merrifield, and et al.,The grand challenges of science robotics, Science Robotics3(2018), no. 14, eaar7650.
[55] Autonomy Capabilities Team, Air Force Research Laboratory
[56] Dayton, OH 45433, USA
[57] Department of Electrical Engineering, Wright State University
[58] Dayton, OH 45435, USA
[59] School of Engineering and Applied Science, University of Pennsylvania
[60] Philadelphia, PA 19104, USA
[61] Department of Mathematics, Texas A&M University
[62] College Station, TX, 77840, USA
[63] Email:jared.culbertson@us.af.mil paul.gustafson@wright.edu kod@seas.upenn.edu stiller@math.tamu.edu
[64] This article may be accessed athttp://www.tac.mta.ca/tac/
[65] THEORY AND APPLICATIONS OF CATEGORIES will disseminate articles that significantly advance
[66] the study of categorical algebra or methods, or that make significant new contributions to mathematical
[67] science using categorical methods. The scope of the journal includes: all areas of pure category theory,
[68] including higher dimensional categories; applications of category theory to algebra, geometry and topology
[69] and other areas of mathematics; applications of category theory to computer science, physics and other
[70] mathematical sciences; contributions to scientific knowledge that make use of categorical methods.
[71] Articles appearing in the journal have been carefully and critically refereed under the responsibility of
[73] for publication.
[74] Subscription informationIndividual subscribers receive abstracts of articles by e-mail as they
[75] are published. To subscribe, send e-mail totac@mta.caincluding a full name and postal address. Full
[76] text of the journal is freely available athttp://www.tac.mta.ca/tac/.
[77] Information for authorsLATEX2e is required. Articles may be submitted in PDF by email
[78] directly to a Transmitting Editor following the author instructions at
[79] http://www.tac.mta.ca/tac/authinfo.html.
[80] Managing editor.Geoff Cruttwell, Mount Allison University:gcruttwell@mta.ca
[81] TEXnical editor.Michael Barr, McGill University:michael.barr@mcgill.ca
[82] Assistant TEX editor.Gavin Seal, Ecole Polytechnique F´ed´erale de Lausanne:
[83] gavin seal@fastmail.fm
[84] Transmitting editors.
[85] Clemens Berger, Universit´e de Nice-Sophia Antipolis:cberger@math.unice.fr
[86] Julie Bergner, University of Virginia:jeb2md (at) virginia.edu
[87] Richard Blute, Universit´e d’ Ottawa:rblute@uottawa.ca
[88] Gabriella B¨ohm, Wigner Research Centre for Physics:bohm.gabriella (at) wigner.mta.hu
[89] Valeria de Paiva: Nuance Communications Inc:valeria.depaiva@gmail.com
[90] Richard Garner, Macquarie University:richard.garner@mq.edu.au
[91] Ezra Getzler, Northwestern University:getzler (at) northwestern(dot)edu
[92] Kathryn Hess, Ecole Polytechnique F´ed´erale de Lausanne:kathryn.hess@epfl.ch
[93] Dirk Hofmann, Universidade de Aveiro:dirk@ua.pt
[94] Pieter Hofstra, Universit´e d’ Ottawa:phofstra (at) uottawa.ca
[95] Anders Kock, University of Aarhus:kock@math.au.dk
[96] Joachim Kock, Universitat Aut‘onoma de Barcelona:kock (at) mat.uab.cat
[97] Stephen Lack, Macquarie University:steve.lack@mq.edu.au
[98] Tom Leinster, University of Edinburgh:Tom.Leinster@ed.ac.uk
[99] Matias Menni, Conicet and Universidad Nacional de La Plata, Argentina:matias.menni@gmail.com
[100] Ieke Moerdijk, Utrecht University:i.moerdijk@uu.nl
[101] Susan Niefield, Union College:niefiels@union.edu
[102] Kate Ponto, University of Kentucky:kate.ponto (at) uky.edu
[103] Robert Rosebrugh, Mount Allison University:rrosebrugh@mta.ca
[104] Jiri Rosicky, Masaryk University:rosicky@math.muni.cz
[105] Giuseppe Rosolini, Universit‘a di Genova:rosolini@disi.unige.it
[106] Alex Simpson, University of Ljubljana:Alex.Simpson@fmf.uni-lj.si
[107] James Stasheff, University of North Carolina:jds@math.upenn.edu
[108] Ross Street, Macquarie University:ross.street@mq.edu.au
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.