diff --git a/src/modelchecker/prctl/AbstractModelChecker.h b/src/modelchecker/prctl/AbstractModelChecker.h
index 793af403e..a45a1dc50 100644
--- a/src/modelchecker/prctl/AbstractModelChecker.h
+++ b/src/modelchecker/prctl/AbstractModelChecker.h
@@ -68,14 +68,14 @@ public:
 	/*!
 	 * Constructs an AbstractModelChecker with the given model.
 	 */
-	explicit AbstractModelChecker(storm::models::AbstractModel<Type> const& model) : model(model) {
+	explicit AbstractModelChecker(storm::models::AbstractModel<Type> const& model, storm::storage::BitVector* subSystem = nullptr) : model(model), subSystem(subSystem) {
 		// Intentionally left empty.
 	}
 	/*!
 	 * Copy constructs an AbstractModelChecker from the given model checker. In particular, this means that the newly
 	 * constructed model checker will have the model of the given model checker as its associated model.
 	 */
-	explicit AbstractModelChecker(AbstractModelChecker<Type> const& modelchecker) : model(modelchecker.model) {
+	explicit AbstractModelChecker(AbstractModelChecker<Type> const& modelchecker) : model(modelchecker.model), subSystem(modelchecker.subSystem) {
 		// Intentionally left empty.
 	}
 	
@@ -205,7 +205,11 @@ public:
 	 */
 	storm::storage::BitVector checkAp(storm::property::prctl::Ap<Type> const& formula) const {
 		if (formula.getAp() == "true") {
-			return storm::storage::BitVector(model.getNumberOfStates(), true);
+			if(subSystem != nullptr) {
+				return *subSystem;
+			} else {
+				return storm::storage::BitVector(model.getNumberOfStates(), true);
+			}
 		} else if (formula.getAp() == "false") {
 			return storm::storage::BitVector(model.getNumberOfStates());
 		}
@@ -215,7 +219,11 @@ public:
 			throw storm::exceptions::InvalidPropertyException() << "Atomic proposition '" << formula.getAp() << "' is invalid.";
 		}
 
-		return storm::storage::BitVector(model.getLabeledStates(formula.getAp()));
+		if(subSystem != nullptr) {
+			return *subSystem & storm::storage::BitVector(model.getLabeledStates(formula.getAp()));
+		} else {
+			return storm::storage::BitVector(model.getLabeledStates(formula.getAp()));
+		}
 	}
 
 	/*!
@@ -305,6 +313,15 @@ public:
 		return result;
 	}
 
+	/*!
+	 * Sets the subsystem.
+	 *
+	 * @param subSystem The subsystem the model check is to be confined to.
+	 */
+	void setSubSystem(storm::storage::BitVector* subSys) {
+		subSystem = subSys;
+	}
+
 private:
 
 	/*!
@@ -314,6 +331,13 @@ private:
 	 * model checker object is unsafe after the object has been destroyed.
 	 */
 	storm::models::AbstractModel<Type> const& model;
+
+	/*!
+	 * A pointer to the subsystem of the Model to which the check of the model is to be confined.
+	 *
+	 * @note that this is a nullptr iff the check is not to be confined.
+	 */
+	storm::storage::BitVector* subSystem;
 };
 
 } // namespace prctl