From Global to Modular Verification

Here, we present a reasonably general model for both single and multi-agent systems. Each agent is modeled as a hybrid system that may coordinate its actions with other agents or treat the actions of other agents as disturbances. The modeling framework is modular in that a hybrid system can be specified as a composition of subsystems, and hierarchical in that a hybrid system can be specified at different levels of abstraction. On one level, an agent may be modeled as a collection of subsystems representing the plant dynamics, sensors, actuators, communication devices, and controllers. On a more abstract level, an agent may be modeled as a finite automaton representing a strategy transducing one hybrid data stream (sensor data and input signals) to another hybrid data stream (control commands and output signals).

The hybrid model described here is inspired by that of [2] for linear hybrid automata, with some generalization. A more thorough treatment may be found in [3]. A hybrid module H is defined to be the tuple , in which:

• is the state space, with a finite set of discrete states, and M an n-manifold; a state of the system is a pair ;
• is the product of the input set and disturbance set; the space of acceptable control and disturbance trajectories are denoted by , ;
• is a finite set of labels;
• is the set of initial conditions;
• is the invariant associated with each discrete state, meaning that the state (q, x) may flow within q only if ;
• is the set of discrete jumps with meaning that if the current state is (q, x), the system may instantaneously take a discrete transition to state (q', x');
• is a map which associates with each discrete state a control system f(q,x,u,d). For notational convenience we use to denote f(q,x,u,d).

Hybrid systems evolve in so-called ``dense time'' by either continuous flows or discrete transitions. Trajectories of the hybrid module H starting at a state (q,x) evolve according to as long as the continuous state remains within Inv(q). If the invariance condition is not satisfied then a discrete transition is forced and the continuous state may be reinitialized. If then the discrete state jumps from q to q' and the continuous state x is reinitialized to x' and then flows according to .

The two main operations on a hybrid module are parallel composition and output hiding. By composing two modules, we identify inputs of one module with outputs of the other module. By hiding the output of a module, it is no longer visible to the environment of the module. Decomposing a complex system into a subsystem hierarchy of hybrid modules and defining the interactions between the modules and the environmental inputs constitutes a control architecture. Figure 1 depicts subsystem interconnections and agent interactions.

  
Figure 1: Multiple Agent Interactions

Conversely, if a hybrid system is constructed from hybrid modules using composition and hiding, then the construction can be ``flattened'' into a single equivalent hybrid module by simple and well-defined operations such as variable substitution and parallel composition of finite state machines along with logical operations on guards, assignments, and invariants. This enables a fully modular and hierarchical design philosophy for complex hybrid systems.

We propose to generalize the verification theory for hybrid automata to hybrid modules, and to extend HYTECH for analyzing hybrid modules. For this purpose, we hope to build on several recent successes in compositional and hierarchical model checking for very large discrete systems, and adapt the underlying methods to the mixed discrete-continuous case. This includes, in particular, the following three methods:

Assume-guarantee reasoning for hybrid modules

An assume-guarantee principle asserts that if, under given environment assumptions, every subsystem is guaranteed to perform correctly, then the compound system performs correctly. Since for discrete systems, assume-guarantee principles depend on the existence of winning strategies in games between various subsystems (such as games between controller and plant), hybrid analogues will involve the study of continuous games. For this purpose, we plan to extend a novel temporal logic, called ATL, which we developed for the specification of discrete games, to the hybrid case [63].

Refinement checking for hybrid modules

Since it is computationally infeasible, even in simple cases, to check if one module refines another module, in practice, one is satisfied with checking sufficient conditions for refinement, such as whether there is a simulation relation between two modules. For hybrid modules, refinement checking is only more difficult, and therefore the role of simulation relations is even more important. We plan to define tractable notions of simulation between hybrid modules, and extend a novel algorithm for simulation checking, which we developed for discrete systems, to the hybrid case [64].

Hierarchical model checking for hybrid modules

We recently devised an efficient method for searching very large state spaces that are structured hierarchically [65]. The method explores a more detailed level only when the information that is available on a more abstract level is not sufficient for establishing the desired property of the system. Since hybrid state spaces are intrinsically infinite, a method that applies on-demand state expansion is even more promising than in the discrete case, and will make possible the algorithmic analysis of some systems that otherwise cannot be analyzed automatically.

In all three cases, we will develop the prerequisite theoretical results, and design and implement corresponding algorithms for hybrid modules.