diff --git a/src/storm/logic/FragmentSpecification.cpp b/src/storm/logic/FragmentSpecification.cpp
index c00d53cf7..314bca97f 100644
--- a/src/storm/logic/FragmentSpecification.cpp
+++ b/src/storm/logic/FragmentSpecification.cpp
@@ -45,6 +45,17 @@ namespace storm {
             return pctl;
         }
 
+        FragmentSpecification pctlstar() {
+            FragmentSpecification pctlstar = pctl();
+
+            pctlstar.setBinaryBooleanPathFormulasAllowed(true);
+            pctlstar.setUnaryBooleanPathFormulasAllowed(true);
+            pctlstar.setNestedOperatorsAllowed(true);
+            pctlstar.setNestedPathFormulasAllowed(true);
+
+            return pctlstar;
+        }
+
         FragmentSpecification flatPctl() {
             FragmentSpecification flatPctl = pctl();
 
@@ -53,6 +64,35 @@ namespace storm {
             return flatPctl;
         }
 
+        FragmentSpecification prctl() {
+            FragmentSpecification prctl = pctl();
+
+            prctl.setRewardOperatorsAllowed(true);
+            prctl.setCumulativeRewardFormulasAllowed(true);
+            prctl.setInstantaneousFormulasAllowed(true);
+            prctl.setReachabilityRewardFormulasAllowed(true);
+            prctl.setLongRunAverageOperatorsAllowed(true);
+            prctl.setStepBoundedCumulativeRewardFormulasAllowed(true);
+            prctl.setTimeBoundedCumulativeRewardFormulasAllowed(true);
+
+            return prctl;
+        }
+
+        FragmentSpecification prctlstar() {
+            FragmentSpecification prctlstar = pctlstar();
+
+            prctlstar.setRewardOperatorsAllowed(true);
+            prctlstar.setCumulativeRewardFormulasAllowed(true);
+            prctlstar.setInstantaneousFormulasAllowed(true);
+            prctlstar.setReachabilityRewardFormulasAllowed(true);
+            prctlstar.setLongRunAverageOperatorsAllowed(true);
+            prctlstar.setStepBoundedCumulativeRewardFormulasAllowed(true);
+            prctlstar.setTimeBoundedCumulativeRewardFormulasAllowed(true);
+
+            return prctlstar;
+
+        }
+
         FragmentSpecification rpatl() {
             FragmentSpecification rpatl = propositional();
 
@@ -73,20 +113,6 @@ namespace storm {
             return rpatl;
         }
 
-        FragmentSpecification prctl() {
-            FragmentSpecification prctl = pctl();
-
-            prctl.setRewardOperatorsAllowed(true);
-            prctl.setCumulativeRewardFormulasAllowed(true);
-            prctl.setInstantaneousFormulasAllowed(true);
-            prctl.setReachabilityRewardFormulasAllowed(true);
-            prctl.setLongRunAverageOperatorsAllowed(true);
-            prctl.setStepBoundedCumulativeRewardFormulasAllowed(true);
-            prctl.setTimeBoundedCumulativeRewardFormulasAllowed(true);
-
-            return prctl;
-        }
-
         FragmentSpecification csl() {
             FragmentSpecification csl = pctl();
 
diff --git a/src/storm/logic/FragmentSpecification.h b/src/storm/logic/FragmentSpecification.h
index 07dd5c3da..8c50c635a 100644
--- a/src/storm/logic/FragmentSpecification.h
+++ b/src/storm/logic/FragmentSpecification.h
@@ -249,12 +249,18 @@ namespace storm {
         // Flat PCTL.
         FragmentSpecification flatPctl();
 
-        // rPATL for SMGs
-        FragmentSpecification rpatl();
+        // PCTL*
+        FragmentSpecification pctlstar();
 
         // PCTL + cumulative, instantaneous, reachability and long-run rewards.
         FragmentSpecification prctl();
 
+        // PCTL* + cumulative, instantaneous, reachability and long-run rewards.
+        FragmentSpecification prctlstar();
+
+        // rPATL for SMGs
+        FragmentSpecification rpatl();
+
         // Regular CSL.
         FragmentSpecification csl();