Design of Robotics and Embedded systems, Analysis, and Modeling Seminar (DREAMS)
The Design of Robotics and Embedded systems, Analysis, and Modeling Seminar (DREAMS) occurs weekly on Mondays from 4.10-5.00 p.m. in 250 Sutardja Dai Hall.
Similar to last year, DREAMS has joined forces with the Control Theory Seminar and the CITRIS People and Robots Seminar CPAR.
The Design of Robotics and Embedded systems, Analysis, and Modeling Seminar topics are announced to the DREAMS list, which includes the chessworkshop workgroup, which includes the chesslocal workgroup.
Information on the seminar series might be useful for potential speakers. If you have any questions about DREAMS, please contact Dorsa Sadigh. If you want to subscribe to our mailing list, please drop me a line.
Seminars from previous semesters can be found here.
Data-driven and model-based quantitative verification and correct-by-design synthesis of CPS
Aug 22, 2016, 4-5pm, 250 SDH, Alessandro Abate, University of Oxford.
I discuss a new and formal, measurement-driven and model-based automated verification and synthesis technique, to be applied on quantitative properties over systems with partly unknown dynamics. I focus on physical systems (with spatially continuous variables, possibly noisy), driven by external inputs and accessed under noisy measurements, and suggest that the approach can be as well generalised over CPS. I formulate this new setup as a data-driven Bayesian model inference problem, formally embedded within a quantitative, model-based verification procedure.
While emphasising the generality of the approach over a number of diverse model classes, this talk zooms in on systems represented via stochastic hybrid models (SHS), which are probabilistic models with heterogeneous dynamics (continuous/discrete, i.e. hybrid, as well as nonlinear) - as such, SHS are quite a natural framework for CPS. With focus on model-based verification procedures, I provide the characterisation of general temporal specifications based on Bellman’s dynamic programming. The computation of such properties and the synthesis of related control architectures optimising properties of interest, is attained via the development of abstraction techniques based on quantitative approximations. Theory is complemented by algorithms, all packaged in a software tool (FAUST^2) that is freely available to users.
Alessandro Abate is an Associate Professor in the Department of Computer Science at the University of Oxford, and a Fellow of the Alan Turing Institute in London (UK). He received a Laurea in Electrical Engineering in October 2002 from the University of Padova (IT), an MS in May 2004 and a PhD in December 2007, both in Electrical Engineering and Computer Sciences, at UC Berkeley (USA). He has been an International Fellow in the CS Lab at SRI International in Menlo Park (USA), and a PostDoctoral Researcher at Stanford University (USA), in the Department of Aeronautics and Astronautics. From June 2009 to mid 2013 he has been an Assistant Professor at the Delft Center for Systems and Control, TU Delft (NL).
His research interests are in the formal verification and control of complex (probabilistic and hybrid) models, in the integration of data-based learning aspects within these deductive techniques, and in the application of complex models over a number of domains, particularly in energy and in systems biology.
Building Trust in Decision Support Systems for Aerospace
Aug 29, 2016, 4-5pm, 250 SDH, Mykel Kochenderfer, Stanford University.
Starting in the 1970s, decades of effort went into building human-designed rules for providing automatic maneuver guidance to pilots to avoid mid-air collisions. The resulting system was later mandated worldwide on all large aircraft and significantly improved the safety of the airspace. Recent work has investigated the feasibility of using partially observable Markov decision processes (POMDPs) and advanced computational techniques to derive optimized decision logic that better handles various sources of uncertainty and balances competing system objectives. This approach has resulted in a system called Airborne Collision Avoidance System (ACAS) X that significantly reduces the risk of mid-air collision while also reducing the alert rate, and it is in the process of becoming the next international standard. Using ACAS X as a case study, this talk will discuss lessons learned about building trust in advanced decision support systems. This talk will also outline research challenges in facilitating greater levels of automation and integrating unmanned aircraft into the airspace.
Mykel Kochenderfer is Assistant Professor of Aeronautics and Astronautics at Stanford University. Prior to joining the faculty, he was at MIT Lincoln Laboratory where he worked on airspace modeling and aircraft collision avoidance, with his early work leading to the establishment of the ACAS X program. He received a Ph.D. from the University of Edinburgh and B.S. and M.S. degrees in computer science from Stanford University. Prof. Kochenderfer is the director of the Stanford Intelligent Systems Laboratory (SISL), conducting research on advanced algorithms and analytical methods for the design of robust decision making systems. He is the author of "Decision Making under Uncertainty: Theory and Application" from MIT Press. He is a third generation pilot.
Multicopter dynamics and control: surviving the complete loss of multiple actuators and quickly generating trajectories
Sep 12, 2016, 4-5pm, 250 SDH, Mark Mueller, University of California, Berkeley.
Multicopters are increasingly becoming part of our everyday lives, with current and future applications including delivery services, entertainment, and aerial sensing. These systems are expected to be safe and to have a high degree of autonomy. This talk will look at the dynamics of a multicopter, and then discuss multicopter failsafe strategies and fast trajectory generation.
The first part of the talk presents an actuator redundancy scheme for multicopters, allowing e.g. a quadcopter to maintain controlled flight despite the complete failure of half its actuators. This redundancy is a crucial part of the safety concept of a NYC Broadway musical drone performance, where eight quadcopters perform eight shows per week in front of an audience of 2'000 people, without any protective nets. The related 'monospinner' will also be presented: with only one moving part, it is potentially the world's mechanically simplest, controllable flying vehicle.
Mark W. Mueller completed his PhD studies, advised by Prof. Raffaello D'Andrea, at the Institute for Dynamic Systems and Control at the ETH Zurich at the end of 2015. He received a bachelors degree from the University of Pretoria, and a masters from the ETH Zurich in 2011, both in Mechanical Engineering. After working a brief period at a startup company, he joined the Mechanical Engineering Department at Berkeley in August of this year.
Opportunities and Challenges in Control Systems arising from Ubiquitous Communication and Computation
Sep 19, 2016, 4-5pm, 250 SDH, Joao Hespanha, University of California, Santa Barbara.
Advances in VLSI (Very Large Scale Integration) design and fabrication have resulted in the availability of low-cost, low-power, small-sized devices that have significant computational power and are able to communicate wirelessly. In addition, advances in MEMS (Micro Electric Mechanical Systems) technology have resulted in wide availability of solid-state sensors and actuators. The net result is ubiquitous sensing, communication, and computation that can be incorporated into small low-power devices.
In this talk, I will discuss how the above-mentioned technological advances present important opportunities and interesting challenges for control system designers. To this effect, I will discuss how the introduction of digital communication in control loops gives rise to a need for new tools for the design and analysis of feedback control systems. I will also describe recent work demonstrating that feedback control based on on-line optimization is a viable approach to solve a wide range of control problem.
João P. Hespanha received his Ph.D. degree in electrical engineering and applied science from Yale University, New Haven, Connecticut in 1998. From 1999 to 2001, he was Assistant Professor at the University of Southern California, Los Angeles. He moved to the University of California, Santa Barbara in 2002, where he currently holds a Professor position with the Department of Electrical and Computer Engineering. Prof. Hespanha is the Chair of the Department of Electrical and Computer Engineering and a member of the Executive Committee for the Institute for Collaborative Biotechnologies (ICB). Dr. Hespanha is a Fellow of the IEEE and was an IEEE distinguished lecturer from 2007 to 2013. His current research interests include hybrid and switched systems; multi-agent control systems; distributed control over communication networks (also known as networked control systems); the use of vision in feedback control; stochastic modeling in biology; and network security.
The Quest for Average Response Time
Sep 22, 2016, 4-5pm, 250 SDH, Tom Henzinger, IST Austria.
Responsiveness -the requirement that every request to a system be eventually handled- is one of the fundamental liveness properties of a reactive system and lies at the heart of all methods for specifying and verifying liveness. Average response time is a quantitative measure for the responsiveness requirement used commonly in performance evaluation. The static computation of average response time has proved remarkably elusive even for finite-state models of reactive systems. We present, for the first time, a robust formalism that allows the specification and computation of quantitative temporal properties including average response time. The formalism is based on nested weighted automata, which can serve as monitors for measuring the response time of a reactive system. We show that the average response time can be computed in exponential space for nondeterministic finite-state models of reactive systems and in polynomial time for probabilistic finite-state models. This work is joint with Krishnendu Chatterjee and Jan Otop.
Thomas A. Henzinger is president of IST Austria (Institute of Science and Technology Austria). He holds a Dipl.-Ing. degree in Computer Science from Kepler University in Linz, Austria, an M.S. degree in Computer and Information Sciences from the University of Delaware, a Ph.D. degree in Computer Science from Stanford University (1991), and a Dr.h.c. from Fourier University in Grenoble, France (2012) and from Masaryk University in Brno, Czech Republic (2015). He was Assistant Professor of Computer Science at Cornell University (1992-95), Assistant Professor (1996-97), Associate Professor (1997-98), and Professor (1998-2004) of Electrical Engineering and Computer Sciences at the University of California, Berkeley. He was also Director at the Max-Planck Institute for Computer Science in Saarbruecken, Germany (1999) and Professor of Computer and Communication Sciences at EPFL in Lausanne, Switzerland (2004-09). His research focuses on modern systems theory, especially models, algorithms, and tools for the design and verification of reliable software, hardware, and embedded systems. His HyTech tool was the first model checker for mixed discrete-continuous systems. He is an ISI highly cited researcher, a member of Academia Europaea, a member of the German Academy of Sciences (Leopoldina), a member of the Austrian Academy of Sciences, a Fellow of the AAAS, a Fellow of the ACM, and a Fellow of the IEEE. He has received the Milner Award of the Royal Society, the Wittgenstein Award of the Austrian Science Fund, and an ERC Advanced Investigator Grant.
Collaborative control for human-in-the-loop systems: Optimal interface design and reachability-based collaborative navigation
Sep 26, 2016, 4-5pm, 250 SDH, Meeko Oishi, University of New Mexico.
Methods for the analysis and design of human-in-the-loop systems must account for interactions between the automation, the human, and the environment. We consider two problems: 1) user-interface design, and 2) collaborative navigation in dynamic, uncertain environments. The user-interface, which provides information to the user about the underlying automation, and allows the user to issue input commands to the system, is key for enabling situational awareness and trust of the automation, yet is often designed in an ad-hoc fashion. We use sensor placement techniques to determine the optimal elements for display in the user-interface, and exploit submodularity properties to facilitate solution of the resulting combinatorial optimization problem. We additionally consider the problem of collaborative navigation in dynamic, uncertain environments. While assurances of safety are computationally intractable, solutions that exploit the forward reachable set are real-time compatible. We describe a method to compute the forward stochastic reachable set and its probability measure efficiently, that enables robust performance in difficult planning problems.
Meeko Oishi is an Associate Professor of Electrical and Computer Engineering at the University of New Mexico. She received the Ph.D. (2004) and M.S. (2000) in Mechanical Engineering from Stanford University, and a B.S.E. in Mechanical Engineering from Princeton University (1998). Her research interests include nonlinear dynamical systems, hybrid control theory, control of human-in-the-loop systems, reachability analysis, and modeling of motor performance and control in Parkinson’s disease. She previously held a faculty position at the University of British Columbia at Vancouver. She is the recipient of the NSF CAREER Award, the UNM Regents’ Lecturer Award, the UNM Teaching Fellowship, the Peter Wall Institute Early Career Scholar Award, the Truman Postdoctoral Fellowship in National Security Science and Engineering, and the George Bienkowski Memorial Prize, Princeton University. She was a Summer Faculty Fellow at AFRL Space Vehicles Directorate 2013–2015.
Adaptive Horizon Model Predictive Control
Sep 29, 2016, 4-5pm, 250 SDH, Arthur Krener, University of California, Davis.
Adaptive Horizon Model Predictive Control (AHMPC) is a scheme for varying the horizon length of Model Predictive Control (MPC) as needed. Its goal is to achieve stabilization with horizons as small as possible so that it can be used on faster or more complicated dynamic process. Beside the standard requirements of MPC including a terminal cost that is a control Lyapunov function, AHMPC requires a terminal feedback that turns the control Lyapunov function into a standard Lyapunov function in some domain around the operating point. But this domain need not be known explicitly. Just as MPC does not compute off-line the optimal cost and the optimal feedback over a large domain instead it computes these quantities on-line when and where they are needed, AHMPC does not compute off-line the domain on which the terminal cost is a control Lyapunov function instead it computes on-line when a state is in this domain.
AHMPC verifies in real time that stabilization is being achieved. This is particularly important when dealing with nonlinear systems because the nonlinear programs that MPC passes to the nonlinear program solver are typically nonconvex. Therefore the solver may return local rather than global solutions and these may fail to be stabilizing. AHMPC detects when the solutions are not stabilizing. If so there is a need to pass different initial guesses to the solver to find global solutions or at least local solutions that are stabilizing.
Arthur Krener is a mathematician whose research interests are in developing methods for the control and estimation of nonlinear dynamical systems and stochastic processes. In 1971 he received the PhD in Mathematics from the University of California, Berkeley and joined the faculty of the University of California, Davis. He retired from UCD in 2006 as a Distinguished Professor of Mathematics and he currently is a Distinguished Visiting Professor at the Naval Postgraduate School. He has also held visiting positions at Harvard University, Imperial College, NASA Ames Research Center, the University of California, Berkeley, the University of Paris, the University of Maryland, the University of Padua and North Carolina State University. He is a member of the American Mathematical Association, a Fellow of the Society for Industrial and Applied Mathematics and a Life Fellow of the Institute of Electrical and Electronics Engineers. Krener has held a variety of administrative posts, including Chair of the Department of Mathematics, UC Davis, member of the Committee on Academic Personnel, UC Davis and Chair of the SIAM Activity Group on Control and Systems Theory.
Interaction force reconstruction for humanoid robots
Oct 04, 2016, 3-4pm, 730 SDH, Marilena Vendittelli, Sapienza University of Rome.
Humanoids are, by definition, robotic systems for which the control of interaction forces with the environment is elemental for the accomplishment of any loco-manipulation task. Any feedback controller of the interaction forces would invariably require some form of measure or estimation of the forces actually exchanged between the robot and the environment. In this talk we will discuss the peculiarity of the interaction force estimation problem in the case of humanoids and we will propose methods that do not make use of force sensors and do not limit the interaction to specific points of the humanoid body. The illustration of the proposed approach is completed by experimental validation on the robot NAO. The talk is based on the work in  and  where two different approaches to interaction force estimation are considered. In , an accurate reconstruction of contact forces and identification of the contact point is obtained using joint position and motor current measurements under the assumption of static equilibrium. The method is designed for manipulation task or multi-contact locomotion, where accurate estimation of the contact forces is important for task accomplishment, including equilibrium preservation. Interaction forces are, instead, perceived in  through a measure of the equilibrium perturbation. The reconstructed force is used as a guiding force in collaborative tasks and the humanoid locomotion results from the proposed equilibrium preservation strategy.
BIBLIO  T. Mattioli, M. Vendittelli, "Interaction force reconstruction for humanoid robots," IEEE Robotics and Automation Letters, 2016. DOI: 10.1109/LRA.2016.2601345
 M. Bellaccini, A. Paolillo, L. Lanari, M. Vendittelli, "Manual guidance of humanoid robots without force sensors: preliminary experiments with NAO," 2014 IEEE International Conference on Robotics and Automation, Hong Kong, China, May 2014. DOI: 10.1109/ICRA.2014.6907003
