| Atom |
An atom of a LTL formula is a set of its subformulae.
|
| Closure |
This class computes the closure and basic formulae for a LTL formula.
|
| Tableau |
A Tableau is a translator from a LTL formula to a label-on-state NGBW
based on [Zohar Manna and Amir Pnueli.
|
| TableauOptions |
This class contains several options for the Tableau translators.
|
| TableauTranslators |
This class provides several translators based on the Tableau approach.
|
| TableauTranslators.LTL2LOSNBW |
This is a translator from a LTL formula to a label-on-state NBW based on
the Tableau approach.
|
| TableauTranslators.LTL2LOSNGBW |
This is a translator from a LTL formula to a label-on-state NGBW based on
the Tableau approach.
|
| TableauTranslators.LTL2NBW |
This is a translator from a LTL formula to an NBW based on the Tableau
approach.
|
| TableauTranslators.LTL2NGBW |
This is a translator from a LTL formula to an NGBW based on the Tableau
approach.
|
| TableauTranslators.QPTL2LOSNBW |
This is a translator from a QPTL formula to a label-on-state NBW based on
the Tableau approach.
|
| TableauTranslators.QPTL2LOSNGBW |
This is a translator from a QPTL formula to a label-on-state NGBW based
on the Tableau approach.
|
| TableauTranslators.QPTL2NBW |
This is a translator from a QPTL formula to an NBW based on the Tableau
approach.
|
| TableauTranslators.QPTL2NGBW |
This is a translator from a QPTL formula to an NGBW based on the Tableau
approach.
|