Package org.svvrl.goal.core.comp.wdbw

  • Class Summary 
    Class Description
    DeterminizationToDBWByDEK07
    This class implements the algorithm of determinizing an ω-automaton to an equivalent DBW if any equivalent DBW exists [Christian Dax, Jochen Eisinger, Felix Klaedtke: Mechanizing the Powerset Construction for Restricted Classes of omega -Automata.
    DeterminizationToWDBWByDEK07
    This class implements the algorithm of determinizing an ω-automaton to an equivalent WDBW if any equivalent WDBW exists [Christian Dax, Jochen Eisinger, Felix Klaedtke: Mechanizing the Powerset Construction for Restricted Classes of omega -Automata.
    WDBWComplement
    This class provides an implementation of complementing a WDBW (weak deterministic Büchi word automata).
    WDCWComplement
    This class provides an implementation of complementing a WDCW (weak deterministic co-Büchi word automata).