diff --git a/prism-tests/bugfixes/supersimple.pm.boundedltl.props b/prism-tests/bugfixes/supersimple.pm.boundedltl.props
index 230177a3..5527a470 100644
--- a/prism-tests/bugfixes/supersimple.pm.boundedltl.props
+++ b/prism-tests/bugfixes/supersimple.pm.boundedltl.props
@@ -8,12 +8,12 @@ P>=1 [ F<=1 P>0 [ X F "a" ] ]
 // RESULT: true
 P>0.5 [ F>=1 P>0 [ X F "a" ] ]
 
-// These ones *should* fail for now
-// since there is no support for timed LTL currently
+// These ones are now supported
+// as well
 
-// RESULT: Error "not supported"
+// RESULT: true
 P>0.5 [ X F P>0 [ X F<=4 "a" ] ]
-// RESULT: Error "not supported"
+// RESULT: true
 P>0.5 [ X F<=1 P>0 [ X F "a" ] ]
-// RESULT: Error "not supported"
+// RESULT: true
 P>0.5 [ X F P>0 [ X F<=1 "a" ] ]
diff --git a/prism/src/automata/LTL2DA.java b/prism/src/automata/LTL2DA.java
index 0948cce8..68f8f952 100644
--- a/prism/src/automata/LTL2DA.java
+++ b/prism/src/automata/LTL2DA.java
@@ -49,6 +49,7 @@ import jltl2ba.LTLFragments;
 import jltl2dstar.LTL2Rabin;
 import parser.Values;
 import parser.ast.Expression;
+import parser.visitor.ExpandStepBoundsSyntactically;
 import parser.ast.ExpressionHOA;
 import parser.ast.ExpressionLabel;
 import parser.ast.ExpressionUnaryOp;
@@ -102,9 +103,6 @@ public class LTL2DA extends PrismComponent
 
 		boolean useExternal = useExternal();
 		boolean containsTemporalBounds = Expression.containsTemporalTimeBounds(ltl);
