The Weakness of Self-Complementation

Model checking is a method for the verification of systems with respect to their specifications. Symbolic model-checking, which enables the verification of large systems, proceeds by evaluating fixed-point expressions over the system's set of states. Such evaluation is particularly simple and efficient when the expressions do not contain alternation between least and greatest fixed-point operators; namely, when they belong to the alternation-free µ-calculus (AFMC). Not all specifications, however, can be translated to AFMC, which is exactly as expressive as weak monadic second-order logic (WS2S). Rabin showed that a set τ of trees can be expressed inWS2S if and only if both τ and its complement can be recognized by nondeterministic Büchi tree automata. For the "only if" direction, Rabin constructed, given two nondeterministic Büchi tree automata u and u′ that recognize τ and its complement, a WS2S formula that is satisfied by exactly all trees in τ . Since the translation of WS2S to AFMC is nonelementary, this construction is not practical. Arnold and Niwinski improved Rabin's construction by a direct translation of u and u′ to AFMC, which involves a doubly-exponential blowup and is therefore still impractical. In this paper we describe an alternative and quadratic translation of u and u′ to AFMC. Our translation goes through weak alternating tree automata, and constitutes a step towards efficient symbolic model checking of highly expressive specification formalisms.