Package owl.translations.mastertheorem
Provides the implementation of the Master Theorem as well as an efficient normalisation procedure
for linear temporal logic.
The Master Theorem is described in "S19"
(Bibliography.DISSERTATION_19) and has been presented before in the preceding
conference publication "EKS18"
(Bibliography.LICS_18).
The normalisation procedure is described in "SE20"
(Bibliography.LICS_20).
Classes containing 'Asymmetric' in their name implement the supporting material for the
LDBA-construction described in "SEJK16"
(Bibliography.CAV_16).
-
Class Summary Class Description AsymmetricEvaluatedFixpoints AsymmetricEvaluatedFixpoints.DeterministicAutomata Fixpoints Normalisation Δ₂-Normalisation according toBibliography.LICS_20with minor tweaks skipping unnecessary rewrite steps.Predicates Rewriter Rewriter.ToCoSafety Rewriter.ToSafety Selector SymmetricEvaluatedFixpoints SymmetricEvaluatedFixpoints.DeterministicAutomata SymmetricEvaluatedFixpoints.NonDeterministicAutomata -
Enum Summary Enum Description Normalisation.NormalisationMethod