diff --git a/prism/src/explicit/Bisimulation.java b/prism/src/explicit/Bisimulation.java
index 64588a9a..bae09172 100644
--- a/prism/src/explicit/Bisimulation.java
+++ b/prism/src/explicit/Bisimulation.java
@@ -276,7 +276,7 @@ public class Bisimulation extends PrismComponent
 			BitSet propBSnew = new BitSet();
 			for (int j = propBS.nextSetBit(0); j >= 0; j = propBS.nextSetBit(j + 1))
 				propBSnew.set(partition[j]);
-			modelNew.labels.put(propName, propBSnew);
+			modelNew.addLabel(propName, propBSnew);
 		}
 	}
 }
diff --git a/prism/src/explicit/Model.java b/prism/src/explicit/Model.java
index 9b25a95f..6567041f 100644
--- a/prism/src/explicit/Model.java
+++ b/prism/src/explicit/Model.java
@@ -109,15 +109,21 @@ public interface Model
 	public boolean isDeadlockState(int i);
 	
 	/**
-	 * Get access to an (optional) list of states.
+	 * Get access to a list of states (optionally stored).
 	 */
 	public List<State> getStatesList();
 	
 	/**
-	 * Get access to an (optional) list of constant values.
+	 * Get access to a list of constant values (optionally stored).
 	 */
 	public Values getConstantValues();
 	
+	/**
+	 * Get the states that satisfy a label in this model (optionally stored).
+	 * Returns null if there is no label of this name.
+	 */
+	public BitSet getLabelStates(String name);
+	
 	/**
 	 * Get the total number of transitions in the model.
 	 */
diff --git a/prism/src/explicit/ModelExplicit.java b/prism/src/explicit/ModelExplicit.java
index fc05946c..38db438f 100644
--- a/prism/src/explicit/ModelExplicit.java
+++ b/prism/src/explicit/ModelExplicit.java
@@ -48,21 +48,26 @@ import prism.PrismLog;
  */
 public abstract class ModelExplicit implements Model
 {
-	// Number of states
+	// Basic model information
+	
+	/** Number of states */
 	protected int numStates;
-	// Initial states
+	/** Which states are initial states */
 	protected List<Integer> initialStates; // TODO: should be a (linkedhash?) set really
-	/**
-	 * States that are/were deadlocks. Where requested and where appropriate (DTMCs/MDPs),
-	 * these states may have been fixed at build time by adding self-loops.
-	 */
+	/** States that are/were deadlocks. Where requested and where appropriate (DTMCs/MDPs),
+	 * these states may have been fixed at build time by adding self-loops. */
 	protected TreeSet<Integer> deadlocks;
-	// State info (read only, just a pointer)
+	
+	// Additional, optional information associated with the model
+	
+	/** (Optionally) information about the states of this model,
+	 * i.e. the State object corresponding to each state index. */
 	protected List<State> statesList;
-	// Constant info (read only, just a pointer)
+	/** (Optionally) a list of values for constants associated with this model. */
 	protected Values constantValues;
-
-	public Map<String,BitSet> labels = new TreeMap<String, BitSet>();
+	/** (Optionally) some labels (atomic propositions) associated with the model,
+	 * represented as a String->BitSet mapping from their names to the states that satisfy them. */
+	protected Map<String,BitSet> labels = new TreeMap<String, BitSet>();
 	
 	// Mutators
 
@@ -82,6 +87,7 @@ public abstract class ModelExplicit implements Model
 		// Shallow copy of read-only stuff
 		statesList = model.statesList;
 		constantValues = model.constantValues;
+		labels = model.labels;
 	}
 
 	/**
@@ -104,6 +110,7 @@ public abstract class ModelExplicit implements Model
 		// (i.e. info that is not broken by permute)
 		statesList = null;
 		constantValues = model.constantValues;
+		labels.clear();
 	}
 
 	/**
@@ -115,6 +122,8 @@ public abstract class ModelExplicit implements Model
 		initialStates = new ArrayList<Integer>();
 		deadlocks = new TreeSet<Integer>();
 		statesList = null;
+		constantValues = null;
+		labels = new TreeMap<String, BitSet>();
 	}
 
 	/**
@@ -154,6 +163,17 @@ public abstract class ModelExplicit implements Model
 		this.constantValues = constantValues;
 	}
 
+	/**
+	 * Adds a label and the set the states that satisfy it.
+	 * Any existing label with the same name is overwritten.
+	 * @param name The name of the label
+	 * @param states The states that satisyy the label 
+	 */
+	public void addLabel(String name, BitSet states)
+	{
+		labels.put(name, states);
+	}
+
 	// Accessors (for Model interface)
 
 	@Override
@@ -236,6 +256,12 @@ public abstract class ModelExplicit implements Model
 		return constantValues;
 	}
 
+	@Override
+	public BitSet getLabelStates(String name)
+	{
+		return labels.get(name);
+	}
+	
 	@Override
 	public abstract int getNumTransitions();
 
diff --git a/prism/src/explicit/StateModelChecker.java b/prism/src/explicit/StateModelChecker.java
index f0b017f6..4420fb7e 100644
--- a/prism/src/explicit/StateModelChecker.java
+++ b/prism/src/explicit/StateModelChecker.java
@@ -669,10 +669,12 @@ public class StateModelChecker extends PrismComponent
 			}
 			return StateValues.createFromBitSet(bs, model);
 		} else {
-			BitSet bs = ((ModelExplicit) model).labels.get(expr.getName());
+			// First look at lables attached directly to model
+			BitSet bs = model.getLabelStates(expr.getName());
 			if (bs != null) {
 				return StateValues.createFromBitSet((BitSet) bs.clone(), model);
 			}
+			// Failing that, look in the properties file
 			ll = propertiesFile.getCombinedLabelList();
 			i = ll.getLabelIndex(expr.getName());
 			if (i == -1)
diff --git a/prism/src/explicit/SubNondetModel.java b/prism/src/explicit/SubNondetModel.java
index e2e2897c..92fbdccd 100644
--- a/prism/src/explicit/SubNondetModel.java
+++ b/prism/src/explicit/SubNondetModel.java
@@ -163,6 +163,11 @@ public class SubNondetModel implements NondetModel {
 		throw new UnsupportedOperationException();
 	}
 
+	@Override
+	public BitSet getLabelStates(String name) {
+		throw new UnsupportedOperationException();
+	}
+
 	@Override
 	public int getNumTransitions() {
 		return numTransitions;