Marilena Vendittelli is Assistant Professor at Sapienza University of Rome, Department of Computer, Control and Management Engineering (DIAG), since 2001 and a member of the Robotics Laboratory at DIAG. She worked at LAAS-CNRS in Toulouse, France, first as a visiting scholar in 1995-96 and then as a post-doc in 1997-98, funded by a Marie Curie Research Training Grant. The research activity was focused on planning and control of general (i.e., not transformable in a canonical form) nonholonomic systems. She received the PhD degree in Systems Engineering from Sapienza University of Rome in 1997. In 2012 and 2005 she has been Visiting Scholar respectively at the Courant Institute, New York University, and at the Robotics Institute, Carnegie Mellon University.
Her research interests are in robot motion planning and control, with emphasis on non-holonomic and redundant systems of which wheeled mobile robots and humanoids are respectively the most notable examples. In particular, over the years her research activity has dealt with visual control, localization, motion planning, physical interaction for humanoids; modeling and control of UAVs; sensor-based exploration of unknown environments with teams of mobile robots; task-constrained motion planning for kinematically redundant systems; probabilistic methods for robot motion planning and exploration; planning and control of wheeled mobile robots; steering and stabilization of general nonholonomic systems; nilpotent approximations of systems with singularities.
On these research themes she has published more than 60 papers in international conferences and journals. The total number of citations received is 2142 according to Google Scholar.
From January 2010 to December 2013 she has served as Associate Editor for the IEEE Transactions on Robotics. From 2009 to 2012 she has been Associate Editor in the ICRA Conference Editorial Board and from 2008 to 2011 for the IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS). She has contributed to the organization of several international scientific events among which ICRA 2007 as Registration Chair.
She participates to several EC funded projects, among which SAPHARI (FP7), COMANOID (H2020), SIMPLEXITY (H2020).
Proving that Programs do not Discriminate
Oct 10, 2016, 4-5pm, 250 SDH, Aws Albarghouthi, University of Wisconsin-Madison.
Programs have become powerful arbitrators of a range of significant decisions with far-reaching societal impact -- hiring, welfare allocation, prison sentencing, policing, amongst an ever-growing list. In such scenarios, the program is carrying out a sensitive task, and could potentially be illegally discriminating —- advertently or inadvertently —- against a protected group, e.g., African Americans in the United States.
With the range and sensitivity of algorithmic decisions expanding by the day, the question of whether an algorithm is fair (unbiased) has captured the attention of a broad spectrum of experts, from government regulators and law scholars to computer science theorists. Ultimately, algorithmic fairness is a question about programs and their properties: Does a program discriminate against a subset of the population? In this talk, I will view algorithmic fairness through the lens of program verification. Specifically, I will begin by formalizing the notion of fairness as a probabilistic property of programs. To enable automated verification of fairness, I will show how to reduce the probabilistic verification question to that of volume computation over first-order formulas, and describe a new symbolic volume computation algorithm. Finally, I will present results of applying FairSquare -- the first fairness verification tool -- to a variety of decision-making programs.
Aws Albarghouthi is an Assistant Professor of Computer Science at the University of Wisconsin-Madison. He works on software verification, analysis, and synthesis.
Bounded optimality and human cognition
Oct 17, 2016, 4-5pm, 250 SDH, Tom Griffiths, University of California, Berkeley.
Researchers seeking to include models of human cognition in systems that involve interaction between machines and people face an unsatisfying choice: modeling human behavior as completely rational (which is wrong), or trying to formalize the many heuristics identified by psychologists (which can be hard to generalize). I will talk about a different approach to solving this problem that combines the strength of rational models with the ability to capture the nuances of human behavior. This framework, which we call “resource rationality”, is based on the idea of bounded optimality developed in the AI literature: thinking about rationality not in terms of ideal performance obtainable with infinite computational resources, but in terms of the solution that makes best use of our limited computational resources. I will show that this approach can account for behavior related to classic decision-making heuristics, which has traditionally been taken as evidence against human rationality, and discuss some of the implications of this approach in settings such as physical reasoning and reinforcement learning.
Tom Griffiths is a Professor of Psychology and Cognitive Science at University of California, Berkeley, where he is also the Director of the Institute of Cognitive and Brain Sciences. His research explores connections between human and machine learning, using ideas from statistics and artificial intelligence to try to understand how people solve the challenging computational problems they encounter in everyday life.
Sampling-Based Motion Planning: From Intelligent CAD to Crowd Simulation to Protein Folding
Oct 24, 2016, 4-5pm, 250 SDH, Nancy Amato, Texas A&M University.
Motion planning has application in many domains such as robotics, animation, virtual prototyping and training, and even protein folding and drug design. Surprisingly, sampling-based planning methods have proven effective on problems from all these domains. In this talk, we describe sampling-based planning and give an overview of some variants developed in our group. We describe in more detail our work related to virtual prototyping, crowd simulation, and protein folding. For virtual prototyping, we show that in some cases a hybrid system incorporating both an automatic planner and haptic user input leads to superior results. For crowd simulation, we describe techniques for evacuation planning and for evaluating architectural designs. Finally, we describe our application of sampling-based motion planners to simulate molecular motions, such as protein and RNA folding.
Nancy M. Amato is Regents Professor and Unocal Professor of Computer Science and Engineering at Texas A&M University where she co-directs the Parasol Lab. Her main areas of research focus are motion planning and robotics, computational biology and geometry, and parallel and distributed computing. Amato received undergraduate degrees in Mathematical Sciences and Economics from Stanford University, and M.S. and Ph.D. degrees in Computer Science from UC Berkeley and the University of Illinois, respectively. She was program chair for the 2015 IEEE Intern. Conference on Robotics and Automation (ICRA) and for Robotics: Science and Systems (RSS) in 2016. She is an elected member of the CRA Board of Directors (2014-2017), is co-Chair of CRA-W (2014-2017), and was co-chair of the NCWIT Academic Alliance (2009-2011). She received the 2014 CRA Haberman Award, the inaugural NCWIT Harrold/Notkin Research and Graduate Mentoring Award in 2014, the 2013 IEEE HP/Harriet Rigas Award, and a Texas A&M AFS university-level teaching award in 2011. She received an NSF CAREER Award and is a AAAS Fellow, an ACM Fellow and an IEEE Fellow.
Understanding Others: Robot Learning in Interactions
Oct 26, 2016, 2-3pm, 250 SDH, Subramanian Ramamoorthy, University of Edinburgh.
We are motivated by the problem of building autonomous robots that are able to work collaboratively with other agents, such as human co-workers. One key attribute of such an autonomous system is the ability to make predictions about the actions and intentions of other agents in a dynamic environment - both to interpret the activity context as it is being played out and to adapt actions in response to that contextual information.
I will present recent results addressing questions of how to efficiently represent the hierarchical nature of activities, how to rapidly make inferences about latent factors, such as hidden goals and intent, and how to make optimal decisions in interactions without explicit prior coordination with unknown partners.
Firstly, I will describe a procedure for topological trajectory classification, using the concept of persistent homology, which enables unsupervised extraction of certain kinds of relational concepts in motion data. One use of this representation is in devising a multi-scale version of Bayesian recursive estimation, which is a step towards reliably grounding human instructions in the realized activity.
I will then describe work with a human-robot interface based on the joint use of mobile 3D eye tracking and vision for intention inference. We achieve this through the use of a probabilistic generative model of fixations conditioned on the task that the person is executing. Using preliminary experimental results, I will discuss how this approach is useful in the grounding of plan symbols to their detailed appearance in the environment.
Finally, I will present a model and algorithm for optimal decision making in interactions with unknown partners, based on the use of “policy types” within an incomplete information game, combining the benefits of Harsanyi’s notion of types and Bellman’s notion of optimality in sequential decisions. Using results from human-machine experiments, I will show how this algorithm achieves a better rate of coordination than alternate multi-agent learning algorithms.
Dr. Subramanian Ramamoorthy is a Reader (Associate Professor) in the School of Informatics, University of Edinburgh, where he has been on the faculty since 2007. He is a Coordinator of the EPSRC Robotarium Research Facility, and Executive Committee Member for the Edinburgh Centre for Robotics. He received his PhD in Electrical and Computer Engineering from The University of Texas at Austin in 2007. He is an elected Member of the Young Academy of Scotland at the Royal Society of Edinburgh, and has been a Visiting Professor at Stanford University and the University of Rome “La Sapienza”. His research focus is on robot learning and decision-making under uncertainty, addressed through a combination machine learning techniques with emphasis on issues of transfer, online and reinforcement learning as well as new representations and analysis techniques based on geometric/topological abstractions.
Using Model Checking Verifications at Runtime: The Proof is only Half the Battle
Nov 07, 2016, 4-5pm, 250 SDH, Ian Mitchell, University of British Columbia.
Recent advances in model checking algorithms for continuous state systems allow us to demonstrate the existence of safe control policies robust to model error for cyber-physical systems (CPS) of practical interest, such as shared control drones or wheelchairs, or automated delivery of anesthesia. However, these verification results are only relevant if we can implement those policies. In this talk I will discuss investigations into three challenges that arise at runtime: The sampled data nature of CPS feedback control, runtime state uncertainty, and human-in-the-loop shared control for older adults with cognitive impairment.
Ian M. Mitchell completed his doctoral work in engineering at Stanford University in 2002, spent a year as a postdoctoral researcher at the University of California at Berkeley, and is now an Associate Professor of Computer Science at the University of British Columbia. He is the author of the Toolbox of Level Set Methods, the first publicly available high accuracy implementation of solvers for dynamic implicit surfaces and the time dependent Hamilton-Jacobi equation that works in arbitrary dimension. His research interests include development of algorithms and software for nonlinear differential equations, formal verification, control and planning in cyber-physical and robotic systems, assistive technology and reproducible research.
Safety Verification of Deep Neural Networks
Nov 08, 2016, 4-5pm, 540 Cory, Marta Kwiatkowska, University of Oxford.
Deep neural networks have achieved impressive experimental results in image classification, but can surprisingly be unstable with respect to adversarial perturbations, that is, minimal changes to the input image that cause the network to misclassify it. With potential applications including perception modules and end-to-end controllers for self-driving cars, this raises concerns about their safety. We develop the first SMT-based automated verification framework for feed-forward multi-layer neural networks that works directly with the code of the network, exploring it layer by layer. We define safety for a region around a data point in a given layer by requiring that all points in the region are assigned the same class label. Working with a notion of a manipulation, a mapping between points that intuitively corresponds to a modification of an image, we employ discretisation to enable exhaustive search of the region. Our method can guarantee that adversarial examples are found for the given region and set of manipulations. If found, adversarial examples can be shown to human testers and/or used to fine-tune the network, and otherwise the network is declared safe for the given parameters. We implement the techniques using Z3 and evaluate them on state-of-the-art networks, including regularised and deep learning networks.
Marta Kwiatkowska is Professor of Computing Systems and Fellow of Trinity College, University of Oxford. She led the development of the PRISM model checker (www.prismmodelchecker.org), the leading software tool in the area, winner of the HVC Award 2016, and widely used for research and teaching. Applications of probabilistic model checking have spanned communication and security protocols, nanotechnology designs, power management, game theory, planning and systems biology, with genuine flaws found and corrected in real-world protocols. Kwiatkowska gave the Milner Lecture in 2012 in recognition of "excellent and original theoretical work which has a perceived significance for practical computing" and was awarded an honorary doctorate from KTH Royal Institute of Technology in Stockholm in 2014. Her research is supported by the ERC Advanced Grant VERIWARE "From software verification to everyware verification" and the EPSRC Programme Grant in Mobile Autonomy.
Sampling-Based Techniques for Planning and Control of Autonomous Spacecraft and Space Robots
Nov 14, 2016, 4-5pm, 250 SDH, Marco Pavone, Stanford University.
In this talk I will present a novel guidance framework for safely and efficiently maneuvering autonomous aerospace vehicles in dynamic and cluttered environments. I will first discuss some of the unique aspects of the "spacecraft motion planning problem." Then, I will present a sampling-based motion planning algorithm called the Fast Marching Tree algorithm (FMT*) and discuss its adaptation to spacecraft motion planning. In particular, this entails deterministic convergence guarantees, tractable inclusion of differential constraints, and planning under uncertainty via Monte Carlo sampling. I will conclude the talk with an overview of related projects in the field of autonomous aerospace systems currently under investigation in my research group.
Dr. Marco Pavone is an Assistant Professor of Aeronautics and Astronautics at Stanford University, where he is the Director of the Autonomous Systems Laboratory. Before joining Stanford, he was a Research Technologist within the Robotics Section at the NASA Jet Propulsion Laboratory. He received a Ph.D. degree in Aeronautics and Astronautics from the Massachusetts Institute of Technology in 2010. His main research interests are in the development of methodologies for the analysis, design, and control of autonomous systems, with an emphasis on autonomous aerospace vehicles and large-scale robotic networks. He is a recipient of an NSF CAREER Award, a NASA Early Career Faculty Award, a Hellman Faculty Scholar Award, and was named NASA NIAC Fellow in 2011. His work has been recognized with best paper nominations or awards at the Field and Service Robotics Conference (2015), at the Robotics: Science and Systems Conference (2014), and at NASA symposia (2015). He is currently serving as an Associate Editor for the IEEE Control Systems Magazine.
Dealing with Delays Or: How I Learned to Stop Worrying And Love Air Travel
Nov 21, 2016, 4-5pm, 250 SDH, Hamsa Balakrishnan, Massachusetts Institute of Technology.
Flight delays result in significant costs to passengers, airlines, and society as a whole. This fact motivates the development of models that can help characterize air traffic delays, and optimization algorithms that can help us reduce them.
In the first part of the talk, I will describe the development of a new class of networked system models of delay dynamics. These models reflect both the spatial properties (i.e., inter-airport interactions) and temporal patterns of delay propagation. They also provide features that can help assess various aspects of system resilience, and even predict the future evolution of delays.
In the second part of the talk, I will present an integer programming approach to mitigate flight delays by solving large-scale air traffic flow management problems in the presence of capacity uncertainties. The proposed stochastic optimization approach uses column generation to determine the optimal departure times, routes, and cancellation decisions for all flights in the air traffic network, allowing for recourse as the scenarios develop. Using nation-scale examples from the United States, I will demonstrate that the approach is scalable and fast enough for real-time implementation.
Hamsa Balakrishnan is an Associate Professor of Aeronautics and Astronautics at the Massachusetts Institute of Technology (MIT). Before joining MIT, she was at the NASA Ames Research Center. She received her M.S. and PhD degrees from Stanford University, and a B.Tech. from the Indian Institute of Technology Madras. Her research is in the design, analysis, and implementation of control and optimization algorithms for large-scale cyber-physical infrastructures, with an emphasis on air transportation systems. She is the co-founder and chief scientist of Resilient Ops, Inc.
Prof. Balakrishnan was a recipient of the NSF CAREER Award in 2008, the Kevin Corker Award for Best Paper of ATM-2011, the inaugural CNA Award for Operational Analysis in 2012, the AIAA Lawrence Sperry Award in 2012, and the American Automatic Control Council's Donald P. Eckman Award in 2014. She is an Associate Fellow of the American Institute of Aeronautics and Astronautics.
Optimizing cooperative driving for goods transportation
Nov 28, 2016, 4-5pm, 250 SDH, Karl Johansson, KTH Royal Institute of Technology.
The freight transportation sector is of great importance to our society and the demand for transportation is strongly linked to economic development. Despite the influence transportation has on energy consumption and the environment, road goods transportation today is mainly done by individual long-haulage trucks with no real-time coordination or global optimization. In this talk, we will discuss how this might change in the future through a more integrated transport system with an open market for transport assignments and the collaboration between individual trucks and fleets of trucks. Networked control challenges and solutions on various level of this transportation system will be presented. Extensive experiments done on European highways will illustrate the state-of-the-art. The presentation will be based on joint work over the last ten years with collaborators at KTH and at the truck manufacturer Scania.
Karl H. Johansson is Director of the Stockholm Strategic Research Area ICT The Next Generation and Professor at the School of Electrical Engineering, KTH Royal Institute of Technology. He received MSc and PhD degrees in Electrical Engineering from Lund University. He has held visiting positions at UC Berkeley, Caltech, NTU, HKUST Institute of Advanced Studies, and NTNU. His research interests are in networked control systems, cyber-physical systems, and applications in transportation, energy, and automation. He is a member of the IEEE Control Systems Society Board of Governors and the European Control Association Council. He has received several best paper awards and other distinctions, including a ten-year Wallenberg Scholar Grant, a Senior Researcher Position with the Swedish Research Council, and Future Research Leader Award from the Swedish Foundation for Strategic Research. He is Fellow of the IEEE and IEEE Control Systems Society Distinguished Lecturer.
Dec 05, 2016, 4-5pm, 250 SDH, Yon Visell, University of California, Santa Barbara.
I will describe recent work in my lab on haptics, soft electronics, and interactive systems. A longstanding goal in engineering has been to design technologies that are able to reflect the amazing perceptual and motor capabilities of biological systems for touch, including the human hand. This objective turns out to be difficult to achieve, due, not least, to our limited understanding of the mechanics underlying touch sensation, i.e. of what it is that is felt when we touch objects in the world. Some of the challenges involved can be traced to the complexity of the mechanical interactions, the high dimensionality of the signals, the multiple length scales, time scales, and physical regimes involved, and the sensitive dependence of what we feel on what we do - the way that touch-elicited mechanical signals depend on the way we move and contact objects. I will describe research that has aimed at addressing these challenges, and will explain how the results are informing the development of new technologies for wearable computing, virtual reality, and robotics.
Yon Visell is Assistant Professor of Electrical and Computer Engineering Department and Media Arts and Technology at the University of California, Santa Barbara. Assistant Professor (2013-2015) in the Electrical and Computer Engineering Department, Drexel University. Post-Doctoral Fellow (2011-2012) at the Institute of Intelligent Systems and Robotics, Université Pierre et Marie Curie Paris 06. PhD degree in Electrical and Computer Engineering at McGill University's Center for Intelligent Machines (2011). MA and BA degrees in Physics (Univ. Texas-Austin and Wesleyan Univ.). He spent more than 5 years in industrial R&D at high technology firms including Ableton, where he contributed to music software that is now used by artists worldwide, from Pete Townshend to Vijay Iyer and Nine Inch Nails. His work has received several awards, including a Google Faculty Research Award, and Best Paper awards at the 2010 and 2016 IEEE Haptics Symposium. His electronic music and artworks have exhibited at some of the most prominent cultural venues worldwide.
This group has the following subpages:
|You are not logged in|
|©2002-2016 U.C. Regents|