diff --git a/prism/src/acceptance/AcceptanceBuchiDD.java b/prism/src/acceptance/AcceptanceBuchiDD.java
index d94be344..ad45f52a 100644
--- a/prism/src/acceptance/AcceptanceBuchiDD.java
+++ b/prism/src/acceptance/AcceptanceBuchiDD.java
@@ -99,6 +99,12 @@ public class AcceptanceBuchiDD implements AcceptanceOmegaDD
 		return new AcceptanceBuchiDD(acceptingStates.copy());
 	}
 
+	@Override
+	public void intersect(JDDNode restrict)
+	{
+		acceptingStates = JDD.And(acceptingStates, restrict.copy());
+	}
+
 	@Override
 	public String getSizeStatistics()
 	{
diff --git a/prism/src/acceptance/AcceptanceGenRabinDD.java b/prism/src/acceptance/AcceptanceGenRabinDD.java
index 194d241d..aa8f6564 100644
--- a/prism/src/acceptance/AcceptanceGenRabinDD.java
+++ b/prism/src/acceptance/AcceptanceGenRabinDD.java
@@ -153,6 +153,20 @@ public class AcceptanceGenRabinDD
 			return new AcceptanceGenericDD(AcceptanceGeneric.ElementType.AND, genericL, genericKs);
  		}
 
+		/**
+		 * Replaces the BDD functions for the acceptance sets
+		 * of this generalized Rabin pair with the intersection
+		 * of the current acceptance sets and the function {@code restrict}.
+		 * <br>[ REFS: <i>none</i>, DEREFS: <i>none</i> ]
+		 */
+		public void intersect(JDDNode restrict)
+		{
+			L = JDD.And(L, restrict.copy());
+			for (int i = 0; i < K_list.size(); i++) {
+				K_list.set(i, JDD.And(K_list.get(i), restrict.copy()));
+			}
+		}
+
 		/** Returns a textual representation of this Rabin pair. */
 		@Override
 		public String toString()
@@ -221,6 +235,14 @@ public class AcceptanceGenRabinDD
 		return result;
 	}
 
