Testing containment of omega-regular languages.

The use of automata to model non-terminating processes such as communication protocols and complex integrated hardware systems in conceptually attractive because it affords a well- understood mathematical model with an established literature. However, it has long been recognized that a serious limitation of the automaton model in this context is the size of the automaton state-space, which grows exponentially with the number of coordinating components in the protocol or system. Since most protocols or hardware systems of interest have many coordinating components, the automaton model has been all but dismissed from serious consideration in this context; the enormous size of the ensuing state-space has been thought to render its analysis intractable.