Jonathan DeCastro

Research Scientist
Toyota Research Institute

I am currently at the Toyota Research Institute in Cambridge, MA. I received my Ph.D. in 2017 from Cornell University as an affiliate of the Verifiable Robotics Research Group.

My research interests lie in the intersection of control theory, dynamical systems and formal methods. I have a deep interest in the following topics:

  • Correct-by-construction synthesis of continuous controllers from temporal logic specifications.
  • Algorithms for falsification of interesting system properties, such as safety.
  • Application of formal synthesis, verification, and falsification to robotics applications of all kinds.

One Kendall Square
Cambridge, MA 02139
jonathan.decastro - at - tri - dot - global



J. DeCastro, R. Ehlers, M. Rungger, A. Balkan and H. Kress-Gazit, “Automated Generation of Dynamics-Based Runtime Certificates for High-Level Control,” Journal of Discrete Event Dynamical Systems: Special Topical Issue on Formal Methods in Control, 27(2):371-405, 2017.   [bibtex | link]

J. Alonso-Mora, J. DeCastro, V. Raman, D. Rus and H. Kress-Gazit, “Reactive Mission and Motion Planning while Avoiding Dynamic Obstacles,” Autonomous Robots, August, 2017.   [bibtex | link]

J. DeCastro and H. Kress-Gazit, “Synthesis of Nonlinear Continuous Controllers for Verifiably-Correct High-Level, Reactive Behaviors,” International Journal of Robotics Research, 34(3):378-394, 2015.   [bibtex | link]

J. DeCastro, “Rate-Based Model Predictive Control of Turbofan Engine Clearance,” AIAA Journal of Propulsion and Power, 23(4):804–813, 2007. [bibtex | link]


J. DeCastro, L. Liebenwein, C.-I. Vasile, R. Tedrake, S. Karaman and D. Rus, “Counterexample-Guided Safety Contracts for Autonomous Driving,” The 13th International Workshop on the Algorithmic Foundations of Robotics (WAFR). Mérida, Mexico, December 2018.   [bibtex]

L. Liebenwein, W. Schwarting, C.-I. Vasile, J. DeCastro, J. Alonso-Mora, S. Karaman and D. Rus, “Compositional and Contract-based Verification for Autonomous Driving on Road Networks,” International Symposium on Robotics Research (ISRR). Puerto Varas, Chile, December 2017.   [bibtex | video]

J. DeCastro and H. Kress-Gazit, “Nonlinear Controller Synthesis and Automatic Workspace Partitioning for Reactive High-Level Behaviors,” 19th ACM International Conference on Hybrid Systems: Computation and Control (HSCC). Vienna, Austria, 2016.   [bibtex | video]

J. DeCastro, J. Alonso-Mora, V. Raman, D. Rus and H. Kress-Gazit, “Collision-Free Reactive Mission and Motion Planning for Multi-Robot Systems,” International Symposium on Robotics Research (ISRR). Sestri Levante, Italy, 2015.   [bibtex | video]

J. DeCastro, V. Raman and H. Kress-Gazit, “Dynamics-Driven Adaptive Abstraction for Reactive High-Level Mission and Motion Planning,” IEEE International Conference on Robotics and Automation (ICRA). Seattle, WA, USA, 2015.   [bibtex]

J. DeCastro and H. Kress-Gazit, “Guaranteeing Reactive High-Level Behaviors for Robots with Complex Dynamics,” IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS). Tokyo, Japan, 2013.   [bibtex]

J. DeCastro, L. Tang, B. Zhang and G. Vachtsevanos, “A Safety Verification Approach to Fault-Tolerant Aircraft Supervisory Control,” AIAA Guidance, Navigation, and Control Conference (GNC). Portland, OR, USA, 2011. [bibtex]

J. DeCastro, L. Tang, C. S. Byington and D. E. Culley, “Analysis of Fault-Tolerance and Decentralization Concepts for Distributed Engine Control,” 45th AIAA Joint Propulsion Conference and Exhibit (JPC). Denver, CO, USA, 2009. [bibtex]

Technical Reports

J. DeCastro, R. Ehlers, M. Rungger, A. Balkan, P. Tabuada and H. Kress-Gazit, “Dynamics-Based Reactive Synthesis and Automated Revisions for High-Level Robot Control,”.   [arXiv]

Automatic Synthesis High-Level, Reactive Controllers for Nonlinear Systems

Can we automatically synthesize controllers for robots with dynamics that are capable of fulfilling complex tasks in human environments?

The highlight of this work was an approach for constructing a library of controllers that, collectively, guarantee the sequence of motions as requested by the high-level controller (represented as a finite-state machine). I show that the composition of the low-level controllers for individual behaviors preserve the correctness of the high-level specification under all possible environment behaviors.

This work included, among other aspects, transferring the high-level specification into sound mathematical structures for the low-level controllers, abstraction refinement, and specification repair (specifically, environment assumption refinement).

Relevant publications: [DeCastro & Kress-Gazit (IROS 2013)] [DeCastro & Kress-Gazit (IJRR 2015)] [DeCastro, Raman & Kress-Gazit (ICRA 2015)] [DeCastro & Kress-Gazit (HSCC 2016)]

Low-Complexity Synthesis for Multi-Robot Scenarios with Dynamic Obstacles

In multi-robot scenarios operating in human environments, controller synthesis can quickly become intractible due to the exponential growth of complexity with the number of robots and dynamic obstacles present in the environment. A high-level synthesis scheme that uses a local planner with local collision avoidance guarantees has been adopted to produce a mission planner that is able to correctly coordinate multiple robots in the presence of dynamic obstacles. To avoid exponential complexity, we do not require observation of the global behavior of the dynamic obstacles; instead the controller reasons about behaviors of the dynamic obstacles locally, yet preserves global guarantees of task satisfaction. I demonstrate the runtime features of the approach via experiments involving a heterogeneous team of robots.

Relevant publications: [DeCastro, et. al. (ISRR 2015)]


Simulation Tools for Aircraft Control Systems

I was once a researcher on a team at NASA dedicated to developing the software tool C-MAPSS, a “virtual” engine model now popular among resesarchers around the world to prototype control algorithms and simulation-in-the-loop testbeds. I have partipated in several research projects involving C-MAPSS, including fault-tolerant control algorithms for aircraft, nonlinear engine fault detection algorithms, and several others.

Relevant publications: [DeCastro, et. al. (2011)]

Program Committee Member: Hybrid Systems: Computation and Control (HSCC), 2019 | 2018

Workshop Organizer: “Command Your Own Robot”, Expanding Your Horizons Conference (Cornell U.), 2015 | 2014

Mentor: Soft Robotics Design Competition (two teams), 2015

  • First Prize (out of 82 teams)
  • Honorable Mention for outstanding project idea

Voting Member: Cornell Graduate and Professional Student Assembly, 2014 | 2013

Course Instructor: "Systems Modeling", Rochester Institute of Technology, Winter 2010-2011