This project concerns the design of multi-agent multi-modal control systems, their distributed real-time software implementation, and their formal analysis. As a common foundation we build on the use of heterogeneous hybrid modeling techniques.
Control theory has traditionally done a good job of building robust, centralized control laws for systems that are well described by rather detailed differential equation or difference equation models. The drawback to the traditional approach is that it is not easily applicable to scenarios involving multi-modal, multi-objective control, or multiple distributed computers controlling parts of a complex control system.
We will develop and advance to the level of practical application the fundamentally new control paradigm of hybrid systems, in parallel and through feedback with experimentation on the Boeing developed Open Control Platform (OCP), and a UAV rotorcraft testbed at UC Berkeley. Specifically, we will develop techniques for modeling, deriving, and validating multi-agent, multi-modal control laws and their computational realization, as well as techniques for implementing and evaluating software that realizes distributed, hierarchical control designs. Special emphasis will be put on the integration of the hybrid control technology with the OCP.
Our activities are organized into three thrusts.
Thrust 1: Multi-agent Multi-modal Control Design. The research in this part of the project focuses on hybrid systems theory to enable multi-agent multi-modal control. Hybrid systems theory integrates discrete and continuous dynamics to model the interaction of computation and real time. Our approach is to use hybrid systems models for the design, analysis, and synthesis of distributed, hierarchical control systems that deliver high levels of mission reliability in dynamic and rapidly evolving environments. Special emphasis is put on probabilistic methods which account for uncertainties in the environment and the model.
Thrust 2: Distributed Real-Time Software Components. The focus of this part of the project is to adapt sophisticated software techniques to the problem domain of real-time control systems. The problem domain mandates a priority on real-time guarantees and verifiable designs. Our approach is based on formalizing the models of computation that govern the interaction between components (both hardware and software components), and building software that realizes these models of computation. Control systems integrate a variety of hardware, including networked sensors and actuators, with a variety of service demands, ranging from hard-real-time signal processing to interaction with human operators. Hence, our approach emphasizes the composition of heterogeneous models of computation.
Thrust 3: Formal Real-Time Software Components. In this part of the project we focus on bridging the gap between the mathematical design of control algorithms and their software implementation. We are developing modular, hierarchical formal models for hybrid controller designs, and a methodology of formal refinement between such designs and time-triggered implementations. The objective of the methodology is to ensure that the safety and performance properties of the mathematical control design are preserved by the software implementation. The refinement proceeds in several steps, first from hybrid automata models to platform-independent time-triggered programs, and then to specific RTOS and communication architectures. The refinement proceeds one component at a time, using assume-guarantee methods for constraining the context of individual components.
Our effort is organized in three thrusts: controller design and analysis; embedded software design; and formal modeling and verification.
Thrust 1: Multi-agent Multi-modal Control Design. We did extensive research on multi-modal control derivation, in particular, mode switching synthesis for specifications which are based on mission completion properties. The objective is to develop a general framework for the study of control mode switching, and algorithms for the derivation of sequences of control modes which will satisfy reachability tasks. We also developed algorithms for computing the maximal controlled invariant set and least restrictive controller for discrete time systems. We implemented the algorithm for least restrictive controller synthesis based on robust semidefinite programming. We introduced a new framework for the geometric study of hybrid systems. Its usefulness was demonstrated in the analysis of Zeno phenomena, the stability of hybrid equilibria, and the controllability of hybrid systems.
Thrust 2: Distributed Real-Time Software Components. We have started to apply modern software concepts, including sophisticated approaches to concurrency management, discovery, middleware, type systems, and higher-order functions to the domain of real-time control systems. We have been using a pre-existing Java-based software framework called Ptolemy II as an experimental platform, and we have been working with the Berkeley Aerobots project to put our software concepts on autonomous model helicopters. We did extensive experimentation with various embedded devices with sensors and actuators, integrating them in various ways into our software infrastructure. The objective is to develop techniques for portable, component-based design of embedded software. We plan to use the same techniques for programming a variety of platforms, including the Open Control Platform.
Thrust 3: Formal Real-Time Software Components. We extended the theory and implementation of the model checker HyTech to cope with rectangular and nonlinear hybrid systems. We also developed a systematic classification of which requirements of hybrid systems can be model checked. We extended the nondeterministic framework of hybrid systems to a probabilistic one. This provides an analytical framework for the verification of fault detection and handling. We also extended the standard model of hybrid systems to permit hierarchical nesting of both parallel composition (component and thread composition) and sequential composition (mode composition). This will permit us to develop a formal methodology for faithfully implementing distributed, hierarchical control models in real-time software.
We will continue to develop the scientific basis of a hybrid systems framework for designing, analyzing, and simulating multi-agent, multi-modal control models (both on-line and off-line) using tools from control theory (differential geometric, optimal control) and computer science (concurrency models, model checking). The methodology will be developed to be consistent with the Open Control Platform. Some of the key issues to be addressed are listed below.
Hybrid systems theory and simulation. We will continue to build the mathematical and control theoretic foundation of the hybrid systems based approach. Our goal here is to derive and estimate the performance and validate the safety of hybrid control designs (for flight applications and other safety critical operations) under consideration of implementation constraints such as hardware architecture, sensor fusion, resource sharing, real time, etc. Simulation is used as a precursor to the implementation of the control laws on our UAV test bed and on the OCP. We will use a heterogeneous model simulator and a real-time validation environment for high-level control designs, both developed here at Berkeley and by the OCP contractor, as well as commercially available toolkits from Matlab, Matrix-X, RTI, Xilink, etc. This will be done in a way consistent with and in support of the OCP, in order to bridge the gap between functional control design and software implementation.
Heterogeneous model composition. On the software side, we will continue to focus on the composition of heterogeneous models of computation. For example, publish-and-subscribe interactions between components (with priorities) are suitable for managing irregular events and alarms, but not so well suited for regular, high-sample-rate signal processing nor for continuous dynamics. Time-triggered formalisms are better suited for hard-real-time processing, but not as well suited for irregular interactions. Our approach, therefore, is to study the composition of these models and to build software that enables systematic composition. Another example of such heterogeneous compositions uses state machine models to govern modes of operation of systems whose behavior is better represented in some other way, such as by continuous-time models, to get hybrid systems.
Formal verification of real-time software. We will continue to develop a formal methodology for faithfully implementing distributed, hierarchical control models in real-time software. For this purpose, we are developing two languages: Masaccio, a hybrid automaton language enriched with arbitrarily nested parallel and sequential composition, for modeling, analyzing, and deriving hierarchical multi-modal control designs; and Giotto, a time-triggered programming language for implementing periodic tasks and mode switching. We are working on model checking Masaccio models, assume-guarantee refining Masaccio models into Giotto programs, and compiling Giotto programs on various real-time platforms, including the Open Control Platform.
Probabilistic hybrid systems. Among the most important issues in hybrid control are the use of probabilistic estimates and models in design, safety, and performance analysis, as well as the use of active models for dynamic fault handling during missions. The former avoids overdesign while quantifying the risk of failures in realistic environments; the latter takes on-line actions if such failures nonetheless occur. The foundation of these topics is, at this point, largely speculative, and fundamental, exploratory research is needed both in the mathematics of hybrid control theory and in experimentation with real-world platforms such as the UAV testbed in order to drive and validate the relevance of theoretical models.
UC Berkeley has a tradition of making software freely available in order to disseminate methodology. Our standard copyright agreement is very liberal, permitting commercialization of the software and derivative works. This mechanism has proved extremely effective at technology transfer. Within the university, distributing software is viewed as a form of publication, even within the tenure and promotion process.
Although technically we do not provide support for such software, we have in the past been able to provide some support through newsgroups, e-mail mailing lists, and the World Wide Web. We plan to continue this informal support network for software developed under this project, and to extend it with the use of applets for dissemination and education of potential users.
Previous software releases from the Ptolemy group have received quite a bit of attention in industry. They are openly acknowledged as the progenitors of the latest mixed signal design environment from Hewlett Packard's EESoft division (now part of Agilent), called ADS, or advanced development system. Ptolemy software has also strongly influenced versions of the SPW and CONVERGENCE design environments from the industry leader in signal processing design software, Cadence Design Systems. More recent software from Cadence has been influenced indirectly through the Polis project, also at Berkeley, which built on top of Ptolemy group software a hardware/software codesign environment. Our work has also had considerable influence on the COSSAP system produced by Synopsys and its descendants. BNeD [http://www.BNeD.com] has commercialized a modeling environment for the design of optical fiber systems based on Ptolemy software. Structured Software Systems has constructed a financial modeling system and on-line trading system based on Ptolemy software. Technologies Lyre has interfaced Ptolemy software to hardware subsystems designed for rapid prototyping of signal processing systems. A number of companies have used and extended software from the Ptolemy group without turning it into commercial products. These include Lockheed Martin, Hughes Aircraft, Motorola, Berkeley Design Technology, DQDT (Dimensions in Quick Design Turnaround), White Eagle Systems Technology, Inc., LG Electronics, Data Flux Systems, Mitsubishi, and Thomson CSF. Ptolemy software has also been used at several universities, including the University of Pittsburgh, the University of Washington, and several in Europe.
The model checkers HyTech and Mocha have more than 200 registered users worldwide, primarily at industrial research labs and academic institutions. The HyTech software is used by both computer scientists and control theorists. It has been acknowledged as analysis tool in numerous scientific publications, for example, in aerospace, automotive, manufacturing, and robotics applications
Karl Johansson, Tom Henzinger, and Luca de Alfaro taught a graduate course on Hybrid Systems at the University of California, Berkeley, in Spring 2000.