diff --git a/prism/src/automata/LTL2DA.java b/prism/src/automata/LTL2DA.java
index e19811da..e06882fe 100644
--- a/prism/src/automata/LTL2DA.java
+++ b/prism/src/automata/LTL2DA.java
@@ -97,12 +97,12 @@ public class LTL2DA extends PrismComponent
 			useExternal = false;
 		}
 
-		if (AcceptanceType.contains(allowedAcceptance, AcceptanceType.RABIN) && !useExternal) {
-			// If we may construct a Rabin automaton, check the library first
+		if (!useExternal) {
 			try {
-				result = LTL2RabinLibrary.getDRAforLTL(ltl, constants);
+				// checking the library first
+				result = LTL2RabinLibrary.getDAforLTL(ltl, constants, allowedAcceptance);
 				if (result != null) {
-					getLog().println("Taking deterministic Rabin automaton from library...");
+					getLog().println("Taking "+result.getAutomataType()+" from library...");
 				}
 			} catch (Exception e) {
 				if (containsTemporalBounds) {
@@ -118,13 +118,16 @@ public class LTL2DA extends PrismComponent
 			}
 		}
 
-		// TODO (JK): support generation of DSA for simple path formula with time bound
-		if (result == null && !containsTemporalBounds) {
-			if (useExternal) {
-				result = convertLTLFormulaToDAWithExternalTool(ltl, constants, allowedAcceptance);
+		if (result == null) {
+			if (!containsTemporalBounds) {
+				if (useExternal) {
+					result = convertLTLFormulaToDAWithExternalTool(ltl, constants, allowedAcceptance);
+				} else {
+					// use jltl2dstar LTL2DA
+					result = LTL2Rabin.ltl2da(ltl.convertForJltl2ba(), allowedAcceptance);
+				}
 			} else {
-				// use jltl2dstar LTL2DA
-				result = LTL2Rabin.ltl2da(ltl.convertForJltl2ba(), allowedAcceptance);
+				throw new PrismNotSupportedException("Could not convert LTL formula to deterministic automaton, formula had time-bounds");
 			}
 		}
 
diff --git a/prism/src/automata/LTL2RabinLibrary.java b/prism/src/automata/LTL2RabinLibrary.java
index c8f30ad8..4173888c 100644
--- a/prism/src/automata/LTL2RabinLibrary.java
+++ b/prism/src/automata/LTL2RabinLibrary.java
@@ -30,8 +30,10 @@ package automata;
 import java.io.*;
 import java.util.*;
 
+import acceptance.AcceptanceOmega;
 import acceptance.AcceptanceRabin;
 import acceptance.AcceptanceRabin.RabinPair;
+import acceptance.AcceptanceType;
 import parser.Values;
 import parser.ast.*;
 import parser.visitor.ASTTraverse;
@@ -73,6 +75,45 @@ public class LTL2RabinLibrary
 		//dras.put("!((G \"L0\")&(G F \"L1\"))", "4 states (start 3), 2 labels: 0-{1}->1 0-{0, 1}->3 0-{}->1 0-{0}->0 1-{1}->1 1-{0, 1}->1 1-{}->1 1-{0}->1 2-{1}->1 2-{0, 1}->3 2-{}->1 2-{0}->0 3-{1}->1 3-{0, 1}->3 3-{}->1 3-{0}->2; 2 acceptance pairs: ({},{1}) ({1, 2, 3},{0})"); 
 	}
 
+	/**
+	 * Attempts to convert an LTL formula into a deterministic omega-automaton (with
+	 * one of the allowed acceptance conditions) by direct translation methods of the library:
+	 *
+	 * Relies on getDRAForLTL, with appropriate pre/post-processing for acceptance types
+	 * that are not Rabin.
+	 *
+	 * Return {@code null} if the automaton can not be constructed using the library.
+	 * <br> The LTL formula is represented as a PRISM Expression,
+	 * in which atomic propositions are represented by ExpressionLabel objects.
+	 * @param ltl the LTL formula
+	 * @param constants values for constants in the formula (may be {@code null})
+	 */
+	public static DA<BitSet, ? extends AcceptanceOmega> getDAforLTL(Expression ltl, Values constants, AcceptanceType... allowedAcceptance) throws PrismException {
+		// first try Rabin ...
+		if (AcceptanceType.contains(allowedAcceptance, AcceptanceType.RABIN)) {
+			return getDRAforLTL(ltl, constants);
+		}
+
+		// ..., then Streett (via negation and complementation at the acceptance level)
+		if (AcceptanceType.contains(allowedAcceptance, AcceptanceType.STREETT)) {
+			Expression negatedLtl = Expression.Not(ltl);
+			DA<BitSet, AcceptanceRabin> da = getDRAforLTL(negatedLtl, constants);
+			if (da != null) {
+				DA.switchAcceptance(da, da.getAcceptance().complementToStreett());
+				return da;
+			}
+		}
+
+		// ..., and then generic acceptance
+		if (AcceptanceType.contains(allowedAcceptance, AcceptanceType.GENERIC)) {
+			DA<BitSet, AcceptanceRabin> da = getDRAforLTL(ltl, constants);
+			DA.switchAcceptance(da, da.getAcceptance().toAcceptanceGeneric());
+			return da;
+		}
+
+		return null;
+	}
+
 	/**
 	 * Attempts to convert an LTL formula into a DRA by direct translation methods of the library:
 	 * <ul>