16.1.   INTRODUCTION

Based on operational, financial, and environmental considerations, large-scale
systems ranging from automated highway systems [1], air traffic management
systems [2], unmanned aerial vehicle networks [3], communication networks
and power distribution networks have been advocated to have higher levels
of automation. Recent advances of embedded system technologies in sensing,
computation and communication have enabled the rapid realization of sophisticated,
high-performance embedded controllers. The control of largescale
systems is extremely challenging since by nature the systems are
distributed and highly dynamic, the environments in which the systems reside
in are usually rapidly evolving, and multiobjective design specifications intensify
the complexity of system design. One natural way to manage the
complexity of system design is by compositional methods. Of particular
interest is a multimodal control paradigm in which control systems are
designed by hierarchically nesting compositions of modes of operation such
that each mode of operation is designed to cope with a designated scenario
with respect to a design specification while the organization of modes of
operation depends on the ordering of these specifications.

A multimodal control system can be modeled as a hierarchical nesting of
parallel and serial compositions of discrete and continuous components.
Furthermore, a model of computation (MOC) [4] governs the behaviors and
interactions of components at each level of the hierarchy. Hybrid systems
[5-7] are considered as formalisms used to describe a complex system as
combinations of MOCs. This naturally leads to the generalization of the
design problem for the control of large-scale systems as a problem of multimodal
control synthesisrdesign in the modeling framework of hybrid systems.
The high-profile and safety-critical nature of such applications has fostered a
large and growing body of work on formal methods for hybrid systems:
mathematical logics, computational models and methods, and automated
reasoning tools supporting the formal specification and verification of performance
requirements for hybrid systems, along with the design and synthesis
of control programs for hybrid systems that are provably correct with respect
to formal specifications.

A multimodal control paradigm, which assumes that a set of controllers of
satisfactory performance have already been designed and must be used, is
considered. Each controller may be designed for a different set of outputs in
order to meet the given performance objectives and system constraints. When
such a collection of control modes is available, an important problem is to be
able to accomplish a variety of high-level tasks by appropriately switching
between the low-level control modes. Multimodal control has been studied,
especially in the context of stability and safety; see reference 8 for stability
results of switching between stable linear time-invariant controllers, reference
9 for safe switching conditions for systems with pointwise-in-time
constraints on state and control, and references 10 and 11 for controller
designs and switching conditions for satisfying multiple objectives such as
safety and optimal performance. In reference 12, we have proposed a
framework for the synthesis of mode switching for reachability specifications.
The problem of controller synthesis for preserving stability of a global
equilibrium point has been studied in reference 8.