diff --git a/src/formula/AP.h b/src/formula/AP.h
index 3fa19a202..4b7d18011 100644
--- a/src/formula/AP.h
+++ b/src/formula/AP.h
@@ -59,7 +59,7 @@ public:
 	/*!
 	 * @returns the name of the atomic proposition
 	 */
-	const std::string& getAP() {
+	const std::string& getAP() const {
 		return ap;
 	}
 
@@ -67,7 +67,7 @@ public:
 	 * @returns a string representation of the leaf.
 	 *
 	 */
-	virtual std::string toString() {
+	virtual std::string toString() const {
 		return getAP();
 	}
 
@@ -76,7 +76,7 @@ public:
 	 *
 	 * @returns a new AP-object that is identical the called object.
 	 */
-	virtual PCTLStateFormula<T>* clone() {
+	virtual PCTLStateFormula<T>* clone() const {
 	  return new AP(ap);
 	}
 
@@ -89,7 +89,7 @@ public:
 	 *
 	 * @returns A bit vector indicating all states that satisfy the formula represented by the called object.
 	 */
-	virtual mrmc::storage::BitVector *check(mrmc::modelChecker::DtmcPrctlModelChecker<T>& modelChecker) {
+	virtual mrmc::storage::BitVector *check(const mrmc::modelChecker::DtmcPrctlModelChecker<T>& modelChecker) const {
 	  return modelChecker.checkAP(this);
 	}
 
diff --git a/src/formula/And.h b/src/formula/And.h
index de6821b8d..742633f3b 100644
--- a/src/formula/And.h
+++ b/src/formula/And.h
@@ -91,21 +91,21 @@ public:
 	/*!
 	 * @returns a pointer to the left child node
 	 */
-	PCTLStateFormula<T>& getLeft() {
+	const PCTLStateFormula<T>& getLeft() const {
 		return *left;
 	}
 
 	/*!
 	 * @returns a pointer to the right child node
 	 */
-	PCTLStateFormula<T>& getRight() {
+	const PCTLStateFormula<T>& getRight() const {
 		return *right;
 	}
 
 	/*!
 	 * @returns a string representation of the formula
 	 */
-	virtual std::string toString() {
+	virtual std::string toString() const {
 		std::string result = "(";
 		result += left->toString();
 		result += " && ";
@@ -121,7 +121,7 @@ public:
 	 *
 	 * @returns a new AND-object that is identical the called object.
 	 */
-	virtual PCTLStateFormula<T>* clone() {
+	virtual PCTLStateFormula<T>* clone() const {
 		And<T>* result = new And();
 		if (this->left != NULL) {
 		  result->setLeft(left->clone());
@@ -141,7 +141,7 @@ public:
 	 *
 	 * @returns A bit vector indicating all states that satisfy the formula represented by the called object.
 	 */
-	virtual mrmc::storage::BitVector *check(mrmc::modelChecker::DtmcPrctlModelChecker<T>& modelChecker) {
+	virtual mrmc::storage::BitVector *check(const mrmc::modelChecker::DtmcPrctlModelChecker<T>& modelChecker) const {
 		return modelChecker.checkAnd(this);
 	}
 
diff --git a/src/formula/BoundedUntil.h b/src/formula/BoundedUntil.h
index f6c6b6d93..93355b7f3 100644
--- a/src/formula/BoundedUntil.h
+++ b/src/formula/BoundedUntil.h
@@ -97,21 +97,21 @@ public:
 	/*!
 	 * @returns a pointer to the left child node
 	 */
-	PCTLStateFormula<T>& getLeft() {
+	const PCTLStateFormula<T>& getLeft() const {
 		return *left;
 	}
 
 	/*!
 	 * @returns a pointer to the right child node
 	 */
-	PCTLStateFormula<T>& getRight() {
+	const PCTLStateFormula<T>& getRight() const {
 		return *right;
 	}
 
 	/*!
 	 * @returns the maximally allowed number of steps for the bounded until operator
 	 */
-	uint_fast64_t getBound() {
+	uint_fast64_t getBound() const {
 		return bound;
 	}
 
@@ -127,7 +127,7 @@ public:
 	/*!
 	 * @returns a string representation of the formula
 	 */
-	virtual std::string toString() {
+	virtual std::string toString() const {
 		std::string result = "(";
 		result += left->toString();
 		result += " U<=";
@@ -145,7 +145,7 @@ public:
 	 *
 	 * @returns a new BoundedUntil-object that is identical the called object.
 	 */
-	virtual PCTLPathFormula<T>* clone() {
+	virtual PCTLPathFormula<T>* clone() const {
 		BoundedUntil<T>* result = new BoundedUntil();
 		result->setBound(bound);
 		if (left != NULL) {
@@ -167,7 +167,7 @@ public:
 	 *
 	 * @returns A vector indicating the probability that the formula holds for each state.
 	 */
-	virtual std::vector<T> *check(mrmc::modelChecker::DtmcPrctlModelChecker<T>& modelChecker) {
+	virtual std::vector<T> *check(const mrmc::modelChecker::DtmcPrctlModelChecker<T>& modelChecker) const {
 	  return modelChecker.checkBoundedUntil(this);
 	}
 
diff --git a/src/formula/Next.h b/src/formula/Next.h
index d1647fee3..1a5acb1ec 100644
--- a/src/formula/Next.h
+++ b/src/formula/Next.h
@@ -65,7 +65,7 @@ public:
 	/*!
 	 * @returns the child node
 	 */
-	PCTLStateFormula<T>& getChild() {
+	const PCTLStateFormula<T>& getChild() const {
 		return *child;
 	}
 
@@ -80,7 +80,7 @@ public:
 	/*!
 	 * @returns a string representation of the formula
 	 */
-	virtual std::string toString() {
+	virtual std::string toString() const {
 		std::string result = "(";
 		result += " X ";
 		result += child->toString();
@@ -95,7 +95,7 @@ public:
 	 *
 	 * @returns a new BoundedUntil-object that is identical the called object.
 	 */
-	virtual PCTLPathFormula<T>* clone() {
+	virtual PCTLPathFormula<T>* clone() const {
 		Next<T>* result = new Next<T>();
 		if (child != NULL) {
 			result->setChild(child);
@@ -112,7 +112,7 @@ public:
 	 *
 	 * @returns A vector indicating the probability that the formula holds for each state.
 	 */
-	virtual std::vector<T> *check(mrmc::modelChecker::DtmcPrctlModelChecker<T>& modelChecker) {
+	virtual std::vector<T> *check(const mrmc::modelChecker::DtmcPrctlModelChecker<T>& modelChecker) const {
 	  return modelChecker.checkNext(this);
 	}
 
diff --git a/src/formula/Not.h b/src/formula/Not.h
index 835c8844b..c816a827b 100644
--- a/src/formula/Not.h
+++ b/src/formula/Not.h
@@ -60,7 +60,7 @@ public:
 	/*!
 	 * @returns The child node
 	 */
-	PCTLStateFormula<T>& getChild() {
+	const PCTLStateFormula<T>& getChild() const {
 		return *child;
 	}
 
@@ -75,7 +75,7 @@ public:
 	/*!
 	 * @returns a string representation of the formula
 	 */
-	virtual std::string toString() {
+	virtual std::string toString() const {
 		std::string result = "!";
 		result += child->toString();
 		return result;
@@ -88,7 +88,7 @@ public:
 	 *
 	 * @returns a new AND-object that is identical the called object.
 	 */
-	virtual PCTLStateFormula<T>* clone() {
+	virtual PCTLStateFormula<T>* clone() const {
 		Not<T>* result = new Not<T>();
 		if (child != NULL) {
 			result->setChild(child);
@@ -105,7 +105,7 @@ public:
 	 *
 	 * @returns A bit vector indicating all states that satisfy the formula represented by the called object.
 	 */
-	virtual mrmc::storage::BitVector *check(mrmc::modelChecker::DtmcPrctlModelChecker<T>& modelChecker) {
+	virtual mrmc::storage::BitVector *check(const mrmc::modelChecker::DtmcPrctlModelChecker<T>& modelChecker) const {
 	  return modelChecker.checkNot(this);
 	}
 
diff --git a/src/formula/Or.h b/src/formula/Or.h
index a1e563e4f..78185b0d5 100644
--- a/src/formula/Or.h
+++ b/src/formula/Or.h
@@ -90,21 +90,21 @@ public:
 	/*!
 	 * @returns a pointer to the left child node
 	 */
-	PCTLStateFormula<T>& getLeft() {
+	const PCTLStateFormula<T>& getLeft() const {
 		return *left;
 	}
 
 	/*!
 	 * @returns a pointer to the right child node
 	 */
-	PCTLStateFormula<T>& getRight() {
+	const PCTLStateFormula<T>& getRight() const {
 		return *right;
 	}
 
 	/*!
 	 * @returns a string representation of the formula
 	 */
-	virtual std::string toString() {
+	virtual std::string toString() const {
 		std::string result = "(";
 		result += left->toString();
 		result += " || ";
@@ -120,7 +120,7 @@ public:
 	 *
 	 * @returns a new AND-object that is identical the called object.
 	 */
-	virtual PCTLStateFormula<T>* clone() {
+	virtual PCTLStateFormula<T>* clone() const {
 		Or<T>* result = new Or();
 		if (this->left != NULL) {
 		  result->setLeft(left->clone());
@@ -140,7 +140,7 @@ public:
 	 *
 	 * @returns A bit vector indicating all states that satisfy the formula represented by the called object.
 	 */
-	virtual mrmc::storage::BitVector *check(mrmc::modelChecker::DtmcPrctlModelChecker<T>& modelChecker) {
+	virtual mrmc::storage::BitVector *check(const mrmc::modelChecker::DtmcPrctlModelChecker<T>& modelChecker) const {
 	  return modelChecker.checkOr(this);
 	}
 
diff --git a/src/formula/PCTLPathFormula.h b/src/formula/PCTLPathFormula.h
index 86812c902..a70a35f53 100644
--- a/src/formula/PCTLPathFormula.h
+++ b/src/formula/PCTLPathFormula.h
@@ -42,7 +42,7 @@ public:
 	 * @note This function is not implemented in this class.
 	 * @returns a new AND-object that is identical the called object.
 	 */
-	virtual PCTLPathFormula<T>* clone() = 0;
+	virtual PCTLPathFormula<T>* clone() const = 0;
 
 	/*!
 	 * Calls the model checker to check this formula.
@@ -55,7 +55,7 @@ public:
 	 *
 	 * @returns A vector indicating the probability that the formula holds for each state.
 	 */
-	virtual std::vector<T>* check(mrmc::modelChecker::DtmcPrctlModelChecker<T>& modelChecker) = 0;
+	virtual std::vector<T>* check(const mrmc::modelChecker::DtmcPrctlModelChecker<T>& modelChecker) const = 0;
 };
 
 } //namespace formula
diff --git a/src/formula/PCTLStateFormula.h b/src/formula/PCTLStateFormula.h
index ac7c458eb..a8ca831c3 100644
--- a/src/formula/PCTLStateFormula.h
+++ b/src/formula/PCTLStateFormula.h
@@ -42,7 +42,7 @@ public:
 	 * @note This function is not implemented in this class.
 	 * @returns a new AND-object that is identical the called object.
 	 */
-	virtual PCTLStateFormula<T>* clone() = 0;
+	virtual PCTLStateFormula<T>* clone() const = 0;
 
 	/*!
 	 * Calls the model checker to check this formula.
@@ -55,7 +55,7 @@ public:
 	 *
 	 * @returns A bit vector indicating all states that satisfy the formula represented by the called object.
 	 */
-	virtual mrmc::storage::BitVector *check(mrmc::modelChecker::DtmcPrctlModelChecker<T>& modelChecker) = 0;
+	virtual mrmc::storage::BitVector *check(const mrmc::modelChecker::DtmcPrctlModelChecker<T>& modelChecker) const = 0;
 };
 
 } //namespace formula
diff --git a/src/formula/PCTLformula.h b/src/formula/PCTLformula.h
index b1e7bf0b9..add5c5198 100644
--- a/src/formula/PCTLformula.h
+++ b/src/formula/PCTLformula.h
@@ -38,7 +38,7 @@ public:
 	 * @note This function is not implemented in this class.
 	 * @returns a string representation of the formula
 	 */
-	virtual std::string toString() = 0;
+	virtual std::string toString() const = 0;
 };
 
 } //namespace formula
diff --git a/src/formula/ProbabilisticOperator.h b/src/formula/ProbabilisticOperator.h
index e974feaaf..49e6530de 100644
--- a/src/formula/ProbabilisticOperator.h
+++ b/src/formula/ProbabilisticOperator.h
@@ -73,21 +73,21 @@ public:
 	/*!
 	 * @returns the child node (representation of a PCTL path formula)
 	 */
-	PCTLPathFormula<T>& getPathFormula () {
+	const PCTLPathFormula<T>& getPathFormula () const {
 		return *pathFormula;
 	}
 
 	/*!
 	 * @returns the lower bound for the probability
 	 */
-	const T& getLowerBound() {
+	const T& getLowerBound() const {
 		return lower;
 	}
 
 	/*!
 	 * @returns the upper bound for the probability
 	 */
-	const T& getUpperBound() {
+	const T& getUpperBound() const {
 		return upper;
 	}
 
@@ -114,7 +114,7 @@ public:
 	/*!
 	 * @returns a string representation of the formula
 	 */
-	virtual std::string toString() {
+	virtual std::string toString() const {
 		std::string result = "(";
 		result += " P[";
 		result += lower;
@@ -133,7 +133,7 @@ public:
 	 *
 	 * @returns a new AND-object that is identical the called object.
 	 */
-	virtual PCTLStateFormula<T>* clone() {
+	virtual PCTLStateFormula<T>* clone() const {
 		ProbabilisticOperator<T>* result = new ProbabilisticOperator<T>();
 		result->setInterval(lower, upper);
 		if (pathFormula != NULL) {
@@ -151,7 +151,7 @@ public:
 	 *
 	 * @returns A bit vector indicating all states that satisfy the formula represented by the called object.
 	 */
-	virtual mrmc::storage::BitVector *check(mrmc::modelChecker::DtmcPrctlModelChecker<T>& modelChecker) {
+	virtual mrmc::storage::BitVector *check(const mrmc::modelChecker::DtmcPrctlModelChecker<T>& modelChecker) const {
 	  return modelChecker.checkProbabilisticOperator(this);
 	}
 
diff --git a/src/formula/Until.h b/src/formula/Until.h
index 86de81728..f6bf62a98 100644
--- a/src/formula/Until.h
+++ b/src/formula/Until.h
@@ -90,21 +90,21 @@ public:
 	/*!
 	 * @returns a pointer to the left child node
 	 */
-	PCTLStateFormula<T>& getLeft() {
+	const PCTLStateFormula<T>& getLeft() const {
 		return *left;
 	}
 
 	/*!
 	 * @returns a pointer to the right child node
 	 */
-	PCTLStateFormula<T>& getRight() {
+	const PCTLStateFormula<T>& getRight() const {
 		return *right;
 	}
 
 	/*!
 	 * @returns a string representation of the formula
 	 */
-	virtual std::string toString() {
+	virtual std::string toString() const {
 		std::string result = "(";
 		result += left->toString();
 		result += " U ";
@@ -120,7 +120,7 @@ public:
 	 *
 	 * @returns a new BoundedUntil-object that is identical the called object.
 	 */
-	virtual PCTLPathFormula<T>* clone() {
+	virtual PCTLPathFormula<T>* clone() const {
 		Until<T>* result = new Until();
 		if (left != NULL) {
 			result->setLeft(left->clone());
@@ -140,7 +140,7 @@ public:
 	 *
 	 * @returns A vector indicating the probability that the formula holds for each state.
 	 */
-	virtual std::vector<T> *check(mrmc::modelChecker::DtmcPrctlModelChecker<T>& modelChecker) {
+	virtual std::vector<T> *check(const mrmc::modelChecker::DtmcPrctlModelChecker<T>& modelChecker) const {
 	  return modelChecker.checkUntil(this);
 	}