diff --git a/src/formula/AbstractFormula.h b/src/formula/AbstractFormula.h
index 42ba7bc02..186415965 100644
--- a/src/formula/AbstractFormula.h
+++ b/src/formula/AbstractFormula.h
@@ -14,7 +14,7 @@ namespace storm { namespace formula {
 template <class T> class AbstractFormula;
 }}
 
-#include "src/modelChecker/AbstractModelChecker.h"
+#include "src/modelchecker/AbstractModelChecker.h"
 #include "src/formula/AbstractFormulaChecker.h"
 
 namespace storm {
diff --git a/src/formula/AbstractPathFormula.h b/src/formula/AbstractPathFormula.h
index 4337cbe19..eeffcb4c1 100644
--- a/src/formula/AbstractPathFormula.h
+++ b/src/formula/AbstractPathFormula.h
@@ -13,8 +13,8 @@ template <class T> class AbstractPathFormula;
 }}
 
 #include "src/formula/AbstractFormula.h"
+#include "src/modelchecker/AbstractModelChecker.h"
 
-#include "modelChecker/AbstractModelChecker.h"
 #include <vector>
 #include <iostream>
 #include <typeinfo>
diff --git a/src/formula/AbstractStateFormula.h b/src/formula/AbstractStateFormula.h
index 9309bf610..9f4750f06 100644
--- a/src/formula/AbstractStateFormula.h
+++ b/src/formula/AbstractStateFormula.h
@@ -12,9 +12,9 @@ namespace storm { namespace formula {
 template <class T> class AbstractStateFormula;
 }}
 
-#include "AbstractFormula.h"
+#include "src/formula/AbstractFormula.h"
 #include "src/storage/BitVector.h"
