diff --git a/prism/src/explicit/StateModelChecker.java b/prism/src/explicit/StateModelChecker.java
index 7c232958..fa50b3a0 100644
--- a/prism/src/explicit/StateModelChecker.java
+++ b/prism/src/explicit/StateModelChecker.java
@@ -35,6 +35,7 @@ import parser.ast.*;
 import parser.ast.ExpressionFilter.FilterOperator;
 import parser.type.*;
 import prism.PrismException;
+import prism.PrismLangException;
 import prism.PrismLog;
 import prism.PrismPrintStreamLog;
 import prism.PrismSettings;
@@ -254,6 +255,10 @@ public class StateModelChecker
 		if (expr instanceof ExpressionUnaryOp) {
 			res = checkExpressionUnaryOp(model, (ExpressionUnaryOp) expr);
 		}
+		// Functions
+		else if (expr instanceof ExpressionFunc) {
+			res = checkExpressionFunc(model, (ExpressionFunc) expr);
+		}
 		// Literals
 		else if (expr instanceof ExpressionLiteral) {
 			res = checkExpressionLiteral(model, (ExpressionLiteral) expr);
@@ -347,6 +352,117 @@ public class StateModelChecker
 		return res1;
 	}
 
+	/**
+	 * Model check a function.
+	 */
+	protected StateValues checkExpressionFunc(Model model, ExpressionFunc expr) throws PrismException
+	{
+		switch (expr.getNameCode()) {
+		case ExpressionFunc.MIN:
+		case ExpressionFunc.MAX:
+			return checkExpressionFuncNary(model, expr);
+		case ExpressionFunc.FLOOR:
+		case ExpressionFunc.CEIL:
+			return checkExpressionFuncUnary(model, expr);
+		case ExpressionFunc.POW:
+		case ExpressionFunc.MOD:
+		case ExpressionFunc.LOG:
+			return checkExpressionFuncBinary(model, expr);
+		default:
+			throw new PrismException("Unrecognised function \"" + expr.getName() + "\"");
+		}
+	}
+
+	protected StateValues checkExpressionFuncUnary(Model model, ExpressionFunc expr) throws PrismException
+	{
+		StateValues res1 = null;
+		int op = expr.getNameCode();
+		
+		// Check operand recursively
+		res1 = checkExpression(model, expr.getOperand(0));
+		
+		// Apply operation
+		try {
+			res1.applyFunctionUnary(op);
+		} catch (PrismException e) {
+			if (res1 != null)
+				res1.clear();
+			if (e instanceof PrismLangException)
+				((PrismLangException) e).setASTElement(expr);
+			throw e;
+		}
+		
+		return res1;
+	}
+	
+	protected StateValues checkExpressionFuncBinary(Model model, ExpressionFunc expr) throws PrismException
+	{
+		StateValues res1 = null, res2 = null;
+		int op = expr.getNameCode();
+		
+		// Check operands recursively
+		try {
+			res1 = checkExpression(model, expr.getOperand(0));
+			res2 = checkExpression(model, expr.getOperand(1));
+		} catch (PrismException e) {
+			if (res1 != null)
+				res1.clear();
+			throw e;
+		}
+		
+		// Apply operation
+		try {
+			res1.applyFunctionBinary(op, res2);
+			res2.clear();
+		} catch (PrismException e) {
+			if (res1 != null)
+				res1.clear();
+			if (res2 != null)
+				res2.clear();
+			if (e instanceof PrismLangException)
+				((PrismLangException) e).setASTElement(expr);
+			throw e;
+		}
+		
+		return res1;
+	}
+	
+	protected StateValues checkExpressionFuncNary(Model model, ExpressionFunc expr) throws PrismException
+	{
+		StateValues res1 = null, res2 = null;
+		int i, n, op = expr.getNameCode();
+		
+		// Check first operand recursively
+		res1 = checkExpression(model, expr.getOperand(0));
+		// Go through remaining operands
+		n = expr.getNumOperands();
+		for (i = 1; i < n; i++) {
+			// Check next operand recursively
+			try {
+				res2 = checkExpression(model, expr.getOperand(i));
+			} catch (PrismException e) {
+				if (res2 != null)
+					res2.clear();
+				throw e;
+			}
+			// Apply operation
+			try {
+				res1.applyFunctionBinary(op, res2);
+				res2.clear();
+			} catch (PrismException e) {
+				if (res1 != null)
+					res1.clear();
+				if (res2 != null)
+					res2.clear();
+				if (e instanceof PrismLangException)
+					((PrismLangException) e).setASTElement(expr);
+				throw e;
+			}
+		}
+		
+		return res1;
+	}
+	
 	/**
 	 * Model check a literal.
 	 */
diff --git a/prism/src/explicit/StateValues.java b/prism/src/explicit/StateValues.java
index 41d485bd..d417b602 100644
--- a/prism/src/explicit/StateValues.java
+++ b/prism/src/explicit/StateValues.java
@@ -35,6 +35,7 @@ import java.util.List;
 
 import parser.State;
 import parser.ast.ExpressionBinaryOp;
