Many situation in various application domains can be formalized as switched buffer networks, that is, networks of containers in which quantities of some sub-stances are stored and transported at various rates to other buffers. A mode of such a system is defined by the channels that are active at a given time, which determine the rates of change in the quantities of the substances in all the buffers. Switching occurs while opening or closing channels, starting or stopping a reaction, thus causing the system to move from one mode to another. Hybrid automata provide a natural modeling formalism for such systems, a model on which one can verify properties (lack of overflow or deadlock, arrival of products to certain buffers at pre-specified times and quantities) and even automatically synthesize switching controllers that achieve such goals in an efficient manner. Such verification and synthesis techniques can complement traditional analytic techniques that are harder to apply as the switching aspects become more dominant. Looking from the other side of the spectrum, reachability-based methods can be seen adding more rigor and coverage to simulation-based methodologies.
展开▼
