diff --git a/prism/src/explicit/DTMCModelChecker.java b/prism/src/explicit/DTMCModelChecker.java
index c439f02d..1d8dbf98 100644
--- a/prism/src/explicit/DTMCModelChecker.java
+++ b/prism/src/explicit/DTMCModelChecker.java
@@ -84,10 +84,10 @@ public class DTMCModelChecker extends ProbModelChecker
 			ExpressionTemporal exprTemp = (ExpressionTemporal) expr;
 			// Next
 			if (exprTemp.getOperator() == ExpressionTemporal.P_X) {
-				throw new PrismException("The explicit engine does not yet handle the next operator");
+				probs = checkProbNext(model, exprTemp);
 			}
 			// Until
-			if (exprTemp.getOperator() == ExpressionTemporal.P_U) {
+			else if (exprTemp.getOperator() == ExpressionTemporal.P_U) {
 				if (exprTemp.hasBounds()) {
 					probs = checkProbBoundedUntil(model, exprTemp);
 				} else {
@@ -106,6 +106,21 @@ public class DTMCModelChecker extends ProbModelChecker
 		return probs;
 	}
 
+	/**
+	 * Compute probabilities for a next operator.
+	 */
+	protected StateValues checkProbNext(Model model, ExpressionTemporal expr) throws PrismException
+	{
+		BitSet target = null;
+		ModelCheckerResult res = null;
+
+		// Model check the operand
+		target = checkExpression(model, expr.getOperand2()).getBitSet();
+
+		res = computeNextProbs((DTMC) model, target);
+		return StateValues.createFromDoubleArray(res.soln, model);
+	}
+	
 	/**
 	 * Compute probabilities for a bounded until operator.
 	 */
@@ -330,6 +345,39 @@ public class DTMCModelChecker extends ProbModelChecker
 
 	// Numerical computation functions
 
+	/**
+	 * Compute next=state probabilities.
+	 * i.e. compute the probability of being in a state in {@code target} in the next step.
+	 * @param dtmc The DTMC
+	 * @param target Target states
+	 */
+	public ModelCheckerResult computeNextProbs(DTMC dtmc, BitSet target) throws PrismException
+	{
+		ModelCheckerResult res = null;
+		int n;
+		double soln[], soln2[];
+		long timer;
+
+		timer = System.currentTimeMillis();
+		
+		// Store num states
+		n = dtmc.getNumStates();
+
+		// Create/initialise solution vector(s)
+		soln = Utils.bitsetToDoubleArray(target, n);
+		soln2 = new double[n];
+
+		// Next-step probabilities 
+		dtmc.mvMult(soln, soln2, null, false);
+
+		// Return results
+		res = new ModelCheckerResult();
+		res.soln = soln2;
+		res.numIters = 1;
+		res.timeTaken = timer / 1000.0;
+		return res;
+	}
+
 	/**
 	 * Compute reachability probabilities.
 	 * i.e. compute the probability of reaching a state in {@code target}.
diff --git a/prism/src/explicit/MDPModelChecker.java b/prism/src/explicit/MDPModelChecker.java
index d1534c05..6158d7b3 100644
--- a/prism/src/explicit/MDPModelChecker.java
+++ b/prism/src/explicit/MDPModelChecker.java
@@ -90,7 +90,7 @@ public class MDPModelChecker extends ProbModelChecker
 			ExpressionTemporal exprTemp = (ExpressionTemporal) expr;
 			// Next
 			if (exprTemp.getOperator() == ExpressionTemporal.P_X) {
-				throw new PrismException("The explicit engine does not yet handle the next operator");
+				probs = checkProbNext(model, exprTemp, min);
 			}
 			// Until
 			else if (exprTemp.getOperator() == ExpressionTemporal.P_U) {
@@ -112,6 +112,21 @@ public class MDPModelChecker extends ProbModelChecker
 		return probs;
 	}
 
+	/**
+	 * Compute probabilities for a next operator.
+	 */
+	protected StateValues checkProbNext(Model model, ExpressionTemporal expr, boolean min) throws PrismException
+	{
+		BitSet target = null;
+		ModelCheckerResult res = null;
+
+		// Model check the operand
+		target = checkExpression(model, expr.getOperand2()).getBitSet();
+
+		res = computeNextProbs((MDP) model, target, min);
+		return StateValues.createFromDoubleArray(res.soln, model);
+	}
+	
 	/**
 	 * Compute probabilities for a bounded until operator.
 	 */
@@ -228,6 +243,40 @@ public class MDPModelChecker extends ProbModelChecker
 
 	// Numerical computation functions
 
+	/**
+	 * Compute next=state probabilities.
+	 * i.e. compute the probability of being in a state in {@code target} in the next step.
+	 * @param mdp The MDP
+	 * @param target Target states
+	 * @param min Min or max probabilities (true=min, false=max)
+	 */
+	public ModelCheckerResult computeNextProbs(MDP mdp, BitSet target, boolean min) throws PrismException
+	{
+		ModelCheckerResult res = null;
+		int n;
+		double soln[], soln2[];
+		long timer;
+
+		timer = System.currentTimeMillis();
+		
+		// Store num states
+		n = mdp.getNumStates();
+
+		// Create/initialise solution vector(s)
+		soln = Utils.bitsetToDoubleArray(target, n);
+		soln2 = new double[n];
+
+		// Next-step probabilities 
+		mdp.mvMultMinMax(soln, min, soln2, null, false, null);
+
+		// Return results
+		res = new ModelCheckerResult();
+		res.soln = soln2;
+		res.numIters = 1;
+		res.timeTaken = timer / 1000.0;
+		return res;
+	}
+
 	/**
 	 * Compute reachability probabilities.
 	 * i.e. compute the min/max probability of reaching a state in {@code target}.
diff --git a/prism/src/explicit/STPGModelChecker.java b/prism/src/explicit/STPGModelChecker.java
index 24937942..3431743a 100644
--- a/prism/src/explicit/STPGModelChecker.java
+++ b/prism/src/explicit/STPGModelChecker.java
@@ -84,7 +84,7 @@ public class STPGModelChecker extends ProbModelChecker
 			ExpressionTemporal exprTemp = (ExpressionTemporal) expr;
 			// Next
 			if (exprTemp.getOperator() == ExpressionTemporal.P_X) {
-				throw new PrismException("The explicit engine does not yet handle the next operator");
+				probs = checkProbNext(model, exprTemp, min1, min2);
 			}
 			// Until
 			else if (exprTemp.getOperator() == ExpressionTemporal.P_U) {
@@ -106,6 +106,21 @@ public class STPGModelChecker extends ProbModelChecker
 		return probs;
 	}
 
+	/**
+	 * Compute probabilities for a next operator.
+	 */
+	protected StateValues checkProbNext(Model model, ExpressionTemporal expr, boolean min1, boolean min2) throws PrismException
+	{
+		BitSet target = null;
+		ModelCheckerResult res = null;
+
+		// Model check the operand
+		target = checkExpression(model, expr.getOperand2()).getBitSet();
+
+		res = computeNextProbs((STPG) model, target, min1, min2);
+		return StateValues.createFromDoubleArray(res.soln, model);
+	}
+	
 	/**
 	 * Compute probabilities for a bounded until operator.
 	 */
@@ -196,6 +211,41 @@ public class STPGModelChecker extends ProbModelChecker
 
 	// Numerical computation functions
 
+	/**
+	 * Compute next=state probabilities.
+	 * i.e. compute the probability of being in a state in {@code target} in the next step.
+	 * @param stpg The STPG
+	 * @param target Target states
+	 * @param min1 Min or max probabilities for player 1 (true=lower bound, false=upper bound)
+	 * @param min2 Min or max probabilities for player 2 (true=min, false=max)
+	 */
+	public ModelCheckerResult computeNextProbs(STPG stpg, BitSet target, boolean min1, boolean min2) throws PrismException
+	{
+		ModelCheckerResult res = null;
+		int n;
+		double soln[], soln2[];
+		long timer;
+
+		timer = System.currentTimeMillis();
+		
+		// Store num states
+		n = stpg.getNumStates();
+
+		// Create/initialise solution vector(s)
+		soln = Utils.bitsetToDoubleArray(target, n);
+		soln2 = new double[n];
+
+		// Next-step probabilities 
+		stpg.mvMultMinMax(soln, min1, min2, soln2, null, false, null);
+
+		// Return results
+		res = new ModelCheckerResult();
+		res.soln = soln2;
+		res.numIters = 1;
+		res.timeTaken = timer / 1000.0;
+		return res;
+	}
+
 	/**
 	 * Compute reachability probabilities.
 	 * i.e. compute the min/max probability of reaching a state in {@code target}.