diff --git a/prism/src/parser/ast/ASTElement.java b/prism/src/parser/ast/ASTElement.java
index 83260575..39a5a4e4 100644
--- a/prism/src/parser/ast/ASTElement.java
+++ b/prism/src/parser/ast/ASTElement.java
@@ -496,6 +496,17 @@ public abstract class ASTElement
 		return visitor.getMaxNesting();
 	}
 
+	/**
+	 * Compute (maximum) number of nested probabilistic operators (P, S, R).
+	 * Optionally, pass a properties file for looking up property references.
+	 */
+	public int computeProbNesting(PropertiesFile propertiesFile) throws PrismLangException
+	{
+		ComputeProbNesting visitor = new ComputeProbNesting(propertiesFile);
+		accept(visitor);
+		return visitor.getMaxNesting();
+	}
+
 	/**
 	 * Convert to string showing tree representation.
 	 */
diff --git a/prism/src/parser/visitor/ComputeProbNesting.java b/prism/src/parser/visitor/ComputeProbNesting.java
index 90142f96..e49d7b5d 100644
--- a/prism/src/parser/visitor/ComputeProbNesting.java
+++ b/prism/src/parser/visitor/ComputeProbNesting.java
@@ -34,11 +34,20 @@ import prism.PrismLangException;
  */
 public class ComputeProbNesting extends ASTTraverse
 {
+	// Optional properties file to look up property references;
+	PropertiesFile propertiesFile = null;
+	
 	private int currentNesting;
 	private int maxNesting;
 	
 	public ComputeProbNesting()
 	{
+		this(null);
+	}
+
+	public ComputeProbNesting(PropertiesFile propertiesFile)
+	{
+		this.propertiesFile = propertiesFile;
 		currentNesting = 0;
 		maxNesting = 0;
 	}
@@ -80,5 +89,17 @@ public class ComputeProbNesting extends ASTTraverse
 	{
 		currentNesting--;
 	}
+	
+	public void visitPost(ExpressionProp e) throws PrismLangException
+	{
+		// If possible, look up property and recurse
+		if (propertiesFile != null) {
+			Property prop = propertiesFile.lookUpPropertyObjectByName(e.getName());
+			if (prop != null) {
+				prop.accept(this);
+			} else {
+				throw new PrismLangException("Unknown property reference " + e, e);
+			}
+		}
+	}
 }
-