| PastAutomaton |
This class is intended to construct a classic finite state automaton for a
past LTL formula (or past QPTL formula in prenex normal form) such that a
word is accepted by the automaton if and only if the reverse of the word
end-satisfies the formula.
|
| PastCover |
This class provides methods for computing covers of LTL past formulae.
|
| QPTL2ABWFuture |
This class provides a translation from a QPTL formula without past operators
to an equivalent alternating Büchi automaton.
|
| QPTL2BA |
|
| QPTL2BACanonical |
This class provides a translation from a QPTL formula in canonical forms to
an equivalent NBW.
|
| QPTL2BAFuture |
This class provides a translation from a QPTL formula without past operators
to an equivalent NBW.
|
| QPTL2BAOptions |
This class contains several options for the QPTL2BA translation algorithm.
|
| QPTL2BATranslators |
This class provides several translators based on the QPTL2BA translation
algorithm.
|
| QPTL2BATranslators.CanonicalQPTL2TWACW |
This class provides a translator from a QPTL formula in canonical forms to an
equivalent two-way alternating co-Büchi automaton.
|
| QPTL2BATranslators.FutureQPTL2ABW |
This class provides a translator from a QPTL formula without past operators
to an equivalent alternating Büchi automaton.
|
| QPTL2BATranslators.QPTL2NBW |
This class provides a translator from a QPTL formula to an NBW.
|
| QPTL2TWACWCanonical |
This class provides a translation from a QPTL formula in canonical forms to
an equivalent two-way alternating co-Büchi automaton.
|