Language Containment of Non-Deterministic to-Automata
Serdar Ta lran, Ramin Hojat · 2005
1 I n t r o d u c t i o n Many problems in formal verification can be formulated in a language containment framework. Deciding whether the language of an au tomaton M is contained in tha t of P , i.e., L(M) C L(P), is PSPACE-complete if P is non-deterministic. Language containment is usually tested by converting to a language emptiness question: an au tomaton P accepting the language L(P) is constructed, and it is determined whether L(M x P) is empty. Known asymptot ical ly op t imum ways of obtaining such a P requir e determinizing P first. Determinizat ion of w-au tomata with fairness constraints is more complex than determinization of finite au tomata . The straightforward subset construction does not work; specialized constructions taking into account the particular kind of fairness constraints need to be employed. Because of the exponential cost of determinization, it has been considered impractical, and verification systems have either been restricted to using deterministic au toma ta or employed means of verification other than language containment([Kur87],[HSIS94]) * Supported by SRC under grant DC-008-026.