diff --git a/prism/src/prism/StateModelChecker.java b/prism/src/prism/StateModelChecker.java
index 2374c6e7..71ccc8ed 100644
--- a/prism/src/prism/StateModelChecker.java
+++ b/prism/src/prism/StateModelChecker.java
@@ -28,9 +28,11 @@ package prism;
 
 import java.io.File;
 import java.io.FileNotFoundException;
+import java.util.HashMap;
 import java.util.List;
 import java.util.Set;
 import java.util.TreeSet;
+import java.util.Vector;
 
 import mtbdd.PrismMTBDD;
 import dv.DoubleVector;
@@ -40,6 +42,7 @@ import parser.*;
 import parser.ast.*;
 import parser.ast.ExpressionFilter.FilterOperator;
 import parser.type.*;
+import parser.visitor.ReplaceLabels;
 
 // Base class for model checkers - does state-based evaluations (no temporal/probabilistic)
 
@@ -1455,6 +1458,47 @@ public class StateModelChecker extends PrismComponent implements ModelChecker
 		return resVals;
 	}
 
+	/**
+	 * Method for handling the recursive part of PCTL* checking, i.e.,
+	 * recursively checking maximal state subformulas and replacing them
+	 * with labels and the corresponding satisfaction sets.
+	 * <br>
+	 * Extracts maximal state formula from an LTL path formula,
+	 * model checks them (with the current model checker and the current model)
+	 * and replaces them with ExpressionLabel objects that correspond
+	 * to freshly generated labels attached to the model.
+	 * <br>
+	 * Returns the modified Expression.
+	 *
+	 * @param expr the expression (a path formula)
+	 */
+	public Expression handleMaximalStateFormulas(Expression expr) throws PrismException
+	{
+		Vector<JDDNode> labelDD = new Vector<JDDNode>();
+
+		// construct LTL model checker, using this model checker instance
+		// (which is specialised for the model type) for the recursive
+		// model checking computation
+		LTLModelChecker ltlMC = new LTLModelChecker(this);
+
+		// check the maximal state subformulas and gather
+		// the satisfaction sets in labelBS, with index i
+		// in the vector corresponding to label Li in the
+		// returned formula
+		Expression exprNew = ltlMC.checkMaximalStateFormulas(this, model, expr.deepCopy(), labelDD);
+
+		HashMap<String, String> labelReplacements = new HashMap<String, String>();
+		for (int i=0; i < labelDD.size(); i++) {
+			String currentLabel = "L"+i;
+			// Attach satisfaction set for Li to the model, record necessary
+			// label renaming
+			String newLabel = model.addUniqueLabelDD("phi", labelDD.get(i), getDefinedLabelNames());
+			labelReplacements.put(currentLabel, newLabel);
+		}
+		// rename the labels
+		return (Expression) exprNew.accept(new ReplaceLabels(labelReplacements));
+	}
+
 	// Utility functions for symbolic model checkers 
 	
 	/**