+	@Override
+	public void intersect(JDDNode restrict)
+	{
+		for (GenRabinPairDD pair : this) {
+			pair.intersect(restrict);
+		}
+	}
+
 	@Override
 	public void clear()
 	{
diff --git a/prism/src/acceptance/AcceptanceGenericDD.java b/prism/src/acceptance/AcceptanceGenericDD.java
index 418208c5..525c68b2 100644
--- a/prism/src/acceptance/AcceptanceGenericDD.java
+++ b/prism/src/acceptance/AcceptanceGenericDD.java
@@ -176,6 +176,28 @@ public class AcceptanceGenericDD implements AcceptanceOmegaDD {
 		throw new UnsupportedOperationException("Unsupported operator in generic acceptance expression");
 	}
 
+	@Override
+	public void intersect(JDDNode restrict)
+	{
+		switch(kind) {
+		case TRUE:
+		case FALSE:
+			return;
+		case AND:
+		case OR:
+			left.intersect(restrict);
+			right.intersect(restrict);
+			return;
+		case INF:
+		case INF_NOT:
+		case FIN:
+		case FIN_NOT:
+			states = JDD.And(states, restrict.copy());
+		}
+		throw new UnsupportedOperationException("Unsupported operator in generic acceptance expression");
+	}
+
+
 	@Override
 	public AcceptanceGenericDD clone()
 	{
diff --git a/prism/src/acceptance/AcceptanceOmegaDD.java b/prism/src/acceptance/AcceptanceOmegaDD.java
index 0005a4e3..b8b830a6 100644
--- a/prism/src/acceptance/AcceptanceOmegaDD.java
+++ b/prism/src/acceptance/AcceptanceOmegaDD.java
@@ -47,6 +47,14 @@ public interface AcceptanceOmegaDD extends Cloneable
 	 */
 	public AcceptanceOmegaDD clone();
 
+	/**
+	 * Replaces the BDD functions for all the acceptance sets
+	 * of this acceptance condition with the intersection
+	 * of the current acceptance sets and the function {@code restrict}.
+	 * <br>[ REFS: <i>none</i>, DEREFS: <i>none</i> ]
+	 */
+	public void intersect(JDDNode restrict);
+
 	/**
 	 * Get a string describing the acceptance condition's size,
 	 * i.e. "x Rabin pairs", etc.
diff --git a/prism/src/acceptance/AcceptanceRabinDD.java b/prism/src/acceptance/AcceptanceRabinDD.java
index 8fb51204..b59ff6d2 100644
--- a/prism/src/acceptance/AcceptanceRabinDD.java
+++ b/prism/src/acceptance/AcceptanceRabinDD.java
@@ -130,6 +130,18 @@ public class AcceptanceRabinDD
 			return new AcceptanceGenericDD(AcceptanceGeneric.ElementType.AND, genericL, genericK);
  		}
 
+		/**
+		 * Replaces the BDD functions for the acceptance sets
+		 * of this Rabin pair with the intersection
+		 * of the current acceptance sets and the function {@code restrict}.
+		 * <br>[ REFS: <i>none</i>, DEREFS: <i>none</i> ]
+		 */
+		public void intersect(JDDNode restrict)
+		{
+			L = JDD.And(L, restrict.copy());
+			K = JDD.And(K, restrict.copy());
+		}
+
 		/** Returns a textual representation of this Rabin pair. */
 		@Override
 		public String toString()
@@ -189,6 +201,14 @@ public class AcceptanceRabinDD
 		return result;
 	}
 
+	@Override
+	public void intersect(JDDNode restrict)
+	{
+		for (RabinPairDD pair : this) {
+			pair.intersect(restrict);
+		}
+	}
+
 	/**
 	 * Get the Streett acceptance condition that is the dual of this Rabin acceptance condition, i.e.,
 	 * any word that is accepted by this condition is rejected by the returned Streett condition.
diff --git a/prism/src/acceptance/AcceptanceReachDD.java b/prism/src/acceptance/AcceptanceReachDD.java
index e80b2333..36fc034f 100644
--- a/prism/src/acceptance/AcceptanceReachDD.java
+++ b/prism/src/acceptance/AcceptanceReachDD.java
@@ -99,6 +99,12 @@ public class AcceptanceReachDD implements AcceptanceOmegaDD
 		return new AcceptanceReachDD(goalStates.copy());
 	}
 
+	@Override
+	public void intersect(JDDNode restrict)
+	{
+		goalStates = JDD.And(goalStates, restrict.copy());
+	}
+
 	@Override
 	public String getSizeStatistics()
 	{
diff --git a/prism/src/acceptance/AcceptanceStreettDD.java b/prism/src/acceptance/AcceptanceStreettDD.java
index 8c2f9cc2..4d25d32b 100644
--- a/prism/src/acceptance/AcceptanceStreettDD.java
+++ b/prism/src/acceptance/AcceptanceStreettDD.java
@@ -132,6 +132,18 @@ public class AcceptanceStreettDD
 		    return new AcceptanceGenericDD(AcceptanceGeneric.ElementType.OR, genericR, genericG);
                 }
 
+		/**
+		 * Replaces the BDD functions for the acceptance sets
+		 * of this Streett pair with the intersection
+		 * of the current acceptance sets and the function {@code restrict}.
+		 * <br>[ REFS: <i>none</i>, DEREFS: <i>none</i> ]
+		 */
+		public void intersect(JDDNode restrict)
+		{
+			R = JDD.And(R, restrict.copy());
+			G = JDD.And(G, restrict.copy());
+		}
+
 		@Override
 		public String toString()
 		{
@@ -191,6 +203,14 @@ public class AcceptanceStreettDD
 	}
 
 
+	@Override
+	public void intersect(JDDNode restrict)
+	{
+		for (StreettPairDD pair : this) {
+			pair.intersect(restrict);
+		}
+	}
+
 	@Override
 	public void clear()
 	{