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 S -calculus (AFMC). Not all specifications, however, can be translated to AFMC, which is exactly as expressive as weak monadic second-orderlogic (WS2S). Rabin showed that a set T of trees can be expressed in WS2S if and only if both T and its complement can be recognized by nondeterministic B¨uchi tree automata. For the “only if” direction, Rabin constructed, given two nondeterministic B¨uchi tree automata U and UWV that recognize T and its complement, a WS2S formula that is satisfied by exactly all trees in T . Since the trans...

• Type: Conference
• Year: 1999
• Where: STACS
• Authors: Orna Kupferman, Moshe Y. Vardi
• Keywords: B¨uchi Tree Automata, Nondeterministic B¨uchi, STACS 1999, Theoretical Computer Science, Tree Automata