Reasoning about Finite-State Switched Systems
=============================================

A {\em switched system\/} is composed of components. The components do
not interact with one another. Rather, they all interact with the same
environment, which switches one of them on at each moment in time. In
standard concurrency, a component restricts the environment of the
other components, thus the concurrent system has fewer behaviors than
its components. On the other hand, in a switched system, a component
suggests an alternative to the other components, thus the switched
system has richer behaviors than its components.    

We study finite-state switched systems, where each of the underlying
components is a finite-state transducer. While the main challenge,
namely compositionality, is similar in standard concurrent systems and
in switched systems, the problems and solutions are different. In the
verification front, we suggest and study an assume-guarantee paradigm
for switched systems, and study formalisms in which satisfaction of a
specification in all components imply its satisfaction in the switched
system. In the synthesis front, we show that while compositional
synthesis and design are undecidable, the problem of synthesizing a
switching rule with which a given switched system satisfies an LTL
specification is decidable.