+import parser.ast.ExpressionFunc;
 import parser.ast.ExpressionUnaryOp;
 import parser.type.Type;
 import parser.type.TypeBool;
@@ -291,7 +292,8 @@ public class StateValues
 	}
 
 	/**
-	 * Modify the vector by applying binary operator {@code op} with second operand {@code sv}.
+	 * Modify the vector by applying binary operator {@code op} with second operand {@code sv},
+	 * where {@code op} refers to the codes in {@link ExpressionBinaryOp}.
 	 */
 	public void applyBinaryOp(int op, StateValues sv) throws PrismException
 	{
@@ -769,7 +771,8 @@ public class StateValues
 	}
 
 	/**
-	 * Modify the vector by applying unary operator {@code op}.
+	 * Modify the vector by applying unary operator {@code op},
+	 * where {@code op} refers to the codes in {@link ExpressionUnaryOp}.
 	 */
 	public void applyUnaryOp(int op) throws PrismException
 	{
@@ -814,6 +817,250 @@ public class StateValues
 		}
 	}
 
+	/**
+	 * Modify the vector by applying (unary) function {@code op},
+	 * where {@code op} refers to the codes in {@link parser.ast.ExpressionFunc}.
+	 */
+	public void applyFunctionUnary(int op) throws PrismException
+	{
+		switch (op) {
+		case ExpressionFunc.FLOOR:
+			floor();
+			break;
+		case ExpressionFunc.CEIL:
+			ceil();
+			break;
+		default:
+			throw new PrismException("Unknown unary function");
+		}
+	}
+
+	/**
+	 * Modify the vector by applying 'floor'.
+	 */
+	public void floor() throws PrismException
+	{
+		if (type instanceof TypeInt) {
+			// Nothing to do
+		} else if (type instanceof TypeDouble) {
+			valuesI = new int[size];
+			type = TypeInt.getInstance();
+			for (int i = 0; i < size; i++) {
+				valuesI[i] = ExpressionFunc.evaluateFloor(valuesD[i]);
+			}
+			valuesD = null;
+		} else {
+			throw new PrismException("Function floor can not be applied to Boolean vectors");
+		}
+	}
+
+	/**
+	 * Modify the vector by applying 'ceil'.
+	 */
+	public void ceil() throws PrismException
+	{
+		if (type instanceof TypeInt) {
+			// Nothing to do
+		} else if (type instanceof TypeDouble) {
+			valuesI = new int[size];
+			type = TypeInt.getInstance();
+			for (int i = 0; i < size; i++) {
+				valuesI[i] = ExpressionFunc.evaluateCeil(valuesD[i]);
+			}
+			valuesD = null;
+		} else {
+			throw new PrismException("Function ceil can not be applied to Boolean vectors");
+		}
+	}
+
+	/**
+	 * Modify the vector by applying (binary or N-ary) function {@code op} with second operand {@code sv},
+	 * where {@code op} refers to the codes in {@link parser.ast.ExpressionFunc}.
+	 */
+	public void applyFunctionBinary(int op, StateValues sv) throws PrismException
+	{
+		switch (op) {
+		case ExpressionFunc.POW:
+			pow(sv);
+			break;
+		case ExpressionFunc.MOD:
+			mod(sv);
+			break;
+		case ExpressionFunc.LOG:
+			log(sv);
+			break;
+		case ExpressionFunc.MIN:
+			min(sv);
+			break;
+		case ExpressionFunc.MAX:
+			max(sv);
+			break;
+		default:
+			throw new PrismException("Unknown binary function");
+		}
+	}
+
+	/**
+	 * Modify the vector by applying 'pow' with second operand {@code sv}.
+	 */
+	public void pow(StateValues sv) throws PrismException
+	{
+		if (type instanceof TypeInt) {
+			if (sv.type instanceof TypeInt) {
+				for (int i = 0; i < size; i++) {
+					valuesI[i] = ExpressionFunc.evaluatePowInt(valuesI[i], sv.valuesI[i]);
+				}
+			} else if (sv.type instanceof TypeDouble) {
+				valuesD = new double[size];
+				type = TypeDouble.getInstance();
+				for (int i = 0; i < size; i++) {
+					valuesD[i] = ExpressionFunc.evaluatePowDouble(valuesI[i], sv.valuesD[i]);
+				}
+				valuesI = null;
+			} else {
+				throw new PrismException("Function pow() can not be applied to Boolean vectors");
+			}
+		} else if (type instanceof TypeDouble) {
+			if (sv.type instanceof TypeInt) {
+				for (int i = 0; i < size; i++) {
+					valuesD[i] = ExpressionFunc.evaluatePowDouble(valuesD[i], sv.valuesI[i]);
+				}
+			} else if (sv.type instanceof TypeDouble) {
+				for (int i = 0; i < size; i++) {
+					valuesD[i] = ExpressionFunc.evaluatePowDouble(valuesD[i], sv.valuesD[i]);
+				}
+			} else {
+				throw new PrismException("Function pow() can not be applied to Boolean vectors");
+			}
+		} else {
+			throw new PrismException("Function pow() can not be applied to Boolean vectors");
+		}
+	}
+
+	/**
+	 * Modify the vector by applying 'mod' with second operand {@code sv}.
+	 */
+	public void mod(StateValues sv) throws PrismException
+	{
+		if (!(type instanceof TypeInt && sv.type instanceof TypeInt)) {
+			throw new PrismException("Function mod() can only be applied to integer vectors");
+		}
+		for (int i = 0; i < size; i++) {
+			valuesI[i] = ExpressionFunc.evaluateMod(valuesI[i], sv.valuesI[i]);
+		}
+	}
+
+	/**
+	 * Modify the vector by applying 'log' with operand {@code sv}.
+	 */
+	public void log(StateValues sv) throws PrismException
+	{
+		if (type instanceof TypeInt) {
+			valuesD = new double[size];
+			type = TypeDouble.getInstance();
+			if (sv.type instanceof TypeInt) {
+				for (int i = 0; i < size; i++) {
+					valuesD[i] = ExpressionFunc.evaluateLog(valuesI[i], sv.valuesI[i]);
+				}
+			} else if (sv.type instanceof TypeDouble) {
+				for (int i = 0; i < size; i++) {
+					valuesD[i] = ExpressionFunc.evaluateLog(valuesI[i], sv.valuesD[i]);
+				}
+			} else {
+				throw new PrismException("Function log() can not be applied to Boolean vectors");
+			}
+			valuesI = null;
+		} else if (type instanceof TypeDouble) {
+			if (sv.type instanceof TypeInt) {
+				for (int i = 0; i < size; i++) {
+					valuesD[i] = ExpressionFunc.evaluateLog(valuesD[i], sv.valuesI[i]);
+				}
+			} else if (sv.type instanceof TypeDouble) {
+				for (int i = 0; i < size; i++) {
+					valuesD[i] = ExpressionFunc.evaluateLog(valuesD[i], sv.valuesD[i]);
+				}
+			} else {
+				throw new PrismException("Function log() can not be applied to Boolean vectors");
+			}
+		} else {
+			throw new PrismException("Function log() can not be applied to Boolean vectors");
+		}
+	}
+
+	/**
+	 * Modify the vector by applying 'min' with operand {@code sv}.
+	 */
+	public void min(StateValues sv) throws PrismException
+	{
+		if (type instanceof TypeInt) {
+			if (sv.type instanceof TypeInt) {
+				for (int i = 0; i < size; i++) {
+					valuesI[i] = Math.min(valuesI[i], sv.valuesI[i]);
+				}
+			} else if (sv.type instanceof TypeDouble) {
+				valuesD = new double[size];
+				type = TypeDouble.getInstance();
+				for (int i = 0; i < size; i++) {
+					valuesD[i] = Math.min(valuesI[i], sv.valuesD[i]);
+				}
+				valuesI = null;
+			} else {
+				throw new PrismException("Function min() can not be applied to Boolean vectors");
+			}
+		} else if (type instanceof TypeDouble) {
+			if (sv.type instanceof TypeInt) {
+				for (int i = 0; i < size; i++) {
+					valuesD[i] = Math.min(valuesD[i], sv.valuesI[i]);
+				}
+			} else if (sv.type instanceof TypeDouble) {
+				for (int i = 0; i < size; i++) {
+					valuesD[i] = Math.min(valuesD[i], sv.valuesD[i]);
+				}
+			} else {
+				throw new PrismException("Function min() can not be applied to Boolean vectors");
+			}
+		} else {
+			throw new PrismException("Function min() can not be applied to Boolean vectors");
+		}
+	}
+
+	/**
+	 * Modify the vector by applying 'max' with operand {@code sv}.
+	 */
+	public void max(StateValues sv) throws PrismException
+	{
+		if (type instanceof TypeInt) {
+			if (sv.type instanceof TypeInt) {
+				for (int i = 0; i < size; i++) {
+					valuesI[i] = Math.max(valuesI[i], sv.valuesI[i]);
+				}
+			} else if (sv.type instanceof TypeDouble) {
+				valuesD = new double[size];
+				type = TypeDouble.getInstance();
+				for (int i = 0; i < size; i++) {
+					valuesD[i] = Math.max(valuesI[i], sv.valuesD[i]);
+				}
+				valuesI = null;
+			} else {
+				throw new PrismException("Function max() can not be applied to Boolean vectors");
+			}
+		} else if (type instanceof TypeDouble) {
+			if (sv.type instanceof TypeInt) {
+				for (int i = 0; i < size; i++) {
+					valuesD[i] = Math.max(valuesD[i], sv.valuesI[i]);
+				}
+			} else if (sv.type instanceof TypeDouble) {
+				for (int i = 0; i < size; i++) {
+					valuesD[i] = Math.max(valuesD[i], sv.valuesD[i]);
+				}
+			} else {
+				throw new PrismException("Function max() can not be applied to Boolean vectors");
+			}
+		} else {
+			throw new PrismException("Function max() can not be applied to Boolean vectors");
+		}
+	}
+
 	/**
 	 * Set the elements of this vector by reading them in from a file.
 	 */