Correct-by-Construction Synthesis of Control Protocols for Aerospace Systems

Current participants: Stephanie Tsuei (CDS MS student) Eric Wolff* (CDS PhD student) * External funding

Past participants: Scott Livingston (CDS PhD student) Ufuk Topcu (Postdoc, CDS) Pete Trautman (PhD student, CDS) Clemens Wilsche* (visiting student, ETHZ)

Objectives

We are developing theory and algorithms for model-based verification and synthesis of control protocols. This includes development of specifications for desired system behavior and methods for synthesizing control protocols to achieve the specification. Target areas that we are currently exploring include:

• Protocols for real-time, multi-agent, airborne communication networks, including air-to-air, air-to-ground and satellite-based communications
• Vehicle management systems, including embedded control protocols individual and integrated subsystems
• Decision-making, resource allocation and fault handling in unmanned, autonomous vehicles and mission systems
• Aircraft electric power distribution systems.

Publications

• Synthesis of Distributed Longitudinal Control 1 Protocols for a Platoon of Autonomous Vehicles. Duo Han, Yilin Mo, Richard M. Murray. Submitted, 2015 Conference on Decision and Control (CDC).
• Control System Analysis on Symmetric Cones. Ivan Papusha and Richard M. Murray. Submitted, 2015 Conference on Decision and Control (CDC).
• A Compositional Approach to Stochastic Optimal Control with Co-safe Temporal Logic Specifications. Matanya B. Horowitz, Eric M. Wolff, Richard M. Murray. 2014 IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS).
• Efficient control synthesis for augmented finite transition systems with an application to switching protocols. Fei Sun, Necmiye Ozay, Eric M. Wolff, Jun Liu and Richard M. Murray. Submitted, 2014 American Control Conference (ACC).
• A Compositional Approach to Stochastic Optimal Control with Temporal Logic Specifications. Matanya B. Horowitz, Eric M. Wolff, Richard M. Murray. Submitted, 2014 American Control Conference (ACC).
• Moving bounding boxes and incremental synthesis for dynamic obstacles. Scott C. Livingston and Richard M. Murray. Submitted, 2014 International Conference on Robotics and Automation (ICRA).
• Optimization-based Control of Nonlinear Systems with Linear Temporal Logic Specifications. Eric M. Wolff, Ufuk Topcu, and Richard M. Murray. Submitted, 2014 International Conference on Robotics and Automation (ICRA).
• Optimal Control of Nonlinear Systems with Temporal Logic Specifications. Eric M. Wolff and Richard M. Murray. Submitted, 2013 International Symposium on Robotics Research (ISRR).
• Automaton-Guided Controller Synthesis for Nonlinear Systems with Temporal Logic. Eric M. Wolff, Ufuk Topcu, and Richard M. Murray. To appear, 2013 International Conference on Intelligent Robots and Systems (IROS).
• Optimal Control of Non-deterministic Systems for a Computationally Efficient Fragment of Temporal Logic. Eric M. Wolff, Ufuk Topcu, and Richard M. Murray. 2013 Conference on Decison and Control (CDC).
• Synthesis of Control Protocols for Autonomous Systems. Tichakorn Wongpiromsarn, Ufuk Topcu and Richard M. Murray. Unmanned Systems, 1(1):21-39 (2013).
• An Aircraft Electric Power Testbed for Validating Automatically Synthesized Reactive Control Protocols. Robert Rogersten, Huan Xu, Necmiye Ozay, Ufuk Topcu, and Richard M. Murray. Submitted, Hybrid Systems: Computation and Control (HSCC) 2013.
• Pre-orders for Reasoning about Input-to-State Stability Properties of Hybrid Systems. Pavithra Prabhakar, Jun Liu and Richard M. Murray. Submitted, Hybrid Systems: Computation and Control (HSCC) 2013.
• Computing Augmented Finite Transition Systems to Synthesize Switching Protocols for Polynomial Switched Systems. Necmiye Ozay, Jun Liu, Pavithra Prabhakar, and Richard M. Murray. 2013 American Control Conference (ACC).
• Convex optimal uncertainty quantification: Algorithms and a case study in energy storage placement for power grids. Shuo Han, Ufuk Topcu, Molei Tao, Houman Owhadi, Richard M. Murray. To appear, 2013 American Control Conference (ACC).
• Just-in-time synthesis for motion planning with temporal logic. Scott C. Livingston and Richard M. Murray. 2013 International Conference on Robotics and Automation (ICRA).
• Efficient reactive controller synthesis for a fragment of linear temporal logic. Eric M. Wolff, Ufuk Topcu, and Richard M. Murray. Submitted, 2013 International Conference on Robotics and Automation (ICRA).
• Patching task-level robot controllers based on a local μ-calculus formula. Scott C. Livingston, Pavithra Prabhakar, Alex B. Jose and Richard M. Murray. 2013 International Conference on Robotics and Automation (ICRA).
• Robot Navigation in Dense Human Crowds: the Case for Cooperation. Pete Trautman, Jeremy Ma, Richard M. Murray and Andreas Krause. Submitted, 2013 International Conference on Robotics and Automation.
• Synthesis of Reactive Switching Protocols from Temporal Logic Specifications. Jun Liu, Necmiye Ozay, Ufuk Topcu, and Richard M. Murray. To appear, IEEE T. Automatic Control.
• Reactive Protocols for Aircraft Electric Power Distribution. Huan Xu, Ufuk Topcu, and Richard M. Murray. 2012 Conference on Decision and Control (CDC).
• Synthesis of Reactive Control Protocols for Differentially Flat Systems. Jun Liu, Ufuk Topcu, Necmiye Ozay, and Richard M. Murray. 2012 Conference on Decision and Control (CDC).
• Towards Formal Synthesis of Reactive Controllers for Dexterous Robotic Manipulation. Sandeep Chinchali, Scott C. Livingston, Ufuk Topcu, Joel W. Burdick, and Richard M. Murray. 2012 International Conference on Robotics and Automation (ICRA).
• On Synthesizing Robust Discrete Controllers under Modeling Uncertainty. Ufuk Topcu, Necmiye Ozay, Jun Liu, and Richard M. Murray. Submitted, 2012 International Conf on Hybrid Systems: Computation and Control (HSCC).
• Synthesis of Switching Protocols from Temporal Logic Specifications. Jun Liu, Necmiye Ozay, Ufuk Topcu and Richard M. Murray. Submitted, 2012 American Control Conference.
• Temporal Logic Control of Switched Affine Systems with an Application in Fuel Balancing. Petter Nilsson, Necmiye Özay, Ufuk Topcu and Richard M. Murray. Submitted, 2012 American Control Conference (ACC).
• Robust Control of Uncertain Markov Decision Processes with Temporal Logic Specifications. Eric M. Wolff, Ufuk Topcu and Richard M. Murray. Submitted, 2012 American Control Conference (ACC).
• Backtracking temporal logic synthesis for uncertain environments. Scott C. Livingston, Richard M. Murray and Joel W. Burdick. 2012 International Conference on Robotics and Automation (ICRA), submitted.
• Distributed Power Allocation for Vehicle Management Systems. Necmiye Ozay, Ufuk Topcu and Richard M. Murray. 2011 IEEE Conference on Decision and Control (CDC).
• Optimization-Based Navigation for the DARPA Grand Challenge. Dmitriy Kogan and Richard M. Murray. Submitted, 2006 Conference on Decision and Control.
• Efficient control synthesis for augmented finite transition systems with an application to switching protocols, Fei Sun, Necmiye Ozay, Eric M. Wolff, Jun Liu, and Richard M. Murray. Submitted, 2014 American Control Conference (ACC).

