- Scott A. Smolka (joint with Concur and QEST)
- V-Formation as Optimal Control
In this talk, I will present a new formulation of the V-formation problem for migrating birds in terms of model predictive control (MPC). In this approach, to drive a flock towards a desired formation, an optimal velocity adjustment (acceleration) is performed at each time-step on each bird’s current velocity using a model-based prediction window of T time-steps. I will present both centralized and distributed versions of this approach. The optimization criteria used is based on fitness metrics of candidate accelerations that V-formations are known to exhibit. These include velocity matching, clear view, and upwash benefit. This MPC-based approach is validated by showing that for a significant majority of simulation runs, the flock succeeds in forming the desired formation. These results help to better understand the emergent behavior of formation flight, and provide a control strategy for flocks of autonomous aerial vehicles. This talk represents joint work with Radu Grosu, Ashish Tiwari, and Junxing Yang.- Short bio: Scott Smolka is a professor in the Department of Computer Science at the State University of New York, Stony Brook. He is also president and co-founder of Reactive Systems, Inc. He has been on the faculty at SUNY at Stony Brook since 1982. Smolka holds an A.B. and A.M. in Mathematics from Boston University and a Ph.D. in Computer Science from Brown University. His work focuses on analysis techniques for reactive systems and he also has extensive experience in building verification tools, including Winston and the Concurrency Factory.
- Ufuk Topcu (joint with QEST)
- Adaptable Yet Provably Correct Autonomous Systems
Acceptance of autonomous systems at scales at which they can make societal and economical impact hinges on factors including how capable they are in delivering complicated missions in uncertain and dynamic environments and how much we can trust that they will operate safely and correctly. In this talk, we present a series of algorithms recently developed to address this need. In particular, these algorithms are for the synthesis of control protocols that enable agents to learn from interactions with their environment and/or humans while verifiably satisfying given formal safety and other high-level mission specifications in nondeterministic and stochastic environments.
We take two complementing approaches. The first approach merges data efficiency notions from learning (e.g., so-called probably approximate correctness) with probabilistic temporal logic specifications. The second one leverages permissiveness in temporal-logic-constrained strategy synthesis with reinforcement learning.
- Short bio: Ufuk Topcu joined the Department of Aerospace Engineering and Engineering Mechanics at The University of Texas at Austin as an assistant professor in Fall 2015. He received his Ph.D. degree from the University of California at Berkeley in 2008. Before joining The University of Texas, he was with the Department of Electrical and Systems Engineering at the University of Pennsylvania. He was a postdoctoral scholar at California Institute of Technology until 2012.
The central question in his research is how we can build provably correct, protocol-based control systems. He currently focuses on technical challenges due to (i) heterogeneity in models, specifications, and uncertainties; (ii) interfacing with human operators and learning modules; (iii) scalability of the tools; and (iv) abundance or lack of information during execution.
- Oleg Sokolsky
- Platform-Specific Code Generation from Platform-Independent Timed Models
Model-based implementation has emerged as an effective approach to systematically develop embedded software for real-time systems. Functional and timing behavior of the software is modeled using modeling languages with formal semantics. We then use formal verification techniques to demonstrate conformance of the model to the timing requirements for the system. Code generation then automatically generates source code from the verified model. The goal of this process is to guarantee that the final implemented system, running on an embedded platform, also conforms to the timing requirements. Several code generation frameworks have emerged, but they rely on restrictive assumptions regarding code execution by the underlying platform or require manual effort to integrate platform-independent code onto the platform. Both may undermine formal guarantees obtained in the course of model-based development.
In this talk, we consider the well-known four-variable model of system execution introduced by Parnas. The four-variable model makes a clear distinction between the external boundary of the system and internal boundary of the software. Timing requirements are typically verified on the external boundary, while generated code operates at the internal boundary of the system. This distinction can lead to a semantic gap between the verified model and generade code. We explore several complementary approaches to account for the distinction between the two boundaries. One approach composes the platform-independent model with a platform execution model for verification, but applies code generation to the platform-independent model only. Another approach uses integer linear programming to calculate a transformation of timing constants in the platform-independent model that keeps effects of platform delays on the occurrence of observable events in the generated code as small as possible.
This talk presents results of a collaboration with my colleagues BaekGyu Kim (currently at Toyota ITC), Insup Lee, Linh T.X. Phan, and Lu Feng.
Short bio: Oleg Sokolsky is a Research Associate Professor with the Department of Computer and Information Science of University of Pennsylvania. He holds a B.S. and M.S. in Computer Science from St. Petersburg State Technical University in Russia, and a Ph.D. degree in Computer Science from State University of New York at Stony Brook. His main research interest is the application of formal methods to design and verification of distributed real-time systems. Other interests, all related to the main one, include on-line monitoring of distributed systems and formal foundations for it, hybrid systems, automated extraction of specifications from source code, and formal methods in software engineering in general and in embedded software in particular.