diff --git a/prism/src/parser/ast/Expression.java b/prism/src/parser/ast/Expression.java
index 8fbe7e2d..a1775a03 100644
--- a/prism/src/parser/ast/Expression.java
+++ b/prism/src/parser/ast/Expression.java
@@ -978,6 +978,11 @@ public abstract class Expression extends ASTElement
 	/**
 	 * Test if an expression is a co-safe LTL formula, detected syntactically
 	 * (i.e. if it is in positive normal form and only uses X, F and U).
+	 * <br>
+	 * Treats nested non-Boolean state subformulas as opaque, i.e., considers
+	 * only the top-level LTL formula without recursing into operators such as P, R, etc.
+	 * <br>
+	 * Temporal operator bounds are considered to render the LTL formula unsafe.
 	 */
 	public static boolean isCoSafeLTLSyntactic(Expression expr)
 	{
@@ -990,6 +995,11 @@ public abstract class Expression extends ASTElement
 	 * If {@code convert} is true, the expression is first converted into positive normal form,
 	 * and then it is checked whether it only uses X, F and U.
 	 * For example, a => ! (G b) would return true if (and only if) {@code convert} was true.
+	 * <br>
+	 * Treats nested non-Boolean state subformulas as opaque, i.e., considers
+	 * only the top-level LTL formula without recursing into operators such as P, R, etc.
+	 * <br>
+	 * Temporal operator bounds are considered to render the LTL formula unsafe.
 	 */
 	public static boolean isCoSafeLTLSyntactic(Expression expr, boolean convert)
 	{
@@ -1000,12 +1010,17 @@ public abstract class Expression extends ASTElement
 			if (!isPositiveNormalFormLTL(expr))
 				return false;
 		}
-		// Check temporal operators
+
+		// Check temporal operators, don't recurse into nested operators
 		try {
-			ASTTraverse astt = new ASTTraverse()
+			ASTTraverse astt = new ExpressionTraverseNonNested()
 			{
 				public void visitPost(ExpressionTemporal e) throws PrismLangException
 				{
+					if (e.hasBounds()) {
+						throw new PrismLangException("Found temporal operator bound", e);
+					}
+
 					if (e.getOperator() == ExpressionTemporal.P_X)
 						return;
 					if (e.getOperator() == ExpressionTemporal.P_F)