• A compositional approach to stochastic optimal control with temporal logic specifications, Matanya Horowitz, Eric M. Wolff, and Richard M. Murray. Submitted, 2014 American Control Conference (ACC).

• Moving bounding boxes and incremental synthesis for dynamic obstacles, Scott C. Livingston, Richard M. Murray. Submitted, 2014 International Conference on Robotics and Automation (ICRA).

• Optimization-based control of nonlinear systems with linear temporal logic specifications, Eric M. Wolff, Ufuk Topcu, and Richard M. Murray. Submitted, 2014 International Conference on Robotics and Automation (ICRA).

• Optimal control of nonlinear systems with temporal logic specifications, Eric M. Wolff and Richard M. Murray. To appear, 2013 International Symposium on Robotics Research (ISRR).

• Automaton-Guided Controller Synthesis for Nonlinear Systems with Temporal Logic, Eric M. Wolff, Ufuk Topcu, and Richard M. Murray. 2013 International Conference on Intelligent Robots and Systems (IROS).

• Optimal Control of Non-deterministic Systems for a Computationally Efficient Fragment of Temporal Logic, Eric M. Wolff, Ufuk Topcu, and Richard M. Murray. To appear, 2013 Conference on Decison and Control (CDC).

• Computing Augmented Finite Transition Systems to Synthesize Switching Protocols for Polynomial Switched Systems, Necmiye Ozay, Jun Liu, Pavithra Prabhakar, and Richard M. Murray. 2013 American Control Conference (ACC)

