diff --git a/src/formula/PrctlFormulaChecker.h b/src/formula/PrctlFormulaChecker.h
index e99cb0666..ddb9d90ab 100644
--- a/src/formula/PrctlFormulaChecker.h
+++ b/src/formula/PrctlFormulaChecker.h
@@ -21,18 +21,21 @@ class PrctlFormulaChecker : public AbstractFormulaChecker<T> {
 		/*!
 		 *	Implementation of AbstractFormulaChecker::conforms() using code
 		 *	looking exactly like the sample code given there.
-		 *
-		 *	We currently allow And, Ap, Eventually, Not, Or,
-		 *	ProbabilisticNoBoundOperator.
 		 */
 		virtual bool conforms(const AbstractFormula<T>* formula) const {
+			// What to support: Principles of Model Checking Def. 10.76 + syntactic sugar
 			if (
 					dynamic_cast<const And<T>*>(formula) ||
 					dynamic_cast<const Ap<T>*>(formula) ||
+					dynamic_cast<const BoundedUntil<T>*>(formula) ||
 					dynamic_cast<const Eventually<T>*>(formula) ||
+					dynamic_cast<const Globally<T>*>(formula) ||
+					dynamic_cast<const Next<T>*>(formula) ||
 					dynamic_cast<const Not<T>*>(formula) ||
 					dynamic_cast<const Or<T>*>(formula) ||
-					dynamic_cast<const ProbabilisticNoBoundOperator<T>*>(formula)
+					dynamic_cast<const ProbabilisticNoBoundOperator<T>*>(formula) ||
+					dynamic_cast<const ProbabilisticBoundOperator<T>*>(formula) ||
+					dynamic_cast<const Until<T>*>(formula)
 				) {
 				return formula->conforms(*this);
 			}