While algorithmic methods ("model checking") were originally developed for the analysis of finite-state systems, much recent interest has concerned the application of such methods to infinite-state systems. In general, two approaches may be followed. In the reductionist approach, we apply algorithms for exploring finite state spaces to a finite quotient of the infinite state system that is "equivalent" to the infinite state system (e.g., the region graph construction for timed automata). In the symbolic approach, we explore the infinite state space directly, by manipulating constraints representing (possibly infinite) state spaces (e.g., the representation of state sets using difference bounded matrices). Although optimal in theoretical complexity, reductionist approaches suffer from state explosion problems, and are outperformed in practice by symbolic algorithms. The main concern with algorithms manipulating infinite state spaces is termination. Termination guarantees can be provided by a reductionist argument: e.g., while there are infinitely many possible state sets, the difference bounded matrix approach can be shown to compute only sets corresponding to the finitely many bisimilarity classes. We have classified infinite state transition systems into four categories, according to which type of symbolic procedures terminates. Moreover, by essentially uniformly replacing the symbolic predecessor operators on transition structures by symbolic controllable predecessor operators on game structures, a similar classification may be obtained for control problems (modeled as multi-player games) as well.
While traditional symbolic model checking algorithms provide qualitative information about systems (i.e., set of states satisfying some logical requirements), we may also be interested in obtaining quantitative information in terms of probabilities of satisfying logical requirements. We can show that by uniformly replacing symbolic predecessors by quantitative predecessor operators, we can obtain quantitative information about systems using the same control structures.
We are also considering a complexity-theoretic study of model checking algorithms based on symbolic operators as primitives ("symbolic complexity"), in contrast to traditional complexity measures based on a Turing machine model. Such symbolic complexity measures are expected to reflect algorithmic properties of symbolic algorithms more closely.
- Multi-modal Control Derivation and Analysis
- Numerical Methods for Optimal Hybrid Control.
- Develop algorithms for the approximate solutions of Hamilton-Jacobi equations for the derivation of flight envelope protection and least restrictive controllers for nonlinear hybrid systems, using game theory. Computational considerations to be addressed in the controller design suite include wavefront propagation, storage of safe sets, shocks and viscosity solutions, as well as ellipsoidal approximation techniques. These ellipsoidal approximation techniques are to allow for numerical linear algebra computations, which are more efficient than Linear Matrix Inequality (LMI) techniques.
- Hierarchical Hybrid Control Design.
- Hybrid systems offer a qualitative new way of controlling design complexity through hierarchy, because continuous processes can be abstracted by discrete modes within a single hybrid model, thus giving rise to various levels of control. We will develop methods and tools for deriving control laws by taking advantage of such hybrid hierarchical descriptions of complex, decentralized control architectures.
- Mission Completion.
- Develop methods and tools for the derivation of controllers with specifications which are based on mission completion properties, rather than safety specifications such as flight envelope protection alone, for example, questions of how one can guarantee how much of a mission can be completed under various contingencies enroute. This would include provable guarantees of at least a gracefully degraded performance when the full mission cannot be completed. The methodology that will need to be used is a clever mixture of the games and optimal control with some reasoning about future performance (on-line approximate solutions of Bellmann dynamic programming equations).
- Develop algorithms for the approximate solutions of Hamilton-Jacobi equations for the derivation of flight envelope protection and least restrictive controllers for nonlinear hybrid systems, using game theory. Computational considerations to be addressed in the controller design suite include wavefront propagation, storage of safe sets, shocks and viscosity solutions, as well as ellipsoidal approximation techniques. These ellipsoidal approximation techniques are to allow for numerical linear algebra computations, which are more efficient than Linear Matrix Inequality (LMI) techniques.
- Numerical Methods for Optimal Hybrid Control.
- Probabilistic Hybrid Systems
- Probabilistic Control.
- When it is not possible to meet specifications deterministically, we will give probabilistic bounds on the performance of controllers, using viscosity solutions and games with randomized strategies for modeling probabilistic disturbances and faults. Specifically, we intend to generalize recent results on reachability of objectives in discrete probabilistic games to the the hybrid case.
- Probabilistic Analysis.
- For multi-modal and multi-vehicle systems, algorithms and tools will be developed to provide probabilistic estimates of safe and desired behavior (envelope protection, mission completion, etc.). We will also develop fault detection and handling tools, with guarantees of performance after the onset of a fault, as well as Markov decision process based tools for incompletely observed modules. We have had some initial success in applying this approach to conflict resolution for air traffic control.
- When it is not possible to meet specifications deterministically, we will give probabilistic bounds on the performance of controllers, using viscosity solutions and games with randomized strategies for modeling probabilistic disturbances and faults. Specifically, we intend to generalize recent results on reachability of objectives in discrete probabilistic games to the the hybrid case.
- Probabilistic Control.
-
We are interested in studying multi-agent hierarchical hybrid systems.
By a hybrid system we mean a dynamic system that has both
continuous and discrete counterparts, by hierarchical we mean that
the controller design is layered to (logarithmically) reduce complexity,
and finally by multi-agent we mean that the interacting network
of hybrid components itself evolves.
An example of multi-agent hierarchical hybrid systems is SmartAHS (Smart Automated Highway Systems). In particular, experience with SmartAHS has demonstrated that the multi and hierarchical aspects of dynamic systems incurs a fundamental difficulty; that of data flow. For example, supposing that we fix a state space model for the involved dynamic counterparts, each agent in the distributed mission assumes a state-of-the-world and acts accordingly. The information required for updating the state-of-the-world for each agent is, in this case, what we refer to as the data flow. We aim to formalize a (soft) framework for Unmanned Aerial Vehicles (UAVs) in which agents are equipped with semantic translators to update their state-of-the-world; i.e. agents need not do direct updates to their assumed state via sensor readings.
In the semantic setting afore mentioned we plan to address the problems
of robustness and hierarchical model decomposition (e.g. I/O, synchronous)
that admit robust controllers at each layer of the hierarchy. Our primary
tool for robustivity analysis will be reach set computations of the assumed
state space models; e.g. Kronos
(timed systems),
HyTech
(linear hybrid systems) and 
(dynamic networks of hybrid automata with general DAEs). For hierarchical
analysis we will experiment with both spatial and temporal abstractions;
e.g. Kronos
(Galois connections), HAM's
(SMDP's). Due to its powerful abstraction framework and symbolic
compuational power we will invest in the tool
for testing ideas and developing code.
is a meta-object protocol for describing and associating semantics to dynamic
networks of hybrid automata. The current implementation is based
on the Common Lisp CLOS/MOP.
The computational engine is powered by BLAS/LAPACK
integrated together with the CMUCL
type inference mechanism. In the current implementation, a class of hybrid
automata called STANDARD-HYBRID-CLASS is implemented with the cause-effect
synchronization and Runge-Kutta 4th order integration semantics.
Our immediate goal is to design a class of hybrid automata for
that allows convex (polyhedral, ellipsoidal) differential inclusions for
time-invariant linear differential equations. We will investigate
whether such convex abstractions are suitable for hierarchical decomposition.
See http://robotics.eecs.berkeley.edu/~simsek/sec/ for more information.
- manage the complexities of triplex redundancy? or of a distributed set of sensors, actuators, and processors?
- guarantee upper bounds on the latencies between the arrival of sensor inputs and the computation of actuator outputs?
- coordinate changes in control mode?
We are currently looking into the notion of design refinement: a methodology which, given a design for a multi-modal embedded control system, enables engineers to develop correct and robust implementations.
How, for example, should an engineer:
Moreover, once an engineer has developed an implementation, how does he or she prove that this implementation preserves the desirable properties of the original controllers? Such properties may include, for example, stability for a helicopter controller, or collision-avoidance for an air traffic control system.
We are particularly interested in time-triggered architectures (TTAs), for two reasons. First, TTAs allow the derivation of precise bounds upper bounds on communication latencies. Second, TTAs view mode changes as changes in schedule, enabling the use of real-time scheduling technology in the implementation of multi-modal controllers.
It is our hope to be able to compile designs for multi-modal embedded controllers (expressed as, say, hybrid automata) directly into time-triggered implementations, in such a way that the implementations can be proven to preserve the desirable properties of the designs.
Since embedded systems are increasingly common, and are often used in safety-critical environments, there is a need for automated tools for the analysis and verification of such systems. These tools should provide rigorous guarantees about correct performance. The technique of symbolic model checking has been successful in providing such guarantees. In particular, the tool HyTech has analyzed many systems of practical interest.
We are extending the capabilities of HyTech in a successor tool, HyperTech. HyperTech is capable of analyzing systems with general (nonlinear) dynamics. HyperTech uses interval numerical methods to overapproximate the reachable states of a hybrid system. In interval methods, the fundamental object of computation is not a real number, but rather an interval of the real line. Interval methods guarantee that the true result of a computation is always contained in the computed result. Because they avoid the problems of round-off errors and missed events, interval methods are suitable for the verification of hybrid systems.
In addition, we are interested in the compositional modeling of hybrid systems. Using compositional methods, one may prove the correctness of a system from the correctness of its subsystems. For purely discrete systems, compositional modeling has enabled the verification of designs too complex to be analyzed by other means. However, much remains to be understood about how to compositionally model and reason about hybrid systems.
- This project focuses particularly on software component architectures
for real-time embedded systems. The problem can be decomposed into
one of abstract syntax (what constraints are there on the logical
structure of an assemblage of components), concrete syntax (how
is an assemblage of components represented in a persistent format),
syntactic transformations (how does an assemblage change structure
over time), semantics (how do components interact), and a type
system (what sorts of data can components exchange). We are examining
CORBA (particularly the TAO realization), Jini, Soap, Java Beans,
and related component architectures.
-
UC Berkeley UAV reserach team, BEAR have been developing a somplete testbed
of multiple UAVs and UGVs, communicating via peer-to-peer wireless network
system. While UGV and other supporting computation and communication components
are mature technologies and available as off-the-shelf products,
UAV technology is relatively new and a lot of research efforts should be
made on helicopter model identification, linear/nonlinear control, flight
management and so on.
Each UAV consists of navigation sensors, onboard computer(s), communication systems and actuators. The vehicle management system (VMS) software for RUAV has been written in C running on real-time operating system, QNX. The software takes the responsibility to maintain navigation sensors incluing INS/GPS, download its flight status and process the uploaded request, and issues the control output calculated using control law. Since the software has jobs running at different but constant rates, the software is divided into three different concurrent processes and communicate with one another via interprocess communication protocols supported by QNX.
Up to now, a onboard flight control algorithm for attitude, velocity, position and heading control has been implemented based on a identified system linear model. This lowest-level regulation layer will be integrated with higher level trajectory generator and flight management layers. Due to the high complexity of the hierarchical control algorithm and many independent and "smart" components such as INS and GPS, operated by independent DSP chips, the onboard software calls for careful job description. This effort has been made in collaboration with Professor Edward Lee, John Koo, and Xiaojun Liu. Also, to manage the resources of the onboard computer and connected components more efficiently and in a more systematic way, the possibility to introduce a resource broker, such as CORBA, are also being reviewed.