-#include "src/modelChecker/AbstractModelChecker.h"
+#include "src/modelchecker/AbstractModelChecker.h"
 
 namespace storm {
 namespace formula {
diff --git a/src/formula/And.h b/src/formula/And.h
index d8078cd15..f92830c52 100644
--- a/src/formula/And.h
+++ b/src/formula/And.h
@@ -10,7 +10,7 @@
 
 #include "src/formula/AbstractStateFormula.h"
 #include "src/formula/AbstractFormulaChecker.h"
-#include "src/modelChecker/AbstractModelChecker.h"
+#include "src/modelchecker/AbstractModelChecker.h"
 #include <string>
 
 namespace storm {
diff --git a/src/formula/Ap.h b/src/formula/Ap.h
index ba5c13287..80bf54fcb 100644
--- a/src/formula/Ap.h
+++ b/src/formula/Ap.h
@@ -10,7 +10,7 @@
 
 #include "src/formula/AbstractStateFormula.h"
 #include "src/formula/AbstractFormulaChecker.h"
-#include "src/modelChecker/AbstractModelChecker.h"
+#include "src/modelchecker/AbstractModelChecker.h"
 
 namespace storm {
 namespace formula {
diff --git a/src/formula/BoundedEventually.h b/src/formula/BoundedEventually.h
index 4be075840..3d1f85e0b 100644
--- a/src/formula/BoundedEventually.h
+++ b/src/formula/BoundedEventually.h
@@ -8,12 +8,12 @@
 #ifndef STORM_FORMULA_BOUNDEDEVENTUALLY_H_
 #define STORM_FORMULA_BOUNDEDEVENTUALLY_H_
 
-#include "AbstractPathFormula.h"
-#include "AbstractStateFormula.h"
+#include "src/formula/AbstractPathFormula.h"
+#include "src/formula/AbstractStateFormula.h"
 #include "src/formula/AbstractFormulaChecker.h"
 #include "boost/integer/integer_mask.hpp"
 #include <string>
-#include "src/modelChecker/AbstractModelChecker.h"
+#include "src/modelchecker/AbstractModelChecker.h"
 
 namespace storm {
 
diff --git a/src/formula/BoundedNaryUntil.h b/src/formula/BoundedNaryUntil.h
index c42dab12b..fad114101 100644
--- a/src/formula/BoundedNaryUntil.h
+++ b/src/formula/BoundedNaryUntil.h
@@ -10,7 +10,7 @@
 
 #include "src/formula/AbstractPathFormula.h"
 #include "src/formula/AbstractStateFormula.h"
-#include "src/modelChecker/AbstractModelChecker.h"
+#include "src/modelchecker/AbstractModelChecker.h"
 #include "boost/integer/integer_mask.hpp"
 #include <string>
 #include <vector>
@@ -68,7 +68,7 @@ public:
 	 * Empty constructor
 	 */
 	BoundedNaryUntil() {
-		this->left = NULL;
+		this->left = nullptr;
 		this->right = new std::vector<std::tuple<AbstractStateFormula<T>*,T,T>>();
 	}
 
@@ -91,10 +91,10 @@ public:
 	 * (this behaviour can be prevented by setting the subtrees to NULL before deletion)
 	 */
 	virtual ~BoundedNaryUntil() {
-	  if (left != NULL) {
+	  if (left != nullptr) {
 		  delete left;
 	  }
-	  if (right != NULL) {
+	  if (right != nullptr) {
 		  delete right;
 	  }
 	}
@@ -205,7 +205,6 @@ private:
 };
 
 } //namespace formula
-
 } //namespace storm
 
 #endif /* STORM_FORMULA_BOUNDEDNARYUNTIL_H_ */
diff --git a/src/formula/BoundedUntil.h b/src/formula/BoundedUntil.h
index e00acac74..0c3323b61 100644
--- a/src/formula/BoundedUntil.h
+++ b/src/formula/BoundedUntil.h
@@ -10,7 +10,7 @@
 
 #include "src/formula/AbstractPathFormula.h"
 #include "src/formula/AbstractStateFormula.h"
-#include "src/modelChecker/AbstractModelChecker.h"
+#include "src/modelchecker/AbstractModelChecker.h"
 #include "boost/integer/integer_mask.hpp"
 #include <string>
 #include "src/formula/AbstractFormulaChecker.h"
diff --git a/src/formula/Eventually.h b/src/formula/Eventually.h
index 4b2ca1ba3..91623d353 100644
--- a/src/formula/Eventually.h
+++ b/src/formula/Eventually.h
@@ -8,9 +8,9 @@
 #ifndef STORM_FORMULA_EVENTUALLY_H_
 #define STORM_FORMULA_EVENTUALLY_H_
 
-#include "AbstractPathFormula.h"
-#include "AbstractStateFormula.h"
-#include "src/modelChecker/AbstractModelChecker.h"
+#include "src/formula/AbstractPathFormula.h"
+#include "src/formula/AbstractStateFormula.h"
+#include "src/modelchecker/AbstractModelChecker.h"
 
 namespace storm {
 
diff --git a/src/formula/Formulas.h b/src/formula/Formulas.h
index 9af1fed84..f7630a113 100644
--- a/src/formula/Formulas.h
+++ b/src/formula/Formulas.h
@@ -8,7 +8,7 @@
 #ifndef STORM_FORMULA_FORMULAS_H_
 #define STORM_FORMULA_FORMULAS_H_
 
-#include "modelChecker/ForwardDeclarations.h"
+#include "modelchecker/ForwardDeclarations.h"
 
 #include "AbstractFormula.h"
 #include "AbstractPathFormula.h"
@@ -35,6 +35,6 @@
 #include "RewardBoundOperator.h"
 #include "RewardNoBoundOperator.h"
 
-#include "modelChecker/DtmcPrctlModelChecker.h"
+#include "modelchecker/DtmcPrctlModelChecker.h"
 
 #endif /* STORM_FORMULA_FORMULAS_H_ */
diff --git a/src/formula/NoBoundOperator.h b/src/formula/NoBoundOperator.h
index 1a28b89d4..79578fee2 100644
--- a/src/formula/NoBoundOperator.h
+++ b/src/formula/NoBoundOperator.h
@@ -8,11 +8,11 @@
 #ifndef STORM_FORMULA_NOBOUNDOPERATOR_H_
 #define STORM_FORMULA_NOBOUNDOPERATOR_H_
 
-#include "AbstractFormula.h"
-#include "AbstractPathFormula.h"
+#include "src/formula/AbstractFormula.h"
+#include "src/formula/AbstractPathFormula.h"
 #include "src/formula/AbstractFormulaChecker.h"
 
-#include "modelChecker/ForwardDeclarations.h"
+#include "src/modelchecker/ForwardDeclarations.h"
 
 namespace storm {
 
diff --git a/src/formula/Not.h b/src/formula/Not.h
index cd7a20399..824e6e03b 100644
--- a/src/formula/Not.h
+++ b/src/formula/Not.h
@@ -10,7 +10,7 @@
 
 #include "AbstractStateFormula.h"
 #include "src/formula/AbstractFormulaChecker.h"
-#include "src/modelChecker/AbstractModelChecker.h"
+#include "src/modelchecker/AbstractModelChecker.h"
 
 namespace storm {
 
diff --git a/src/formula/BoundOperator.h b/src/formula/PathBoundOperator.h
similarity index 84%
rename from src/formula/BoundOperator.h
rename to src/formula/PathBoundOperator.h
index 512d48d2a..72bcc6d56 100644
--- a/src/formula/BoundOperator.h
+++ b/src/formula/PathBoundOperator.h
@@ -1,35 +1,35 @@
 /*
- * BoundOperator.h
+ * PathBoundOperator.h
  *
  *  Created on: 27.12.2012
  *      Author: Christian Dehnert
  */
 
-#ifndef STORM_FORMULA_BOUNDOPERATOR_H_
-#define STORM_FORMULA_BOUNDOPERATOR_H_
+#ifndef STORM_FORMULA_PATHBOUNDOPERATOR_H_
+#define STORM_FORMULA_PATHBOUNDOPERATOR_H_
 
 #include "src/formula/AbstractStateFormula.h"
 #include "src/formula/AbstractPathFormula.h"
 #include "src/formula/AbstractFormulaChecker.h"
-#include "src/modelChecker/AbstractModelChecker.h"
+#include "src/modelchecker/AbstractModelChecker.h"
 #include "src/utility/ConstTemplates.h"
 
 namespace storm {
 
 namespace formula {
 
-template <class T> class BoundOperator;
+template <class T> class PathBoundOperator;
 
 /*!
- *  @brief Interface class for model checkers that support BoundOperator.
+ *  @brief Interface class for model checkers that support PathBoundOperator.
  *   
- *  All model checkers that support the formula class BoundOperator must inherit
+ *  All model checkers that support the formula class PathBoundOperator must inherit
  *  this pure virtual class.
  */
 template <class T>
-class IBoundOperatorModelChecker {
+class IPathBoundOperatorModelChecker {
     public:
-        virtual storm::storage::BitVector* checkBoundOperator(const BoundOperator<T>& obj) const = 0;
+        virtual storm::storage::BitVector* checkPathBoundOperator(const PathBoundOperator<T>& obj) const = 0;
 };
 
 /*!
@@ -54,7 +54,7 @@ class IBoundOperatorModelChecker {
  * @see AbstractFormula
  */
 template<class T>
-class BoundOperator : public AbstractStateFormula<T> {
+class PathBoundOperator : public AbstractStateFormula<T> {
 
 public:
 	enum ComparisonType { LESS, LESS_EQUAL, GREATER, GREATER_EQUAL };
@@ -66,7 +66,7 @@ public:
 	 * @param bound The bound for the probability
 	 * @param pathFormula The child node
 	 */
-	BoundOperator(ComparisonType comparisonOperator, T bound, AbstractPathFormula<T>* pathFormula)
+	PathBoundOperator(ComparisonType comparisonOperator, T bound, AbstractPathFormula<T>* pathFormula)
 		: comparisonOperator(comparisonOperator), bound(bound), pathFormula(pathFormula) {
 		// Intentionally left empty
 	}
@@ -77,7 +77,7 @@ public:
 	 * The subtree is deleted with the object
 	 * (this behavior can be prevented by setting them to NULL before deletion)
 	 */
-	virtual ~BoundOperator() {
+	virtual ~PathBoundOperator() {
 	 if (pathFormula != nullptr) {
 		 delete pathFormula;
 	 }
@@ -173,7 +173,7 @@ public:
 	 * @returns A bit vector indicating all states that satisfy the formula represented by the called object.
 	 */
 	virtual storm::storage::BitVector *check(const storm::modelChecker::AbstractModelChecker<T>& modelChecker) const {
-		return modelChecker.template as<IBoundOperatorModelChecker>()->checkBoundOperator(*this);
+		return modelChecker.template as<IPathBoundOperatorModelChecker>()->checkPathBoundOperator(*this);
 	}
 	
 	/*!
@@ -196,4 +196,4 @@ private:
 
 } //namespace storm
 
-#endif /* STORM_FORMULA_BOUNDOPERATOR_H_ */
+#endif /* STORM_FORMULA_PATHBOUNDOPERATOR_H_ */
diff --git a/src/formula/ProbabilisticBoundOperator.h b/src/formula/ProbabilisticBoundOperator.h
index f679293d4..e9183950d 100644
--- a/src/formula/ProbabilisticBoundOperator.h
+++ b/src/formula/ProbabilisticBoundOperator.h
@@ -10,7 +10,7 @@
 
 #include "AbstractStateFormula.h"
 #include "AbstractPathFormula.h"
-#include "BoundOperator.h"
+#include "src/formula/PathBoundOperator.h"
 #include "utility/ConstTemplates.h"
 
 namespace storm {
@@ -38,14 +38,14 @@ namespace formula {
  * @see AbstractFormula
  */
 template<class T>
-class ProbabilisticBoundOperator : public BoundOperator<T> {
+class ProbabilisticBoundOperator : public PathBoundOperator<T> {
 
 public:
 	/*!
 	 * Empty constructor
 	 */
-	ProbabilisticBoundOperator() : BoundOperator<T>
-		(BoundOperator<T>::LESS_EQUAL, storm::utility::constGetZero<T>(), nullptr) {
+	ProbabilisticBoundOperator() : PathBoundOperator<T>
+		(PathBoundOperator<T>::LESS_EQUAL, storm::utility::constGetZero<T>(), nullptr) {
 		// Intentionally left empty
 	}
 
@@ -58,8 +58,8 @@ public:
 	 * @param pathFormula The child node
 	 */
 	ProbabilisticBoundOperator(
-			typename BoundOperator<T>::ComparisonType comparisonRelation, T bound, AbstractPathFormula<T>* pathFormula) :
-				BoundOperator<T>(comparisonRelation, bound, pathFormula) {
+			typename PathBoundOperator<T>::ComparisonType comparisonRelation, T bound, AbstractPathFormula<T>* pathFormula) :
+				PathBoundOperator<T>(comparisonRelation, bound, pathFormula) {
 		// Intentionally left empty
 	}
 
@@ -68,7 +68,7 @@ public:
 	 */
 	virtual std::string toString() const {
 		std::string result = "P ";
-		result += BoundOperator<T>::toString();
+		result += PathBoundOperator<T>::toString();
 		return result;
 	}
 
diff --git a/src/formula/ReachabilityReward.h b/src/formula/ReachabilityReward.h
index 54e2f447b..ad8171642 100644
--- a/src/formula/ReachabilityReward.h
+++ b/src/formula/ReachabilityReward.h
@@ -11,7 +11,7 @@
 #include "src/formula/AbstractPathFormula.h"
 #include "src/formula/AbstractStateFormula.h"
 #include "src/formula/AbstractFormulaChecker.h"
-#include "src/modelChecker/AbstractModelChecker.h"
+#include "src/modelchecker/AbstractModelChecker.h"
 
 namespace storm {
 namespace formula {
diff --git a/src/formula/RewardBoundOperator.h b/src/formula/RewardBoundOperator.h
index 611280483..3d08c6c95 100644
--- a/src/formula/RewardBoundOperator.h
+++ b/src/formula/RewardBoundOperator.h
@@ -10,7 +10,7 @@
 
 #include "AbstractStateFormula.h"
 #include "AbstractPathFormula.h"
-#include "BoundOperator.h"
+#include "PathBoundOperator.h"
 #include "utility/ConstTemplates.h"
 
 namespace storm {
@@ -37,13 +37,13 @@ namespace formula {
  * @see AbstractFormula
  */
 template<class T>
-class RewardBoundOperator : public BoundOperator<T> {
+class RewardBoundOperator : public PathBoundOperator<T> {
 
 public:
 	/*!
 	 * Empty constructor
 	 */
-	RewardBoundOperator() : BoundOperator<T>(BoundOperator<T>::LESS_EQUAL, storm::utility::constGetZero<T>(), nullptr) {
+	RewardBoundOperator() : PathBoundOperator<T>(PathBoundOperator<T>::LESS_EQUAL, storm::utility::constGetZero<T>(), nullptr) {
 		// Intentionally left empty
 	}
 
@@ -55,8 +55,8 @@ public:
 	 * @param pathFormula The child node
 	 */
 	RewardBoundOperator(
-			typename BoundOperator<T>::ComparisonType comparisonRelation, T bound, AbstractPathFormula<T>* pathFormula) :
-				BoundOperator<T>(comparisonRelation, bound, pathFormula) {
+			typename PathBoundOperator<T>::ComparisonType comparisonRelation, T bound, AbstractPathFormula<T>* pathFormula) :
+				PathBoundOperator<T>(comparisonRelation, bound, pathFormula) {
 		// Intentionally left empty
 	}
 
@@ -65,7 +65,7 @@ public:
 	 */
 	virtual std::string toString() const {
 		std::string result = "R ";
-		result += BoundOperator<T>::toString();
+		result += PathBoundOperator<T>::toString();
 		return result;
 	}
 
diff --git a/src/formula/StateBoundOperator.h b/src/formula/StateBoundOperator.h
new file mode 100644
index 000000000..05c213c07
--- /dev/null
+++ b/src/formula/StateBoundOperator.h
@@ -0,0 +1,197 @@
+/*
+ * BoundOperator.h
+ *
+ *  Created on: 27.12.2012
+ *      Author: Christian Dehnert
+ */
+
+#ifndef STORM_FORMULA_STATEBOUNDOPERATOR_H_
+#define STORM_FORMULA_STATEBOUNDOPERATOR_H_
+
+#include "src/formula/AbstractStateFormula.h"
+#include "src/formula/AbstractPathFormula.h"
+#include "src/formula/AbstractFormulaChecker.h"
+#include "src/modelChecker/AbstractModelChecker.h"
+#include "src/utility/ConstTemplates.h"
+
+namespace storm {
+namespace formula {
+
+template <class T> class StateBoundOperator;
+
+/*!
+ *  @brief Interface class for model checkers that support StateBoundOperator.
+ *   
+ *  All model checkers that support the formula class StateBoundOperator must inherit
+ *  this pure virtual class.
+ */
+template <class T>
+class IStateBoundOperatorModelChecker {
+    public:
+        virtual storm::storage::BitVector* checkStateBoundOperator(const StateBoundOperator<T>& obj) const = 0;
+};
+
+/*!
+ * @brief
+ * Class for a Abstract formula tree with a P (probablistic) operator node over a probability interval
+ * as root.
+ *
+ * Has one Abstract state formula as sub formula/tree.
+ *
+ * @par Semantics
+ * 	  The formula holds iff the probability that the state formula holds is inside the bounds
+ * 	  specified in this operator
+ *
+ * The subtree is seen as part of the object and deleted with it
+ * (this behavior can be prevented by setting them to NULL before deletion)
+ *
+ *
+ * @see AbstractStateFormula
+ * @see AbstractPathFormula
+ * @see ProbabilisticOperator
+ * @see ProbabilisticNoBoundsOperator
+ * @see AbstractFormula
+ */
+template<class T>
+class StateBoundOperator : public AbstractStateFormula<T> {
+
+public:
+	enum ComparisonType { LESS, LESS_EQUAL, GREATER, GREATER_EQUAL };
+
+	/*!
+	 * Constructor
+	 *
+	 * @param comparisonOperator The relation for the bound.
+	 * @param bound The bound for the probability
+	 * @param stateFormula The child node
+	 */
+	StateBoundOperator(ComparisonType comparisonOperator, T bound, AbstractStateFormula<T>* stateFormula)
+		: comparisonOperator(comparisonOperator), bound(bound), stateFormula(stateFormula) {
+		// Intentionally left empty
+	}
+
+	/*!
+	 * Destructor
+	 *
+	 * The subtree is deleted with the object
+	 * (this behavior can be prevented by setting them to NULL before deletion)
+	 */
+	virtual ~StateBoundOperator() {
+	 if (stateFormula != nullptr) {
+		 delete stateFormula;
+	 }
+	}
+
+	/*!
+	 * @returns the child node (representation of a Abstract state formula)
+	 */
+	const AbstractStateFormula<T>& getStateFormula () const {
+		return *stateFormula;
+	}
+
+	/*!
+	 * Sets the child node
+	 *
+	 * @param stateFormula the state formula that becomes the new child node
+	 */
+	void setStateFormula(AbstractStateFormula<T>* stateFormula) {
+		this->stateFormula = stateFormula;
+	}
+
+	/*!
+	 * @returns the comparison relation
+	 */
+	const ComparisonType getComparisonOperator() const {
+		return comparisonOperator;
+	}
+
+	void setComparisonOperator(ComparisonType comparisonOperator) {
+		this->comparisonOperator = comparisonOperator;
+	}
+
+	/*!
+	 * @returns the bound for the measure
+	 */
+	const T& getBound() const {
+		return bound;
+	}
+
+	/*!
+	 * Sets the interval in which the probability that the path formula holds may lie in.
+	 *
+	 * @param bound The bound for the measure
+	 */
+	void setBound(T bound) {
+		this->bound = bound;
+	}
+
+	/*!
+	 * @returns a string representation of the formula
+	 */
+	virtual std::string toString() const {
+		std::string result = "";
+		switch (comparisonOperator) {
+		case LESS: result += "< "; break;
+		case LESS_EQUAL: result += "<= "; break;
+		case GREATER: result += "> "; break;
+		case GREATER_EQUAL: result += ">= "; break;
+		}
+		result += std::to_string(bound);
+		result += " [";
+		result += stateFormula->toString();
+		result += "]";
+		return result;
+	}
+
+	bool meetsBound(T value) const {
+		switch (comparisonOperator) {
+		case LESS: return value < bound; break;
+		case LESS_EQUAL: return value <= bound; break;
+		case GREATER: return value > bound; break;
+		case GREATER_EQUAL: return value >= bound; break;
+		default: return false;
+		}
+	}
+
+	/*!
+	 * Clones the called object.
+	 *
+	 * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
+	 *
+	 * @returns a new AND-object that is identical the called object.
+	 */
+	virtual AbstractStateFormula<T>* clone() const = 0;
+
+	/*!
+	 * Calls the model checker to check this formula.
+	 * Needed to infer the correct type of formula class.
+	 *
+	 * @note This function should only be called in a generic check function of a model checker class. For other uses,
+	 *       the methods of the model checker should be used.
+	 *
+	 * @returns A bit vector indicating all states that satisfy the formula represented by the called object.
+	 */
+	virtual storm::storage::BitVector *check(const storm::modelChecker::AbstractModelChecker<T>& modelChecker) const {
+		return modelChecker.template as<IStateBoundOperatorModelChecker>()->checkStateBoundOperator(*this);
+	}
+	
+	/*!
+     *  @brief Checks if the subtree conforms to some logic.
+     * 
+     *  @param checker Formula checker object.
+     *  @return true iff the subtree conforms to some logic.
+     */
+	virtual bool conforms(const AbstractFormulaChecker<T>& checker) const {
+        return checker.conforms(this->stateFormula);
+    }
+
+private:
+	ComparisonType comparisonOperator;
+	T bound;
+	AbstractStateFormula<T>* stateFormula;
+};
+
+} //namespace formula
+} //namespace storm
+
+#endif /* STORM_FORMULA_STATEBOUNDOPERATOR_H_ */
diff --git a/src/formula/SteadyStateOperator.h b/src/formula/SteadyStateOperator.h
new file mode 100644
index 000000000..0c0543016
--- /dev/null
+++ b/src/formula/SteadyStateOperator.h
@@ -0,0 +1,161 @@
+/*
+ * SteadyState.h
+ *
+ *  Created on: 19.10.2012
+ *      Author: Thomas Heinemann
+ */
+
+#ifndef STORM_FORMULA_STEADYSTATEOPERATOR_H_
+#define STORM_FORMULA_STEADYSTATEOPERATOR_H_
+
+#include "AbstractPathFormula.h"
+#include "AbstractStateFormula.h"
+#include "BoundOperator.h"
+#include "src/formula/AbstractFormulaChecker.h"
+
+namespace storm {
+
+namespace formula {
+
+template <class T> class SteadyStateOperator;
+
+/*!
+ *  @brief Interface class for model checkers that support SteadyStateOperator.
+ *   
+ *  All model checkers that support the formula class SteadyStateOperator must inherit
+ *  this pure virtual class.
+ */
+template <class T>
+class ISteadyStateOperatorModelChecker {
+    public:
+		/*!
+         *  @brief Evaluates SteadyStateOperator formula within a model checker.
+         *
+         *  @param obj Formula object with subformulas.
+         *  @return Result of the formula for every node.
+         */
+        virtual storm::storage::BitVector* checkSteadyStateOperator(const SteadyStateOperator<T>& obj) const = 0;
+};
+
+/*!
+ * @brief
+ * Class for a Abstract (path) formula tree with a SteadyStateOperator node as root.
+ *
+ * Has two Abstract state formulas as sub formulas/trees.
+ *
+ * @par Semantics
+ * The formula holds iff \e child holds  SteadyStateOperator step, \e child holds
+ *
+ * The subtree is seen as part of the object and deleted with the object
+ * (this behavior can be prevented by setting them to NULL before deletion)
+ *
+ * @see AbstractPathFormula
+ * @see AbstractFormula
+ */
+template <class T>
+class SteadyStateOperator : public BoundOperator<T> {
+
+public:
+	/*!
+	 * Empty constructor
+	 */
+	SteadyStateOperator() : BoundOperator<T>
+		(BoundOperator<T>::LESS_EQUAL, storm::utility::constGetZero<T>(), nullptr) {
+		// Intentionally left empty
+	}
+
+	/*!
+	 * Constructor
+	 *
+	 * @param child The child node
+	 */
+	SteadyStateOperator(
+		BoundOperator<T>::ComparisonType comparisonRelation, T bound, AbstractStateFormula<T>* child) {
+		this->child = child;
+	}
+
+	/*!
+	 * Constructor.
+	 *
+	 * Also deletes the subtree.
+	 * (this behaviour can be prevented by setting the subtrees to NULL before deletion)
+	 */
+	virtual ~SteadyStateOperator() {
+	  if (child != NULL) {
+		  delete child;
+	  }
+	}
+
+	/*!
+	 * @returns the child node
+	 */
+	const AbstractStateFormula<T>& getChild() const {
+		return *child;
+	}
+
+	/*!
+	 * Sets the subtree
+	 * @param child the new child node
+	 */
+	void setChild(AbstractStateFormula<T>* child) {
+		this->child = child;
+	}
+
+	/*!
+	 * @returns a string representation of the formula
+	 */
+	virtual std::string toString() const {
+		std::string result = "(";
+		result += " S ";
+		result += child->toString();
+		result += ")";
+		return result;
+	}
+
+	/*!
+	 * Clones the called object.
+	 *
+	 * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
+	 *
+	 * @returns a new BoundedUntil-object that is identical the called object.
+	 */
+	virtual AbstractPathFormula<T>* clone() const {
+		SteadyStateOperator<T>* result = new SteadyStateOperator<T>();
+		if (child != NULL) {
+			result->setChild(child);
+		}
+		return result;
+	}
+
+	/*!
+	 * Calls the model checker to check this formula.
+	 * Needed to infer the correct type of formula class.
+	 *
+	 * @note This function should only be called in a generic check function of a model checker class. For other uses,
+	 *       the methods of the model checker should be used.
+	 *
+	 * @returns A vector indicating the probability that the formula holds for each state.
+	 */
+	virtual storm::storage::BitVector* check(const storm::modelChecker::AbstractModelChecker<T>& modelChecker) const {
+		return modelChecker.template as<ISteadyStateOperatorModelChecker>()->checkSteadyStateOperator(*this);
+	}
+	
+	/*!
+     *  @brief Checks if the subtree conforms to some logic.
+     * 
+     *  @param checker Formula checker object.
+     *  @return true iff the subtree conforms to some logic.
+     */
+	virtual bool conforms(const AbstractFormulaChecker<T>& checker) const {
+        return checker.conforms(this->child);
+    }
+
+private:
+	AbstractStateFormula<T>* child;
+};
+
+} //namespace formula
+
+} //namespace storm
+
+#endif /* STORM_FORMULA_STEADYSTATEOPERATOR_H_ */
diff --git a/src/modelChecker/AbstractModelChecker.h b/src/modelchecker/AbstractModelChecker.h
similarity index 100%
rename from src/modelChecker/AbstractModelChecker.h
rename to src/modelchecker/AbstractModelChecker.h
diff --git a/src/modelChecker/DtmcPrctlModelChecker.h b/src/modelchecker/DtmcPrctlModelChecker.h
similarity index 98%
rename from src/modelChecker/DtmcPrctlModelChecker.h
rename to src/modelchecker/DtmcPrctlModelChecker.h
index 77648de2a..cb9256f48 100644
--- a/src/modelChecker/DtmcPrctlModelChecker.h
+++ b/src/modelchecker/DtmcPrctlModelChecker.h
@@ -16,7 +16,7 @@
 #include "src/storage/BitVector.h"
 #include "src/exceptions/InvalidPropertyException.h"
 #include "src/utility/Vector.h"
-#include "src/modelChecker/AbstractModelChecker.h"
+#include "src/modelchecker/AbstractModelChecker.h"
 #include <vector>
 
 #include "log4cplus/logger.h"
@@ -222,7 +222,7 @@ public:
 	 * @param formula The state formula to check
 	 * @returns The set of states satisfying the formula, represented by a bit vector
 	 */
-	storm::storage::BitVector* checkBoundOperator(const storm::formula::BoundOperator<Type>& formula) const {
+	storm::storage::BitVector* checkPathBoundOperator(const storm::formula::PathBoundOperator<Type>& formula) const {
 		// First, we need to compute the probability for satisfying the path formula for each state.
 		std::vector<Type>* quantitativeResult = this->checkPathFormula(formula.getPathFormula());
 
diff --git a/src/modelChecker/EigenDtmcPrctlModelChecker.h b/src/modelchecker/EigenDtmcPrctlModelChecker.h
similarity index 99%
rename from src/modelChecker/EigenDtmcPrctlModelChecker.h
rename to src/modelchecker/EigenDtmcPrctlModelChecker.h
index 25bf4984b..a7b749129 100644
--- a/src/modelChecker/EigenDtmcPrctlModelChecker.h
+++ b/src/modelchecker/EigenDtmcPrctlModelChecker.h
@@ -11,7 +11,7 @@
 #include "src/utility/Vector.h"
 
 #include "src/models/Dtmc.h"
-#include "src/modelChecker/DtmcPrctlModelChecker.h"
+#include "src/modelchecker/DtmcPrctlModelChecker.h"
 #include "src/solver/GraphAnalyzer.h"
 #include "src/utility/ConstTemplates.h"
 #include "src/exceptions/NoConvergenceException.h"
diff --git a/src/modelChecker/ForwardDeclarations.h b/src/modelchecker/ForwardDeclarations.h
similarity index 100%
rename from src/modelChecker/ForwardDeclarations.h
rename to src/modelchecker/ForwardDeclarations.h
diff --git a/src/modelChecker/GmmxxDtmcPrctlModelChecker.h b/src/modelchecker/GmmxxDtmcPrctlModelChecker.h
similarity index 99%
rename from src/modelChecker/GmmxxDtmcPrctlModelChecker.h
rename to src/modelchecker/GmmxxDtmcPrctlModelChecker.h
index 0c54d63cf..009ecd678 100644
--- a/src/modelChecker/GmmxxDtmcPrctlModelChecker.h
+++ b/src/modelchecker/GmmxxDtmcPrctlModelChecker.h
@@ -11,7 +11,7 @@
 #include <cmath>
 
 #include "src/models/Dtmc.h"
-#include "src/modelChecker/DtmcPrctlModelChecker.h"
+#include "src/modelchecker/DtmcPrctlModelChecker.h"
 #include "src/solver/GraphAnalyzer.h"
 #include "src/utility/Vector.h"
 #include "src/utility/ConstTemplates.h"
diff --git a/src/parser/PrctlParser.cpp b/src/parser/PrctlParser.cpp
index 6f84aa89c..eb90d2550 100644
--- a/src/parser/PrctlParser.cpp
+++ b/src/parser/PrctlParser.cpp
@@ -51,23 +51,23 @@ struct PrctlParser::PrctlGrammar : qi::grammar<Iterator, storm::formula::Abstrac
 				phoenix::new_<storm::formula::Ap<double>>(qi::_1)];
 		probabilisticBoundOperator = (
 				(qi::lit("P") >> qi::lit(">") >> qi::double_ >> qi::lit("[") >> pathFormula >> qi::lit("]"))[qi::_val =
-						phoenix::new_<storm::formula::ProbabilisticBoundOperator<double> >(storm::formula::BoundOperator<double>::GREATER, qi::_1, qi::_2)] |
+						phoenix::new_<storm::formula::ProbabilisticBoundOperator<double> >(storm::formula::PathBoundOperator<double>::GREATER, qi::_1, qi::_2)] |
 				(qi::lit("P") >> qi::lit(">=") >> qi::double_ >> qi::lit("[") >> pathFormula >> qi::lit("]"))[qi::_val =
-						phoenix::new_<storm::formula::ProbabilisticBoundOperator<double> >(storm::formula::BoundOperator<double>::GREATER_EQUAL, qi::_1, qi::_2)] |
+						phoenix::new_<storm::formula::ProbabilisticBoundOperator<double> >(storm::formula::PathBoundOperator<double>::GREATER_EQUAL, qi::_1, qi::_2)] |
 				(qi::lit("P") >> qi::lit("<")  >> qi::double_ >> qi::lit("[") >> pathFormula >> qi::lit("]"))[qi::_val =
-								phoenix::new_<storm::formula::ProbabilisticBoundOperator<double> >(storm::formula::BoundOperator<double>::LESS, qi::_1, qi::_2)] |
+								phoenix::new_<storm::formula::ProbabilisticBoundOperator<double> >(storm::formula::PathBoundOperator<double>::LESS, qi::_1, qi::_2)] |
 				(qi::lit("P") >> qi::lit("<=") >> qi::double_ >> qi::lit("[") >> pathFormula >> qi::lit("]"))[qi::_val =
-						phoenix::new_<storm::formula::ProbabilisticBoundOperator<double> >(storm::formula::BoundOperator<double>::LESS_EQUAL, qi::_1, qi::_2)]
+						phoenix::new_<storm::formula::ProbabilisticBoundOperator<double> >(storm::formula::PathBoundOperator<double>::LESS_EQUAL, qi::_1, qi::_2)]
 				);
 		rewardBoundOperator = (
 				(qi::lit("R") >> qi::lit(">") >> qi::double_ >> qi::lit("[") >> pathFormula >> qi::lit("]"))[qi::_val =
-						phoenix::new_<storm::formula::RewardBoundOperator<double> >(storm::formula::BoundOperator<double>::GREATER, qi::_1, qi::_2)] |
+						phoenix::new_<storm::formula::RewardBoundOperator<double> >(storm::formula::PathBoundOperator<double>::GREATER, qi::_1, qi::_2)] |
 				(qi::lit("R") >> qi::lit(">=") >> qi::double_ >> qi::lit("[") >> pathFormula >> qi::lit("]"))[qi::_val =
-								phoenix::new_<storm::formula::RewardBoundOperator<double> >(storm::formula::BoundOperator<double>::GREATER_EQUAL, qi::_1, qi::_2)] |
+								phoenix::new_<storm::formula::RewardBoundOperator<double> >(storm::formula::PathBoundOperator<double>::GREATER_EQUAL, qi::_1, qi::_2)] |
 				(qi::lit("R") >> qi::lit("<") >> qi::double_ >> qi::lit("[") >> pathFormula >> qi::lit("]"))[qi::_val =
-										phoenix::new_<storm::formula::RewardBoundOperator<double> >(storm::formula::BoundOperator<double>::LESS, qi::_1, qi::_2)] |
+										phoenix::new_<storm::formula::RewardBoundOperator<double> >(storm::formula::PathBoundOperator<double>::LESS, qi::_1, qi::_2)] |
 				(qi::lit("R") >> qi::lit("<=")>> qi::double_ >> qi::lit("[") >> pathFormula >> qi::lit("]"))[qi::_val =
-						phoenix::new_<storm::formula::RewardBoundOperator<double> >(storm::formula::BoundOperator<double>::LESS_EQUAL, qi::_1, qi::_2)]
+						phoenix::new_<storm::formula::RewardBoundOperator<double> >(storm::formula::PathBoundOperator<double>::LESS_EQUAL, qi::_1, qi::_2)]
 				);
 
 		//This block defines rules for parsing formulas with noBoundOperators
diff --git a/src/storm.cpp b/src/storm.cpp
index 9d2fff6d7..2015e85e4 100644
--- a/src/storm.cpp
+++ b/src/storm.cpp
@@ -22,8 +22,8 @@
 #include "src/models/Dtmc.h"
 #include "src/storage/SparseMatrix.h"
 #include "src/models/AtomicPropositionsLabeling.h"
-#include "src/modelChecker/EigenDtmcPrctlModelChecker.h"
-#include "src/modelChecker/GmmxxDtmcPrctlModelChecker.h"
+#include "src/modelchecker/EigenDtmcPrctlModelChecker.h"
+#include "src/modelchecker/GmmxxDtmcPrctlModelChecker.h"
 #include "src/parser/AutoParser.h"
 #include "src/parser/PrctlParser.h"
 #include "src/solver/GraphAnalyzer.h"
diff --git a/test/parser/PrctlParserTest.cpp b/test/parser/PrctlParserTest.cpp
index 5a2dd3cf2..7a2957344 100644
--- a/test/parser/PrctlParserTest.cpp
+++ b/test/parser/PrctlParserTest.cpp
@@ -53,7 +53,7 @@ TEST(PrctlParserTest, parseProbabilisticFormulaTest) {
 
 	storm::formula::ProbabilisticBoundOperator<double>* op = static_cast<storm::formula::ProbabilisticBoundOperator<double>*>(prctlFileParser->getFormula());
 
-	ASSERT_EQ(storm::formula::BoundOperator<double>::GREATER, op->getComparisonOperator());
+	ASSERT_EQ(storm::formula::PathBoundOperator<double>::GREATER, op->getComparisonOperator());
 	ASSERT_EQ(0.5, op->getBound());
 
 	ASSERT_EQ(prctlFileParser->getFormula()->toString(), "P > 0.500000 [F a]");
@@ -73,7 +73,7 @@ TEST(PrctlParserTest, parseRewardFormulaTest) {
 
 	storm::formula::RewardBoundOperator<double>* op = static_cast<storm::formula::RewardBoundOperator<double>*>(prctlFileParser->getFormula());
 
-	ASSERT_EQ(storm::formula::BoundOperator<double>::GREATER_EQUAL, op->getComparisonOperator());
+	ASSERT_EQ(storm::formula::PathBoundOperator<double>::GREATER_EQUAL, op->getComparisonOperator());
 	ASSERT_EQ(15.0, op->getBound());
 
 	ASSERT_EQ(prctlFileParser->getFormula()->toString(), "R >= 15.000000 [(a U !b)]");
diff --git a/test/parser/output.dot b/test/parser/output.dot
new file mode 100644
index 000000000..7e0e80061
--- /dev/null
+++ b/test/parser/output.dot
@@ -0,0 +1,35 @@
+digraph dtmc {
+	1[label="1\n{ phi }"];
+	2[label="2\n{ phi }"];
+	3[label="3\n{ phi }"];
+	4[label="4\n{ smth }"];
+	5[label="5\n{ phi,smth }"];
+	6[label="6\n{ psi }"];
+	7[label="7\n{ phi,psi }"];
+	8[label="8\n{ phi,psi }"];
+	9[label="9\n{ phi }"];
+	10[label="10\n{ phi }"];
+	11[label="11\n{ phi }"];
+	0 -> 0 [label=1]
+	1 -> 3 [label=0.5]
+	1 -> 4 [label=0.5]
+	2 -> 1 [label=0.3]
+	2 -> 7 [label=0.7]
+	3 -> 2 [label=0.05]
+	3 -> 3 [label=0.7]
+	3 -> 6 [label=0.05]
+	3 -> 8 [label=0.2]
+	4 -> 1 [label=0.3]
+	4 -> 5 [label=0.3]
+	4 -> 6 [label=0.4]
+	5 -> 4 [label=1]
+	6 -> 7 [label=1]
+	7 -> 2 [label=0.2]
+	7 -> 6 [label=0.8]
+	8 -> 9 [label=1]
+	9 -> 8 [label=0.3]
+	9 -> 9 [label=0.7]
+	10 -> 4 [label=1]
+	11 -> 5 [label=0.7]
+	11 -> 9 [label=0.3]
+}
diff --git a/test/storm-tests.cpp b/test/storm-tests.cpp
index 9165b68a8..0fdcbb456 100644
--- a/test/storm-tests.cpp
+++ b/test/storm-tests.cpp
@@ -7,7 +7,7 @@
 #include "log4cplus/fileappender.h"
 
 #include "src/utility/Settings.h"
-#include "src/modelChecker/GmmxxDtmcPrctlModelChecker.h"
+#include "src/modelchecker/GmmxxDtmcPrctlModelChecker.h"
 
 log4cplus::Logger logger;