Package owl.translations.ltl2ldba
Contains translations from linear temporal logic to limit-deterministic Büchi automata.
Classes containing 'Symmetric' in their name implement the translation described in
"S19" (Bibliography.DISSERTATION_19).
The construction has been sketched before in the preceding conference publication
"EKS18" (Bibliography.LICS_18).
Classes containing 'Asymmetric' in their name implement the translation described in
"SEJK16" (Bibliography.CAV_16).
-
Class Summary Class Description AnnotatedLDBA<S,T extends LtlLanguageExpressible,B extends GeneralizedBuchiAcceptance,X,Y> Translation-specific internal representation of LDBAs.AsymmetricLDBAConstruction<B extends GeneralizedBuchiAcceptance> AsymmetricProductState SymmetricLDBAConstruction<B extends GeneralizedBuchiAcceptance> SymmetricProductState