Package org.svvrl.goal.core.tran.pltl2ba

  • Class Summary 
    Class Description
    LTL2TWVWAA
    This class provides an implementation of the translation from LTL formulae to co-Büchi two-way very weak alternating automata in [Paul Gastin, Denis Oddoux: LTL with Past and Two-Way Very-Weak Alternating Automata.
    PLTL2BA
    This class provides an implementation of the PLTL2BA translation algorithm [Paul Gastin, Denis Oddoux: LTL with Past and Two-Way Very-Weak Alternating Automata.
    PLTL2BAOptions
    This class contains several options for the PLTL2BA translation algorithm.
    PLTL2BATranslators
    This class provides several translators based on the PLTL2BA translation algorithm.
    PLTL2BATranslators.LTL2NBW
    This class provides a translator from a LTL formula to an NBW.
    PLTL2BATranslators.LTL2NTGBW
    This class provides a translator from a LTL formula into an NTGBW.
    PLTL2BATranslators.LTL2TWVWAA
    This class provides a translator from a LTL formula into a co-Büchi two-way VWAA.
    PLTL2BATranslators.QPTL2NBW
    This class provides a translator from a QPTL formula to an NBW.
    PLTL2BATranslators.QPTL2NTGBW
    This class provides a translator from a QPTL formula to an NTGBW.
    PLTL2BATranslators.QPTL2TWVWAA
    This class provides a translator from a QPTL formula to a co-Büchi 2VWAA.
    TWVWAA2NTGBW
    This class provides an implementation of the conversion in PLTL2BA from co-Büchi two-way VWAA to an equivalent NTGBW.