-		if (containsTemporalBounds) {
-			useExternal = false;
-		}
 
 		if (!useExternal) {
 			try {
@@ -114,51 +112,50 @@ public class LTL2DA extends PrismComponent
 					getLog().println("Taking "+result.getAutomataType()+" from library...");
 				}
 			} catch (Exception e) {
-				if (containsTemporalBounds) {
-					// there is (currently) no other way to translate LTL with temporal bounds,
-					// so treat an exception as a "real" one
-					throw e;
-				} else {
-					// there is the possibility that we might be able to construct
-					// an automaton below, just issue a warning
-					getLog().println("Warning: Exception during attempt to construct DRA using the LTL2RabinLibrary:");
-					getLog().println(" " + e.getMessage());
-				}
+				// there is the possibility that we might be able to construct
+				// an automaton below, just issue a warning
+				getLog().println("Warning: Exception during attempt to construct DRA using the LTL2RabinLibrary:");
+				getLog().println(" " + e.getMessage());
 			}
 		}
 
 		if (result == null) {
-			if (!containsTemporalBounds) {
-				if (useExternal) {
-					result = convertLTLFormulaToDAWithExternalTool(ltl, constants, allowedAcceptance);
-				} else {
-					SimpleLTL simpleLTL = ltl.convertForJltl2ba();
-
-					// don't use LTL2WDBA translation yet
-					boolean allowLTL2WDBA = false;
-					if (allowLTL2WDBA) {
-						LTLFragments fragments = LTLFragments.analyse(simpleLTL);
-						mainLog.println(fragments);
-
-						if (fragments.isSyntacticGuarantee() && AcceptanceType.contains(allowedAcceptance, AcceptanceType.REACH)) {
-							// a co-safety property
-							mainLog.println("Generating DFA for co-safety property...");
-							LTL2WDBA ltl2wdba = new LTL2WDBA(this);
-							result = ltl2wdba.cosafeltl2dfa(simpleLTL);
-						} else if (allowLTL2WDBA && fragments.isSyntacticObligation() && AcceptanceType.contains(allowedAcceptance, AcceptanceType.BUCHI)) {
-							// an obligation property
-							mainLog.println("Generating DBA for obligation property...");
-							LTL2WDBA ltl2wdba = new LTL2WDBA(this);
-							result = ltl2wdba.obligation2wdba(simpleLTL);
-						}
-					}
-					if (result == null) {
-						// use jltl2dstar LTL2DA
-						result = LTL2Rabin.ltl2da(simpleLTL, allowedAcceptance);
+			if (containsTemporalBounds) {
+				// remove time bounds syntactically
+				ExpandStepBoundsSyntactically visitor = new ExpandStepBoundsSyntactically(constants);
+				ltl = (Expression)ltl.deepCopy().accept(visitor);
+
+				mainLog.println("LTL formula with syntactically expanded bounds: "+ltl);
+			}
+
+			if (useExternal) {
+				result = convertLTLFormulaToDAWithExternalTool(ltl, constants, allowedAcceptance);
+			} else {
+				SimpleLTL simpleLTL = ltl.convertForJltl2ba();
+
+				// don't use LTL2WDBA translation yet
+				boolean allowLTL2WDBA = false;
+				if (allowLTL2WDBA) {
+
+					LTLFragments fragments = LTLFragments.analyse(simpleLTL);
+					mainLog.println(fragments);
+
+					if (fragments.isSyntacticGuarantee() && AcceptanceType.contains(allowedAcceptance, AcceptanceType.REACH)) {
+						// a co-safety property
+						mainLog.println("Generating DFA for co-safety property...");
+						LTL2WDBA ltl2wdba = new LTL2WDBA(this);
+						result = ltl2wdba.cosafeltl2dfa(simpleLTL);
+					} else if (allowLTL2WDBA && fragments.isSyntacticObligation() && AcceptanceType.contains(allowedAcceptance, AcceptanceType.BUCHI)) {
+						// an obligation property
+						mainLog.println("Generating DBA for obligation property...");
+						LTL2WDBA ltl2wdba = new LTL2WDBA(this);
+						result = ltl2wdba.obligation2wdba(simpleLTL);
 					}
 				}
-			} else {
-				throw new PrismNotSupportedException("Could not convert LTL formula to deterministic automaton, formula had time-bounds");
+				if (result == null) {
+					// use jltl2dstar LTL2DA
+					result = LTL2Rabin.ltl2da(simpleLTL, allowedAcceptance);
+				}
 			}
 		}
 
diff --git a/prism/src/automata/LTL2RabinLibrary.java b/prism/src/automata/LTL2RabinLibrary.java
index 4173888c..d7e52aed 100644
--- a/prism/src/automata/LTL2RabinLibrary.java
+++ b/prism/src/automata/LTL2RabinLibrary.java
@@ -160,7 +160,7 @@ public class LTL2RabinLibrary
 		// handle simple until formula with time bounds
 		if (Expression.containsTemporalTimeBounds(ltl)) {
 			if (!ltl.isSimplePathFormula()) {
-				throw new PrismNotSupportedException("Unsupported LTL formula with time bounds: "+ltl);
+				return null;
 			}
 
 			ltl = Expression.convertSimplePathFormulaToCanonicalForm(ltl);
diff --git a/prism/src/explicit/LTLModelChecker.java b/prism/src/explicit/LTLModelChecker.java
index c4ac1da4..c900fc92 100644
--- a/prism/src/explicit/LTLModelChecker.java
+++ b/prism/src/explicit/LTLModelChecker.java
@@ -135,11 +135,6 @@ public class LTLModelChecker extends PrismComponent
 				// Only support temporal bounds for discrete time models
 				return false;
 			}
-			
-			if (!expr.isSimplePathFormula()) {
-				// Only support temporal bounds for simple path formulas
-				return false;
-			}
 		}
 
 		if (Expression.isHOA(expr))
@@ -239,10 +234,6 @@ public class LTLModelChecker extends PrismComponent
 			if (model.getModelType().continuousTime()) {
 				throw new PrismNotSupportedException("Automaton construction for time-bounded operators not supported for " + model.getModelType()+".");
 			}
-
-			if (!expr.isSimplePathFormula()) {
-				throw new PrismNotSupportedException("Time-bounded operators not supported in LTL: " + expr);
-			}
 		}
 
 		if (Expression.isHOA(expr)) {
diff --git a/prism/src/prism/LTLModelChecker.java b/prism/src/prism/LTLModelChecker.java
index 82b5bccc..e5d59d3a 100644
--- a/prism/src/prism/LTLModelChecker.java
+++ b/prism/src/prism/LTLModelChecker.java
@@ -177,11 +177,6 @@ public class LTLModelChecker extends PrismComponent
 				// Only support temporal bounds for discrete time models
 				return false;
 			}
-			
-			if (!expr.isSimplePathFormula()) {
-				// Only support temporal bounds for simple path formulas
-				return false;
-			}
 		}
 
 		if (Expression.isHOA(expr)) {
@@ -326,10 +321,6 @@ public class LTLModelChecker extends PrismComponent
 			if (model.getModelType().continuousTime()) {
 				throw new PrismNotSupportedException("DA construction for time-bounded operators not supported for " + model.getModelType()+".");
 			}
-
-			if (!expr.isSimplePathFormula()) {
-				throw new PrismException("Time-bounded operators not supported in LTL: " + expr);
-			}
 		}
 		
 		long time;
diff --git a/prism/src/prism/ProbModelChecker.java b/prism/src/prism/ProbModelChecker.java
index 0c14bec6..37e48955 100644
--- a/prism/src/prism/ProbModelChecker.java
+++ b/prism/src/prism/ProbModelChecker.java
@@ -1023,11 +1023,6 @@ public class ProbModelChecker extends NonProbModelChecker
 				JDD.Deref(statesOfInterest);
 				throw new PrismNotSupportedException("DA construction for time-bounded operators not supported for " + model.getModelType()+".");
 			}
-
-			if (!expr.isSimplePathFormula()) {
-				JDD.Deref(statesOfInterest);
-				throw new PrismNotSupportedException("Time-bounded operators not supported in LTL: " + expr);
-			}
 		}
 
 		// Can't do "dfa" properties yet