diff --git a/prism/src/explicit/ProbModelChecker.java b/prism/src/explicit/ProbModelChecker.java
index 6493dee0..238e5722 100644
--- a/prism/src/explicit/ProbModelChecker.java
+++ b/prism/src/explicit/ProbModelChecker.java
@@ -479,7 +479,7 @@ public class ProbModelChecker extends NonProbModelChecker
 			if (p < 0 || p > 1)
 				throw new PrismException("Invalid probability bound " + p + " in P operator");
 		}
-		min = relOp.isLowerBound();
+		min = relOp.isLowerBound() || relOp.isMin();
 
 		// Compute probabilities
 		switch (modelType) {
@@ -546,7 +546,7 @@ public class ProbModelChecker extends NonProbModelChecker
 			if (r < 0)
 				throw new PrismException("Invalid reward bound " + r + " in R[] formula");
 		}
-		min = relOp.isLowerBound();
+		min = relOp.isLowerBound() || relOp.isMin();
 
 		// Get reward info
 		if (modulesFile == null)
diff --git a/prism/src/param/ParamModelChecker.java b/prism/src/param/ParamModelChecker.java
index 413e524e..14903a9c 100644
--- a/prism/src/param/ParamModelChecker.java
+++ b/prism/src/param/ParamModelChecker.java
@@ -873,7 +873,7 @@ final public class ParamModelChecker extends PrismComponent
 			if (p.compareTo(0) == -1 || p.compareTo(1) == 1)
 				throw new PrismException("Invalid probability bound " + p + " in P operator");
 		}
-		min = relOp.isLowerBound();
+		min = relOp.isLowerBound() || relOp.isMin();
 
 		// Compute probabilities
 		if (!expr.getExpression().isSimplePathFormula()) {
@@ -977,7 +977,7 @@ final public class ParamModelChecker extends PrismComponent
 			if (r.compareTo(0) == -1)
 				throw new PrismException("Invalid reward bound " + r + " in R[] formula");
 		}
-		min = relOp.isLowerBound();
+		min = relOp.isLowerBound() || relOp.isMin();
 
 		// Get reward info
 		if (modulesFile == null)
@@ -1130,7 +1130,7 @@ final public class ParamModelChecker extends PrismComponent
 			if (p.compareTo(0) == -1 || p.compareTo(1) == 1)
 				throw new PrismException("Invalid probability bound " + p + " in P operator");
 		}
-		min = relOp.isLowerBound();
+		min = relOp.isLowerBound() || relOp.isMin();
 
 		// Compute probabilities
 		probs = checkProbSteadyState(model, expr.getExpression(), min, needStates);
diff --git a/prism/src/parser/ast/RelOp.java b/prism/src/parser/ast/RelOp.java
index 89914865..a532c8cc 100644
--- a/prism/src/parser/ast/RelOp.java
+++ b/prism/src/parser/ast/RelOp.java
@@ -31,14 +31,29 @@ public enum RelOp {
 	}
 
 	/**
-	 * Returns true if this corresponds to a lower bound (e.g. >, >=, min=).
+	 * Returns true if this corresponds to a lower bound (i.e. >, >=).
+	 * NB: "min=?" does not return true for this.
 	 */
 	public boolean isLowerBound()
 	{
 		switch (this) {
 		case GT:
 		case GEQ:
-		case MIN:
+			return true;
+		default:
+			return false;
+		}
+	}
+
+	/**
+	 * Returns true if this corresponds to an upper bound (i.e. <, <=).
+	 * NB: "max=?" does not return true for this.
+	 */
+	public boolean isUpperBound()
+	{
+		switch (this) {
+		case LT:
+		case LEQ:
 			return true;
 		default:
 			return false;
@@ -60,13 +75,38 @@ public enum RelOp {
 	}
 
 	/**
-	 * Returns true if this corresponds to an upper bound (e.g. <, <=, max=).
+	 * Returns true if this is numerical (e.g. min=?, max=?).
 	 */
-	public boolean isUpperBound()
+	public boolean isNumerical()
+	{
+		switch (this) {
+		case MIN:
+		case MAX:
+			return true;
+		default:
+			return false;
+		}
+	}
+
+	/**
+	 * Returns true if this corresponds to minimum (min=?).
+	 */
+	public boolean isMin()
+	{
+		switch (this) {
+		case MIN:
+			return true;
+		default:
+			return false;
+		}
+	}
+
+	/**
+	 * Returns true if this corresponds to maximum (max=?).
+	 */
+	public boolean isMax()
 	{
 		switch (this) {
-		case LT:
-		case LEQ:
 		case MAX:
 			return true;
 		default:
diff --git a/prism/src/prism/NondetModelChecker.java b/prism/src/prism/NondetModelChecker.java
index 4c7b9487..b770ebf8 100644
--- a/prism/src/prism/NondetModelChecker.java
+++ b/prism/src/prism/NondetModelChecker.java
@@ -170,7 +170,7 @@ public class NondetModelChecker extends NonProbModelChecker
 			if (p < 0 || p > 1)
 				throw new PrismException("Invalid probability bound " + p + " in P operator");
 		}
-		min = relOp.isLowerBound();
+		min = relOp.isLowerBound() || relOp.isMin();
 
 		// Check for trivial (i.e. stupid) cases
 		if (pb != null) {
@@ -235,7 +235,7 @@ public class NondetModelChecker extends NonProbModelChecker
 			if (r < 0)
 				throw new PrismException("Invalid reward bound " + r + " in R operator");
 		}
-		min = relOp.isLowerBound();
+		min = relOp.isLowerBound() || relOp.isMin();
 
 		// get reward info
 		if (model.getNumRewardStructs() == 0)
diff --git a/prism/src/pta/PTAModelChecker.java b/prism/src/pta/PTAModelChecker.java
index 08e91eba..b704416b 100644
--- a/prism/src/pta/PTAModelChecker.java
+++ b/prism/src/pta/PTAModelChecker.java
@@ -190,10 +190,11 @@ public class PTAModelChecker extends PrismComponent
 		double prob;
 
 		// Check whether Pmin=? or Pmax=? (only two cases allowed)
-		if (expr.getProb() != null) {
+		RelOp relOp = expr.getRelOp();
+		if (!relOp.isNumerical()) {
 			throw new PrismException("PTA model checking currently only supports Pmin=? and Pmax=? properties (try the digital clocks engine instead)");
 		}
-		min = expr.getRelOp().isLowerBound();
+		min = relOp.isLowerBound() || relOp.isMin();
 
 		// Check this is a F path property (only case allowed at the moment)
 		if (!(expr.getExpression() instanceof ExpressionTemporal))