Stage-by-stage (Safra) Operation

This function stepwise complements a Büchi automaton using Safra's construction with 3 steps:

  1. A Büchi automaton is first converted to an equivalent deterministic Rabin automaton.
  2. Then the Rabin automaton is interpreted as a Streett automaton that accepts the complement language of the original Büchi automaton.
  3. Finally, the Streett automaton is converted back to an equivalent Büchi automaton (which complements the original Büchi automaton).


A sample of the step-by-step complement operation.
A screenshot of the step-by-step complement operation.
In the current step, the Büchi automaton (which is equivalent to the
PTL formula "pWq") is converted to an equivalent Rabin automaton.