diff --git a/prism/src/acceptance/AcceptanceGeneric.java b/prism/src/acceptance/AcceptanceGeneric.java
index 2ac902ea..febba209 100644
--- a/prism/src/acceptance/AcceptanceGeneric.java
+++ b/prism/src/acceptance/AcceptanceGeneric.java
@@ -32,7 +32,10 @@ import java.util.ArrayList;
 import java.util.BitSet;
 import java.util.Collections;
 import java.util.List;
+import java.util.Stack;
 
+import acceptance.AcceptanceRabin.RabinPair;
+import acceptance.AcceptanceStreett.StreettPair;
 import prism.PrismException;
 import prism.PrismNotSupportedException;
 import jdd.JDDVars;
@@ -366,6 +369,369 @@ public class AcceptanceGeneric implements AcceptanceOmega {
 		return this.clone();
 	}
 
+	/**
+	 * Attempt to convert this generic acceptance condition
+	 * to a Rabin condition. If this condition does not have
+	 * the required form (top-level disjunctions with conjunctive pairs),
+	 * returns {@code null}.
+	 * <br>
+	 * If the condition does not syntactically have the required
+	 * from but can be easily converted to one (e.g., by converting
+	 * a single Inf(S) to a Fin(emptyset) & Inf(S) etc) or by swapping
+	 * Inf and Fin, this will be done.
+	 * <br>
+	 * The BitSets for the state sets are cloned, i.e., modifications of
+	 * the state sets of the returned acceptance condition will not affect
+	 * the original generic acceptance condition.
+	 *
+	 * @param numStates the number of states in the underlying model/automaton (for generating state sets for true)
+	 * @return the generated AcceptanceRabin condition, or false on failure
+	 */
+	public AcceptanceRabin toAcceptanceRabin(int numStates)
+	{
+		AcceptanceRabin result = new AcceptanceRabin();
+		List<AcceptanceGeneric> disjuncts = extractDisjuncts();
+
+		for (AcceptanceGeneric term : disjuncts) {
+			RabinPair pair = term.toAcceptanceRabinPair(numStates);
+			if (pair == null) return null;
+			result.add(pair);
+		}
+
+		return result;
+	}
+
+	/**
+	 * Attempt to convert this generic acceptance to a Rabin pair.
+	 *
+	 * @param numStates the number of states in the underlying model/automaton (for generating state sets for true)
+	 * @return the generated RabinPair, or false on failure
+	 */
+	private RabinPair toAcceptanceRabinPair(int numStates)
+	{
+		BitSet L = null, K = null;
+		switch (getKind()) {
+		case TRUE:
+			L = new BitSet();
+			K = new BitSet();
+			K.set(0, numStates);
+			break;
+		case FALSE:
+			L = new BitSet();
+			L.set(0, numStates);
+			K = new BitSet();
+			break;
+		case AND: {
+			AcceptanceGeneric left = getLeft();
+			AcceptanceGeneric right = getRight();
+
+			if (left.getKind() == ElementType.INF || left.getKind() == ElementType.INF_NOT) {
+				// swap
+				AcceptanceGeneric tmp = left;
+				left = right;
+				right = tmp;
+			}
+
+			switch (left.getKind()) {
+			case AND:
+			case OR:
+			case FALSE:
+			case TRUE:
+			case INF:
+			case INF_NOT:
+				// not a Rabin condition
+				return null;
+			case FIN:
+				// Fin(A) <=> <>[]!A
+				// L = A
+				L = (BitSet) left.getStates().clone();
+				break;
+			case FIN_NOT:
+				// Fin(!A) <=> <>[]A
+				// L = !A
+				L = (BitSet) left.getStates().clone();
+				L.flip(0, numStates);
+				break;
+			}
+
+			switch (right.getKind()) {
+			case AND:
+			case OR:
+			case FALSE:
+			case TRUE:
+			case FIN:
+			case FIN_NOT:
+				// not a Rabin condition
+				return null;
+			case INF:
+				// Inf(A) <=> []<>A
+				// K = A
+				K = (BitSet) right.getStates().clone();
+				break;
+			case INF_NOT:
+				// Inf(!A) <=> []<>!A
+				// K = !A
+				K = (BitSet) right.getStates().clone();
+				K.flip(0, numStates);
+				break;
+			}
+
+			break;
+		}
+		case FIN:
+			// Fin(A) <=> <>[]!A & []<> true <=> RabinPair(A, true)
+			// L = A
+			L = (BitSet) getStates().clone();
+			// K = true
+			K = new BitSet();
+			K.set(0, numStates);
+			break;
+		case FIN_NOT:
+			// Fin(!A) <=> <>[]A & []<> true <=> RabinPair(!A, true)
+			// L = !A
+			L = (BitSet) getStates().clone();
+			L.flip(0, numStates);
+			// K = true
+			K = new BitSet();
+			K.set(0, numStates);
+			break;
+		case INF:
+			// Inf(A) <=> <>[]!false & []<> A <=> RabinPair(false, A)
+			// L = false
+			L = new BitSet();
+			// K = A
+			K = (BitSet) getStates().clone();
+			break;
+		case INF_NOT:
+			// Inf(!A) <=> <>[]!false & []<> !A <=> RabinPair(false, !A)
+			// L = false
+			L = new BitSet();
+			// K = !A
+			K = (BitSet) getStates().clone();
+			K.flip(0, numStates);
+			break;
+		case OR:
+			// not a Rabin pair
+			return null;
+		}
+
+		return new AcceptanceRabin.RabinPair(L, K);
+	}
+
+	/**
+	 * Attempt to convert this generic acceptance condition
+	 * to a Streett condition. If this condition does not have
+	 * the required form (top-level conjunction with disjunctive pairs),
+	 * returns {@code null}.
+	 * <br>
+	 * If the condition does not syntactically have the required
+	 * from but can be easily converted to one (e.g., by converting
+	 * a single Inf(S) to a Fin(true) | Inf(S) etc) or by swapping
+	 * Inf and Fin, this will be done.
+	 * <br>
+	 * The BitSets for the state sets are cloned, i.e., modifications of
+	 * the state sets of the returned acceptance condition will not affect
+	 * the original generic acceptance condition.
+	 *
+	 * @param numStates the number of states in the underlying model/automaton (for generating state sets for true)
+	 * @return the generated AcceptanceRabin condition, or false on failure
+	 */
+	public AcceptanceStreett toAcceptanceStreett(int numStates)
+	{
+		AcceptanceStreett result = new AcceptanceStreett();
+		List<AcceptanceGeneric> conjuncts = extractConjuncts();
+
+		for (AcceptanceGeneric term : conjuncts) {
+			StreettPair pair = term.toAcceptanceStreettPair(numStates);
+			if (pair == null) return null;
+			result.add(pair);
+		}
+
+		return result;
+	}
+
+	/**
+	 * Attempt to convert this generic acceptance to a Streett pair.
+	 *
+	 * @param numStates the number of states in the underlying model/automaton (for generating state sets for true)
+	 * @return the generated RabinPair, or false on failure
+	 */
+	private StreettPair toAcceptanceStreettPair(int numStates)
+	{
+		BitSet R = null, G = null;
+		switch (getKind()) {
+		case TRUE:
+			// true = []<> false -> []<> false
+			R = new BitSet();
+			G = new BitSet();
+			break;
+		case FALSE:
+			// false = []<> true -> []<> false
+			R = new BitSet();
+			R.set(0, numStates);
+			G = new BitSet();
+			break;
+		case OR: {
+			AcceptanceGeneric left = getLeft();
+			AcceptanceGeneric right = getRight();
+
+			if (left.getKind() == ElementType.INF || left.getKind() == ElementType.INF_NOT) {
+				// swap
+				AcceptanceGeneric tmp = left;
+				left = right;
+				right = tmp;
+			}
+
+			switch (left.getKind()) {
+			case AND:
+			case OR:
+			case FALSE:
+			case TRUE:
+			case INF:
+			case INF_NOT:
+				// not a Streett condition
+				return null;
+			case FIN:
+				// Fin(A) -> R = A
+				R = (BitSet) left.getStates().clone();
+				break;
+			case FIN_NOT:
+				// Fin(!A) -> R = !A
+				R = (BitSet) left.getStates().clone();
+				R.flip(0, numStates);
+				break;
+			}
+
+			switch (right.getKind()) {
+			case AND:
+			case OR:
+			case FALSE:
+			case TRUE:
+			case FIN:
+			case FIN_NOT:
+				// not a Streett condition
+				return null;
+			case INF:
+				// Inf(A) -> G = A
+				G = (BitSet) right.getStates().clone();
+				break;
+			case INF_NOT:
+				// Inf(!A) -> G = !A
+				G = (BitSet) right.getStates().clone();
+				G.flip(0, numStates);
+				break;
+			}
+
+			break;
+		}
+		case FIN:
+			// Fin(A) <=> []<>A -> []<>false
+			// R = A
+			R = (BitSet) getStates().clone();
+			// G = false
+			G = new BitSet();
+			break;
+		case FIN_NOT:
+			// Fin(!A) <=> []<>!A -> []<>false
+			// R = !A
+			R = (BitSet) getStates().clone();
+			R.flip(0, numStates);
+			// G = false
+			G = new BitSet();
+			break;
+		case INF:
+			// Inf(A) <=> []<>true -> []<>A
+			// R = true
+			R = new BitSet();
+			R.set(0, numStates);
+			// G = A
+			G = (BitSet) getStates().clone();
+			break;
+		case INF_NOT:
+			// Inf(!A) <=> []<>true -> []<>!A
+			// R = true
+			R = new BitSet();
+			R.set(0, numStates);
+			// G = !A
+			G = (BitSet) getStates().clone();
+			G.flip(0, numStates);
+			break;
+		case AND:
+			// not a Streett pair
+			return null;
+		}
+
+		return new AcceptanceStreett.StreettPair(R,G);
+	}
+
+	/**
+	 * Extract the operands of the top-level disjunctions, e.g.,
+	 * for (A & B) | (C | D)) would return the list [A&B,C,D].
+	 */
+	public List<AcceptanceGeneric> extractDisjuncts()
+	{
+		ArrayList<AcceptanceGeneric> result = new ArrayList<AcceptanceGeneric>();
+		Stack<AcceptanceGeneric> todo = new Stack<AcceptanceGeneric>();
+
+		todo.add(this);
+		while (!todo.isEmpty()) {
+			AcceptanceGeneric current = todo.pop();
+			switch (current.getKind()) {
+			case AND:
+			case FALSE:
+			case TRUE:
+			case FIN:
+			case FIN_NOT:
+			case INF:
+			case INF_NOT:
+				// not a top level disjunction, add to list
+				result.add(current);
+				break;
+			case OR:
+				// still a top level disjunction, recurse
+				todo.push(current.getRight());
+				todo.push(current.getLeft());
+				break;
+			}
+		}
+
+		return result;
+	}
+
+	/**
+	 * Extract the operands of the top-level conjunctions, e.g.,
+	 * for (A | B) & (C & D)) would return the list [A|B,C,D].
+	 */
+	public List<AcceptanceGeneric> extractConjuncts()
+	{
+		ArrayList<AcceptanceGeneric> result = new ArrayList<AcceptanceGeneric>();
+		Stack<AcceptanceGeneric> todo = new Stack<AcceptanceGeneric>();
+
+		todo.add(this);
+		while (!todo.isEmpty()) {
+			AcceptanceGeneric current = todo.pop();
+			switch (current.getKind()) {
+			case OR:
+			case FALSE:
+			case TRUE:
+			case FIN:
+			case FIN_NOT:
+			case INF:
+			case INF_NOT:
+				// not a top level conjunction, add to list
+				result.add(current);
+				break;
+			case AND:
+				// still a top level conjunction, recurse
+				todo.push(current.getRight());
+				todo.push(current.getLeft());
+				break;
+			}
+		}
+
+		return result;
+	}
+
 	@Override
 	public String toString() {
 		switch(kind) {