• Just-in-time synthesis for motion planning with temporal logic, Scott C. Livingston and Richard M. Murray. 2013 International Conference on Robotics and Automation (ICRA)

• Efficient reactive controller synthesis for a fragment of linear temporal logic, Eric M. Wolff, Ufuk Topcu, and Richard M. Murray. 2013 International Conference on Robotics and Automation (ICRA)

• Patching task-level robot controllers based on a local μ-calculus formula, Scott C. Livingston, Pavithra Prabhakar, Alex B. Jose and Richard M. Murray. 2013 International Conference on Robotics and Automation (ICRA)

• Robot Navigation in Dense Human Crowds: the Case for Cooperation, Pete Trautman, Jeremy Ma, Richard M. Murray and Andreas Krause. 2013 International Conference on Robotics and Automation

• Synthesis of Reactive Switching Protocols from Temporal Logic Specifications, Jun Liu, Necmiye Ozay, Ufuk Topcu, and Richard M. Murray. Submitted, IEEE T. Automatic Control

• Reactive Protocols for Aircraft Electric Power Distribution, Huan Xu, Ufuk Topcu, and Richard M. Murray. 2012 Conference on Decision and Control (CDC)

• Synthesis of Reactive Control Protocols for Differentially Flat Systems, Jun Liu, Ufuk Topcu, Necmiye Ozay, and Richard M. Murray. 2012 Conference on Decision and Control (CDC)

• Towards Formal Synthesis of Reactive Controllers for Dexterous Robotic Manipulation, Sandeep Chinchali, Scott C. Livingston, Ufuk Topcu, Joel W. Burdick, and Richard M. Murray. 2012 International Conference on Robotics and Automation (ICRA)

• Robust Control of Uncertain Markov Decision Processes with Temporal Logic Specifications, Eric M. Wolff, Ufuk Topcu and Richard M. Murray. 2012 Conference on Decision and Control (CDC)

• On Synthesizing Robust Discrete Controllers under Modeling Uncertainty, Ufuk Topcu, Necmiye Ozay, Jun Liu, and Richard M. Murray. 2012 International Conf on Hybrid Systems: Computation and Control (HSCC)

• Synthesis of Switching Protocols from Temporal Logic Specifications, Jun Liu, Necmiye Ozay, Ufuk Topcu and Richard M. Murray. 2012 American Control Conference.

• Temporal Logic Control of Switched Affine Systems with an Application in Fuel Balancing, Petter Nilsson, Necmiye Özay, Ufuk Topcu and Richard M. Murray. 2012 American Control Conference (ACC).

• Backtracking temporal logic synthesis for uncertain environments, Scott Livingston, Richard M. Murray and Joel W. Burdick. 2012 International Conference on Robotics and Automation (ICRA).

Software

• TuLiP - Temporal Logic Planning Toolbox