diff --git a/src/formula/And.h b/src/formula/And.h
index 910e23e8f..62cc46964 100644
--- a/src/formula/And.h
+++ b/src/formula/And.h
@@ -8,7 +8,7 @@
 #ifndef MRMC_FORMULA_AND_H_
 #define MRMC_FORMULA_AND_H_
 
-#include "PCTLStateFormula.h"
+#include "PctlStateFormula.h"
 #include <string>
 
 namespace mrmc {
@@ -27,11 +27,11 @@ namespace formula {
  * The subtrees are seen as part of the object and deleted with the object
  * (this behavior can be prevented by setting them to NULL before deletion)
  *
- * @see PCTLStateFormula
- * @see PCTLFormula
+ * @see PctlStateFormula
+ * @see PctlFormula
  */
 template <class T>
-class And : public PCTLStateFormula<T> {
+class And : public PctlStateFormula<T> {
 
 public:
 	/*!
@@ -50,7 +50,7 @@ public:
 	 * @param left The left sub formula
 	 * @param right The right sub formula
 	 */
-	And(PCTLStateFormula<T>* left, PCTLStateFormula<T>* right) {
+	And(PctlStateFormula<T>* left, PctlStateFormula<T>* right) {
 		this->left = left;
 		this->right = right;
 	}
@@ -75,7 +75,7 @@ public:
 	 *
 	 * @param newLeft the new left child.
 	 */
-	void setLeft(PCTLStateFormula<T>* newLeft) {
+	void setLeft(PctlStateFormula<T>* newLeft) {
 		left = newLeft;
 	}
 
@@ -84,21 +84,21 @@ public:
 	 *
 	 * @param newRight the new right child.
 	 */
-	void setRight(PCTLStateFormula<T>* newRight) {
+	void setRight(PctlStateFormula<T>* newRight) {
 		right = newRight;
 	}
 
 	/*!
 	 * @returns a pointer to the left child node
 	 */
-	const PCTLStateFormula<T>& getLeft() const {
+	const PctlStateFormula<T>& getLeft() const {
 		return *left;
 	}
 
 	/*!
 	 * @returns a pointer to the right child node
 	 */
-	const PCTLStateFormula<T>& getRight() const {
+	const PctlStateFormula<T>& getRight() const {
 		return *right;
 	}
 
@@ -121,7 +121,7 @@ public:
 	 *
 	 * @returns a new AND-object that is identical the called object.
 	 */
-	virtual PCTLStateFormula<T>* clone() const {
+	virtual PctlStateFormula<T>* clone() const {
 		And<T>* result = new And();
 		if (this->left != NULL) {
 		  result->setLeft(left->clone());
@@ -146,8 +146,8 @@ public:
 	}
 
 private:
-	PCTLStateFormula<T>* left;
-	PCTLStateFormula<T>* right;
+	PctlStateFormula<T>* left;
+	PctlStateFormula<T>* right;
 };
 
 } //namespace formula
diff --git a/src/formula/AP.h b/src/formula/Ap.h
similarity index 75%
rename from src/formula/AP.h
rename to src/formula/Ap.h
index 05f200c2c..1f636d7df 100644
--- a/src/formula/AP.h
+++ b/src/formula/Ap.h
@@ -1,5 +1,5 @@
 /*
- * AP.h
+ * Ap.h
  *
  *  Created on: 19.10.2012
  *      Author: Thomas Heinemann
@@ -8,7 +8,7 @@
 #ifndef MRMC_FORMULA_AP_H_
 #define MRMC_FORMULA_AP_H_
 
-#include "PCTLStateFormula.h"
+#include "PctlStateFormula.h"
 
 namespace mrmc {
 
@@ -20,21 +20,21 @@ namespace formula {
  *
  * This class represents the leaves in the formula tree.
  *
- * @see PCTLStateFormula
- * @see PCTLFormula
+ * @see PctlStateFormula
+ * @see PctlFormula
  */
 template <class T>
-class AP : public PCTLStateFormula<T> {
+class Ap : public PctlStateFormula<T> {
 
 public:
 	/*!
 	 * Constructor
 	 *
-	 * Creates a new atomic proposition leaf, with the label AP
+	 * Creates a new atomic proposition leaf, with the label Ap
 	 *
 	 * @param ap The string representing the atomic proposition
 	 */
-	AP(std::string ap) {
+	Ap(std::string ap) {
 		this->ap = ap;
 	}
 
@@ -42,12 +42,12 @@ public:
 	 * Destructor.
 	 * At this time, empty...
 	 */
-	virtual ~AP() { }
+	virtual ~Ap() { }
 
 	/*!
 	 * @returns the name of the atomic proposition
 	 */
-	const std::string& getAP() const {
+	const std::string& getAp() const {
 		return ap;
 	}
 
@@ -56,16 +56,16 @@ public:
 	 *
 	 */
 	virtual std::string toString() const {
-		return getAP();
+		return getAp();
 	}
 
 	/*!
 	 * Clones the called object.
 	 *
-	 * @returns a new AP-object that is identical the called object.
+	 * @returns a new Ap-object that is identical the called object.
 	 */
-	virtual PCTLStateFormula<T>* clone() const {
-	  return new AP(ap);
+	virtual PctlStateFormula<T>* clone() const {
+	  return new Ap(ap);
 	}
 
 	/*!
@@ -78,7 +78,7 @@ public:
 	 * @returns A bit vector indicating all states that satisfy the formula represented by the called object.
 	 */
 	virtual mrmc::storage::BitVector *check(const mrmc::modelChecker::DtmcPrctlModelChecker<T>& modelChecker) const {
-	  return modelChecker.checkAP(*this);
+	  return modelChecker.checkAp(*this);
 	}
 
 private:
diff --git a/src/formula/BoundedUntil.h b/src/formula/BoundedUntil.h
index edc447375..281c112bc 100644
--- a/src/formula/BoundedUntil.h
+++ b/src/formula/BoundedUntil.h
@@ -8,8 +8,8 @@
 #ifndef MRMC_FORMULA_BOUNDEDUNTIL_H_
 #define MRMC_FORMULA_BOUNDEDUNTIL_H_
 
-#include "PCTLPathFormula.h"
-#include "PCTLStateFormula.h"
+#include "PctlPathFormula.h"
+#include "PctlStateFormula.h"
 #include "boost/integer/integer_mask.hpp"
 #include <string>
 
@@ -30,11 +30,11 @@ namespace formula {
  * The subtrees are seen as part of the object and deleted with the object
  * (this behavior can be prevented by setting them to NULL before deletion)
  *
- * @see PCTLPathFormula
- * @see PCTLFormula
+ * @see PctlPathFormula
+ * @see PctlFormula
  */
 template <class T>
-class BoundedUntil : public PCTLPathFormula<T> {
+class BoundedUntil : public PctlPathFormula<T> {
 
 public:
 	/*!
@@ -53,7 +53,7 @@ public:
 	 * @param right The left formula subtree
 	 * @param bound The maximal number of steps
 	 */
-	BoundedUntil(PCTLStateFormula<T>* left, PCTLStateFormula<T>* right,
+	BoundedUntil(PctlStateFormula<T>* left, PctlStateFormula<T>* right,
 					 uint_fast64_t bound) {
 		this->left = left;
 		this->right = right;;
@@ -80,7 +80,7 @@ public:
 	 *
 	 * @param newLeft the new left child.
 	 */
-	void setLeft(PCTLStateFormula<T>* newLeft) {
+	void setLeft(PctlStateFormula<T>* newLeft) {
 		left = newLeft;
 	}
 
@@ -89,21 +89,21 @@ public:
 	 *
 	 * @param newRight the new right child.
 	 */
-	void setRight(PCTLStateFormula<T>* newRight) {
+	void setRight(PctlStateFormula<T>* newRight) {
 		right = newRight;
 	}
 
 	/*!
 	 * @returns a pointer to the left child node
 	 */
-	const PCTLStateFormula<T>& getLeft() const {
+	const PctlStateFormula<T>& getLeft() const {
 		return *left;
 	}
 
 	/*!
 	 * @returns a pointer to the right child node
 	 */
-	const PCTLStateFormula<T>& getRight() const {
+	const PctlStateFormula<T>& getRight() const {
 		return *right;
 	}
 
@@ -144,7 +144,7 @@ public:
 	 *
 	 * @returns a new BoundedUntil-object that is identical the called object.
 	 */
-	virtual PCTLPathFormula<T>* clone() const {
+	virtual PctlPathFormula<T>* clone() const {
 		BoundedUntil<T>* result = new BoundedUntil();
 		result->setBound(bound);
 		if (left != NULL) {
@@ -171,8 +171,8 @@ public:
 	}
 
 private:
-	PCTLStateFormula<T>* left;
-	PCTLStateFormula<T>* right;
+	PctlStateFormula<T>* left;
+	PctlStateFormula<T>* right;
 	uint_fast64_t bound;
 };
 
diff --git a/src/formula/Formulas.h b/src/formula/Formulas.h
index cd2370a24..8db8c1f0d 100644
--- a/src/formula/Formulas.h
+++ b/src/formula/Formulas.h
@@ -9,14 +9,14 @@
 #define MRMC_FORMULA_FORMULAS_H_
 
 #include "And.h"
-#include "AP.h"
+#include "Ap.h"
 #include "BoundedUntil.h"
 #include "Next.h"
 #include "Not.h"
 #include "Or.h"
-#include "PCTLformula.h"
-#include "PCTLPathFormula.h"
-#include "PCTLStateFormula.h"
+#include "PctlFormula.h"
+#include "PctlPathFormula.h"
+#include "PctlStateFormula.h"
 #include "ProbabilisticOperator.h"
 #include "ProbabilisticNoBoundsOperator.h"
 #include "ProbabilisticIntervalOperator.h"
diff --git a/src/formula/Next.h b/src/formula/Next.h
index 3ffa8451d..07924846e 100644
--- a/src/formula/Next.h
+++ b/src/formula/Next.h
@@ -8,8 +8,8 @@
 #ifndef MRMC_FORMULA_NEXT_H_
 #define MRMC_FORMULA_NEXT_H_
 
-#include "PCTLPathFormula.h"
-#include "PCTLStateFormula.h"
+#include "PctlPathFormula.h"
+#include "PctlStateFormula.h"
 
 namespace mrmc {
 
@@ -27,11 +27,11 @@ namespace formula {
  * 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 PCTLPathFormula
- * @see PCTLFormula
+ * @see PctlPathFormula
+ * @see PctlFormula
  */
 template <class T>
-class Next : public PCTLPathFormula<T> {
+class Next : public PctlPathFormula<T> {
 
 public:
 	/*!
@@ -46,7 +46,7 @@ public:
 	 *
 	 * @param child The child node
 	 */
-	Next(PCTLStateFormula<T>* child) {
+	Next(PctlStateFormula<T>* child) {
 		this->child = child;
 	}
 
@@ -65,7 +65,7 @@ public:
 	/*!
 	 * @returns the child node
 	 */
-	const PCTLStateFormula<T>& getChild() const {
+	const PctlStateFormula<T>& getChild() const {
 		return *child;
 	}
 
@@ -73,7 +73,7 @@ public:
 	 * Sets the subtree
 	 * @param child the new child node
 	 */
-	void setChild(PCTLStateFormula<T>* child) {
+	void setChild(PctlStateFormula<T>* child) {
 		this->child = child;
 	}
 
@@ -95,7 +95,7 @@ public:
 	 *
 	 * @returns a new BoundedUntil-object that is identical the called object.
 	 */
-	virtual PCTLPathFormula<T>* clone() const {
+	virtual PctlPathFormula<T>* clone() const {
 		Next<T>* result = new Next<T>();
 		if (child != NULL) {
 			result->setChild(child);
@@ -117,7 +117,7 @@ public:
 	}
 
 private:
-	PCTLStateFormula<T>* child;
+	PctlStateFormula<T>* child;
 };
 
 } //namespace formula
diff --git a/src/formula/Not.h b/src/formula/Not.h
index b4afb7d72..26ae6320c 100644
--- a/src/formula/Not.h
+++ b/src/formula/Not.h
@@ -8,7 +8,7 @@
 #ifndef MRMC_FORMULA_NOT_H_
 #define MRMC_FORMULA_NOT_H_
 
-#include "PCTLStateFormula.h"
+#include "PctlStateFormula.h"
 
 namespace mrmc {
 
@@ -23,11 +23,11 @@ namespace formula {
  * 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 PCTLStateFormula
- * @see PCTLFormula
+ * @see PctlStateFormula
+ * @see PctlFormula
  */
 template <class T>
-class Not : public PCTLStateFormula<T> {
+class Not : public PctlStateFormula<T> {
 
 public:
 	/*!
@@ -41,7 +41,7 @@ public:
 	 * Constructor
 	 * @param child The child node
 	 */
-	Not(PCTLStateFormula<T>* child) {
+	Not(PctlStateFormula<T>* child) {
 		this->child = child;
 	}
 
@@ -60,7 +60,7 @@ public:
 	/*!
 	 * @returns The child node
 	 */
-	const PCTLStateFormula<T>& getChild() const {
+	const PctlStateFormula<T>& getChild() const {
 		return *child;
 	}
 
@@ -68,7 +68,7 @@ public:
 	 * Sets the subtree
 	 * @param child the new child node
 	 */
-	void setChild(PCTLStateFormula<T>* child) {
+	void setChild(PctlStateFormula<T>* child) {
 		this->child = child;
 	}
 
@@ -88,7 +88,7 @@ public:
 	 *
 	 * @returns a new AND-object that is identical the called object.
 	 */
-	virtual PCTLStateFormula<T>* clone() const {
+	virtual PctlStateFormula<T>* clone() const {
 		Not<T>* result = new Not<T>();
 		if (child != NULL) {
 			result->setChild(child);
@@ -110,7 +110,7 @@ public:
 	}
 
 private:
-	PCTLStateFormula<T>* child;
+	PctlStateFormula<T>* child;
 };
 
 } //namespace formula
diff --git a/src/formula/Or.h b/src/formula/Or.h
index 110ee5228..bc1302185 100644
--- a/src/formula/Or.h
+++ b/src/formula/Or.h
@@ -8,7 +8,7 @@
 #ifndef MRMC_FORMULA_OR_H_
 #define MRMC_FORMULA_OR_H_
 
-#include "PCTLStateFormula.h"
+#include "PctlStateFormula.h"
 
 namespace mrmc {
 
@@ -26,11 +26,11 @@ namespace formula {
  * The subtrees are seen as part of the object and deleted with the object
  * (this behavior can be prevented by setting them to NULL before deletion)
  *
- * @see PCTLStateFormula
- * @see PCTLFormula
+ * @see PctlStateFormula
+ * @see PctlFormula
  */
 template <class T>
-class Or : public PCTLStateFormula<T> {
+class Or : public PctlStateFormula<T> {
 
 public:
 	/*!
@@ -49,7 +49,7 @@ public:
 	 * @param left The left sub formula
 	 * @param right The right sub formula
 	 */
-	Or(PCTLStateFormula<T>* left, PCTLStateFormula<T>* right) {
+	Or(PctlStateFormula<T>* left, PctlStateFormula<T>* right) {
 		this->left = left;
 		this->right = right;
 	}
@@ -74,7 +74,7 @@ public:
 	 *
 	 * @param newLeft the new left child.
 	 */
-	void setLeft(PCTLStateFormula<T>* newLeft) {
+	void setLeft(PctlStateFormula<T>* newLeft) {
 		left = newLeft;
 	}
 
@@ -83,21 +83,21 @@ public:
 	 *
 	 * @param newRight the new right child.
 	 */
-	void setRight(PCTLStateFormula<T>* newRight) {
+	void setRight(PctlStateFormula<T>* newRight) {
 		right = newRight;
 	}
 
 	/*!
 	 * @returns a pointer to the left child node
 	 */
-	const PCTLStateFormula<T>& getLeft() const {
+	const PctlStateFormula<T>& getLeft() const {
 		return *left;
 	}
 
 	/*!
 	 * @returns a pointer to the right child node
 	 */
-	const PCTLStateFormula<T>& getRight() const {
+	const PctlStateFormula<T>& getRight() const {
 		return *right;
 	}
 
@@ -120,7 +120,7 @@ public:
 	 *
 	 * @returns a new AND-object that is identical the called object.
 	 */
-	virtual PCTLStateFormula<T>* clone() const {
+	virtual PctlStateFormula<T>* clone() const {
 		Or<T>* result = new Or();
 		if (this->left != NULL) {
 		  result->setLeft(left->clone());
@@ -145,8 +145,8 @@ public:
 	}
 
 private:
-	PCTLStateFormula<T>* left;
-	PCTLStateFormula<T>* right;
+	PctlStateFormula<T>* left;
+	PctlStateFormula<T>* right;
 };
 
 } //namespace formula
diff --git a/src/formula/PCTLformula.h b/src/formula/PctlFormula.h
similarity index 87%
rename from src/formula/PCTLformula.h
rename to src/formula/PctlFormula.h
index 26c805b3e..a4d910483 100644
--- a/src/formula/PCTLformula.h
+++ b/src/formula/PctlFormula.h
@@ -1,5 +1,5 @@
 /*
- * PCTLformula.h
+ * Pctlformula.h
  *
  *  Created on: 19.10.2012
  *      Author: Thomas Heinemann
@@ -23,16 +23,16 @@ namespace formula {
  * @attention This class is abstract.
  * @note Formula classes do not have copy constructors. The parameters of the constructors are usually the subtrees, so
  * 	   the syntax conflicts with copy constructors for unary operators. To produce an identical object, the classes
- * 	   PCTLPathFormula and PCTLStateFormula offer the method clone().
+ * 	   PctlPathFormula and PctlStateFormula offer the method clone().
  */
 template <class T>
-class PCTLFormula {
+class PctlFormula {
 
 public:
 	/*!
 	 * virtual destructor
 	 */
-	virtual ~PCTLFormula() { }
+	virtual ~PctlFormula() { }
 
 	/*!
 	 * @note This function is not implemented in this class.
diff --git a/src/formula/PCTLPathFormula.h b/src/formula/PctlPathFormula.h
similarity index 90%
rename from src/formula/PCTLPathFormula.h
rename to src/formula/PctlPathFormula.h
index c8230f621..9b6a38b94 100644
--- a/src/formula/PCTLPathFormula.h
+++ b/src/formula/PctlPathFormula.h
@@ -1,5 +1,5 @@
 /*
- * PCTLPathFormula.h
+ * PctlPathFormula.h
  *
  *  Created on: 19.10.2012
  *      Author: Thomas Heinemann
@@ -8,7 +8,7 @@
 #ifndef MRMC_FORMULA_PCTLPATHFORMULA_H_
 #define MRMC_FORMULA_PCTLPATHFORMULA_H_
 
-#include "PCTLformula.h"
+#include "PctlFormula.h"
 #include "modelChecker/DtmcPrctlModelChecker.h"
 #include <vector>
 
@@ -26,13 +26,13 @@ namespace formula {
  * 	   clone().
  */
 template <class T>
-class PCTLPathFormula : public PCTLFormula<T> {
+class PctlPathFormula : public PctlFormula<T> {
 
 public:
 	/*!
 	 * empty destructor
 	 */
-	virtual ~PCTLPathFormula() { }
+	virtual ~PctlPathFormula() { }
 
 	/*!
 	 * Clones the called object.
@@ -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() const = 0;
+	virtual PctlPathFormula<T>* clone() const = 0;
 
 	/*!
 	 * Calls the model checker to check this formula.
diff --git a/src/formula/PCTLStateFormula.h b/src/formula/PctlStateFormula.h
similarity index 90%
rename from src/formula/PCTLStateFormula.h
rename to src/formula/PctlStateFormula.h
index c9ed0b5fe..c4eee14f2 100644
--- a/src/formula/PCTLStateFormula.h
+++ b/src/formula/PctlStateFormula.h
@@ -1,5 +1,5 @@
 /*
- * PCTLStateFormula.h
+ * PctlStateFormula.h
  *
  *  Created on: 19.10.2012
  *      Author: Thomas Heinemann
@@ -8,7 +8,7 @@
 #ifndef MRMC_FORMULA_PCTLSTATEFORMULA_H_
 #define MRMC_FORMULA_PCTLSTATEFORMULA_H_
 
-#include "PCTLformula.h"
+#include "PctlFormula.h"
 #include "storage/BitVector.h"
 #include "modelChecker/DtmcPrctlModelChecker.h"
 
@@ -26,13 +26,13 @@ namespace formula {
  * 	   clone().
  */
 template <class T>
-class PCTLStateFormula : public PCTLFormula<T> {
+class PctlStateFormula : public PctlFormula<T> {
 
 public:
 	/*!
 	 * empty destructor
 	 */
-	virtual ~PCTLStateFormula() { }
+	virtual ~PctlStateFormula() { }
 
 	/*!
 	 * Clones the called object.
@@ -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() const = 0;
+	virtual PctlStateFormula<T>* clone() const = 0;
 
 	/*!
 	 * Calls the model checker to check this formula.
diff --git a/src/formula/ProbabilisticIntervalOperator.h b/src/formula/ProbabilisticIntervalOperator.h
index 6fe054366..5fd2943af 100644
--- a/src/formula/ProbabilisticIntervalOperator.h
+++ b/src/formula/ProbabilisticIntervalOperator.h
@@ -8,8 +8,8 @@
 #ifndef MRMC_FORMULA_PROBABILISTICINTERVALOPERATOR_H_
 #define MRMC_FORMULA_PROBABILISTICINTERVALOPERATOR_H_
 
-#include "PCTLStateFormula.h"
-#include "PCTLPathFormula.h"
+#include "PctlStateFormula.h"
+#include "PctlPathFormula.h"
 #include "utility/ConstTemplates.h"
 
 namespace mrmc {
@@ -35,14 +35,14 @@ namespace formula {
  * (this behavior can be prevented by setting them to NULL before deletion)
  *
  *
- * @see PCTLStateFormula
- * @see PCTLPathFormula
+ * @see PctlStateFormula
+ * @see PctlPathFormula
  * @see ProbabilisticOperator
  * @see ProbabilisticNoBoundsOperator
- * @see PCTLFormula
+ * @see PctlFormula
  */
 template<class T>
-class ProbabilisticIntervalOperator : public PCTLStateFormula<T> {
+class ProbabilisticIntervalOperator : public PctlStateFormula<T> {
 
 public:
 	/*!
@@ -61,7 +61,7 @@ public:
 	 * @param upperBound The upper bound for the probability
 	 * @param pathFormula The child node
 	 */
-	ProbabilisticIntervalOperator(T lowerBound, T upperBound, PCTLPathFormula<T>& pathFormula) {
+	ProbabilisticIntervalOperator(T lowerBound, T upperBound, PctlPathFormula<T>& pathFormula) {
 		this->lower = lowerBound;
 		this->upper = upperBound;
 		this->pathFormula = &pathFormula;
@@ -82,7 +82,7 @@ public:
 	/*!
 	 * @returns the child node (representation of a PCTL path formula)
 	 */
-	const PCTLPathFormula<T>& getPathFormula () const {
+	const PctlPathFormula<T>& getPathFormula () const {
 		return *pathFormula;
 	}
 
@@ -105,7 +105,7 @@ public:
 	 *
 	 * @param pathFormula the path formula that becomes the new child node
 	 */
-	void setPathFormula(PCTLPathFormula<T>* pathFormula) {
+	void setPathFormula(PctlPathFormula<T>* pathFormula) {
 		this->pathFormula = pathFormula;
 	}
 
@@ -141,7 +141,7 @@ public:
 	 *
 	 * @returns a new AND-object that is identical the called object.
 	 */
-	virtual PCTLStateFormula<T>* clone() const {
+	virtual PctlStateFormula<T>* clone() const {
 		ProbabilisticIntervalOperator<T>* result = new ProbabilisticIntervalOperator<T>();
 		result->setInterval(lower, upper);
 		if (pathFormula != NULL) {
@@ -166,7 +166,7 @@ public:
 private:
 	T lower;
 	T upper;
-	PCTLPathFormula<T>* pathFormula;
+	PctlPathFormula<T>* pathFormula;
 };
 
 } //namespace formula
diff --git a/src/formula/ProbabilisticNoBoundsOperator.h b/src/formula/ProbabilisticNoBoundsOperator.h
index 0082fe33f..b89080ca7 100644
--- a/src/formula/ProbabilisticNoBoundsOperator.h
+++ b/src/formula/ProbabilisticNoBoundsOperator.h
@@ -8,8 +8,8 @@
 #ifndef MRMC_FORMULA_PROBABILISTICNOBOUNDSOPERATOR_H_
 #define MRMC_FORMULA_PROBABILISTICNOBOUNDSOPERATOR_H_
 
-#include "PCTLformula.h"
-#include "PCTLPathFormula.h"
+#include "PctlFormula.h"
+#include "PctlPathFormula.h"
 
 namespace mrmc {
 namespace formula {
@@ -26,20 +26,20 @@ namespace formula {
  *
  * @note
  * 	This class is a hybrid of a state and path formula, and may only appear as the outermost operator.
- * 	Hence, it is seen as neither a state nor a path formula, but is directly derived from PCTLformula.
+ * 	Hence, it is seen as neither a state nor a path formula, but is directly derived from PctlFormula.
  *
  * 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 PCTLStateFormula
- * @see PCTLPathFormula
+ * @see PctlStateFormula
+ * @see PctlPathFormula
  * @see ProbabilisticOperator
  * @see ProbabilisticIntervalOperator
- * @see PCTLFormula
+ * @see PctlFormula
  */
 template <class T>
-class ProbabilisticNoBoundsOperator: public mrmc::formula::PCTLFormula<T> {
+class ProbabilisticNoBoundsOperator: public mrmc::formula::PctlFormula<T> {
 public:
 	/*!
 	 * Empty constructor
@@ -54,7 +54,7 @@ public:
 	 *
 	 * @param pathFormula The child node.
 	 */
-	ProbabilisticNoBoundsOperator(PCTLPathFormula<T> &pathFormula) {
+	ProbabilisticNoBoundsOperator(PctlPathFormula<T> &pathFormula) {
 		this->pathFormula = &pathFormula;
 	}
 
@@ -68,7 +68,7 @@ public:
 	/*!
 	 * @returns the child node (representation of a PCTL path formula)
 	 */
-	const PCTLPathFormula<T>& getPathFormula () const {
+	const PctlPathFormula<T>& getPathFormula () const {
 		return *pathFormula;
 	}
 
@@ -77,7 +77,7 @@ public:
 	 *
 	 * @param pathFormula the path formula that becomes the new child node
 	 */
-	void setPathFormula(PCTLPathFormula<T>* pathFormula) {
+	void setPathFormula(PctlPathFormula<T>* pathFormula) {
 		this->pathFormula = pathFormula;
 	}
 
@@ -92,7 +92,7 @@ public:
 	}
 
 private:
-	PCTLPathFormula<T>* pathFormula;
+	PctlPathFormula<T>* pathFormula;
 };
 
 } /* namespace formula */
diff --git a/src/formula/ProbabilisticOperator.h b/src/formula/ProbabilisticOperator.h
index 8905e030d..b1131ef4b 100644
--- a/src/formula/ProbabilisticOperator.h
+++ b/src/formula/ProbabilisticOperator.h
@@ -8,7 +8,7 @@
 #ifndef MRMC_FORMULA_PROBABILISTICOPERATOR_H_
 #define MRMC_FORMULA_PROBABILISTICOPERATOR_H_
 
-#include "PCTLStateFormula.h"
+#include "PctlStateFormula.h"
 
 namespace mrmc {
 namespace formula {
@@ -32,14 +32,14 @@ namespace formula {
  * (this behavior can be prevented by setting them to NULL before deletion)
  *
  *
- * @see PCTLStateFormula
- * @see PCTLPathFormula
+ * @see PctlStateFormula
+ * @see PctlPathFormula
  * @see ProbabilisticIntervalOperator
  * @see ProbabilisticNoBoundsOperator
- * @see PCTLFormula
+ * @see PctlFormula
  */
 template<class T>
-class ProbabilisticOperator : public mrmc::formula::PCTLStateFormula<T> {
+class ProbabilisticOperator : public mrmc::formula::PctlStateFormula<T> {
 public:
 	/*!
 	 * Empty constructor
@@ -55,7 +55,7 @@ public:
 	 * @param bound The expected value for path formulas
 	 * @param pathFormula The child node
 	 */
-	ProbabilisticOperator(T bound, PCTLPathFormula<T>& pathFormula) {
+	ProbabilisticOperator(T bound, PctlPathFormula<T>& pathFormula) {
 		this->bound = bound;
 		this->pathFormula = &pathFormula;
 	}
@@ -73,7 +73,7 @@ public:
 	/*!
 	 * @returns the child node (representation of a PCTL path formula)
 	 */
-	const PCTLPathFormula<T>& getPathFormula () const {
+	const PctlPathFormula<T>& getPathFormula () const {
 		return *pathFormula;
 	}
 
@@ -89,7 +89,7 @@ public:
 	 *
 	 * @param pathFormula the path formula that becomes the new child node
 	 */
-	void setPathFormula(PCTLPathFormula<T>* pathFormula) {
+	void setPathFormula(PctlPathFormula<T>* pathFormula) {
 		this->pathFormula = pathFormula;
 	}
 
@@ -109,7 +109,7 @@ public:
 	 *
 	 * @returns a new ProbabilisticOperator-object that is identical to the called object.
 	 */
-	virtual PCTLStateFormula<T>* clone() const {
+	virtual PctlStateFormula<T>* clone() const {
 		ProbabilisticOperator<T>* result = new ProbabilisticOperator<T>();
 		result->setBound(bound);
 		if (pathFormula != NULL) {
@@ -134,9 +134,9 @@ public:
 	}
 
 	/*!
-	 *	Returns a string representation of this PCTLStateFormula
+	 *	Returns a string representation of this PctlStateFormula
 	 * 
-	 * @returns a string representation of this PCTLStateFormula
+	 * @returns a string representation of this PctlStateFormula
 	 */
 	virtual std::string toString() const {
 		std::string result = " P=";
@@ -148,7 +148,7 @@ public:
 	}
 private:
 	T bound;
-	PCTLPathFormula<T>* pathFormula;
+	PctlPathFormula<T>* pathFormula;
 };
 
 } /* namespace formula */
diff --git a/src/formula/Until.h b/src/formula/Until.h
index fb0b67f47..3f094e3a3 100644
--- a/src/formula/Until.h
+++ b/src/formula/Until.h
@@ -8,8 +8,8 @@
 #ifndef MRMC_FORMULA_UNTIL_H_
 #define MRMC_FORMULA_UNTIL_H_
 
-#include "PCTLPathFormula.h"
-#include "PCTLStateFormula.h"
+#include "PctlPathFormula.h"
+#include "PctlStateFormula.h"
 
 namespace mrmc {
 
@@ -28,11 +28,11 @@ namespace formula {
  * The subtrees are seen as part of the object and deleted with the object
  * (this behavior can be prevented by setting them to NULL before deletion)
  *
- * @see PCTLPathFormula
- * @see PCTLFormula
+ * @see PctlPathFormula
+ * @see PctlFormula
  */
 template <class T>
-class Until : public PCTLPathFormula<T> {
+class Until : public PctlPathFormula<T> {
 
 public:
 	/*!
@@ -49,7 +49,7 @@ public:
 	 * @param left The left formula subtree
 	 * @param right The left formula subtree
 	 */
-	Until(PCTLStateFormula<T>* left, PCTLStateFormula<T>* right) {
+	Until(PctlStateFormula<T>* left, PctlStateFormula<T>* right) {
 		this->left = left;
 		this->right = right;
 	}
@@ -74,7 +74,7 @@ public:
 	 *
 	 * @param newLeft the new left child.
 	 */
-	void setLeft(PCTLStateFormula<T>* newLeft) {
+	void setLeft(PctlStateFormula<T>* newLeft) {
 		left = newLeft;
 	}
 
@@ -83,21 +83,21 @@ public:
 	 *
 	 * @param newRight the new right child.
 	 */
-	void setRight(PCTLStateFormula<T>* newRight) {
+	void setRight(PctlStateFormula<T>* newRight) {
 		right = newRight;
 	}
 
 	/*!
 	 * @returns a pointer to the left child node
 	 */
-	const PCTLStateFormula<T>& getLeft() const {
+	const PctlStateFormula<T>& getLeft() const {
 		return *left;
 	}
 
 	/*!
 	 * @returns a pointer to the right child node
 	 */
-	const PCTLStateFormula<T>& getRight() const {
+	const PctlStateFormula<T>& getRight() const {
 		return *right;
 	}
 
@@ -120,7 +120,7 @@ public:
 	 *
 	 * @returns a new BoundedUntil-object that is identical the called object.
 	 */
-	virtual PCTLPathFormula<T>* clone() const {
+	virtual PctlPathFormula<T>* clone() const {
 		Until<T>* result = new Until();
 		if (left != NULL) {
 			result->setLeft(left->clone());
@@ -145,8 +145,8 @@ public:
 	}
 
 private:
-	PCTLStateFormula<T>* left;
-	PCTLStateFormula<T>* right;
+	PctlStateFormula<T>* left;
+	PctlStateFormula<T>* right;
 };
 
 } //namespace formula
diff --git a/src/modelChecker/DtmcPrctlModelChecker.h b/src/modelChecker/DtmcPrctlModelChecker.h
index 984655aa9..9556fd966 100644
--- a/src/modelChecker/DtmcPrctlModelChecker.h
+++ b/src/modelChecker/DtmcPrctlModelChecker.h
@@ -23,8 +23,8 @@ class DtmcPrctlModelChecker;
 
 }
 
-#include "src/formula/PCTLPathFormula.h"
-#include "src/formula/PCTLStateFormula.h"
+#include "src/formula/PctlPathFormula.h"
+#include "src/formula/PctlStateFormula.h"
 
 #include "src/formula/Formulas.h"
 
@@ -96,7 +96,7 @@ public:
 	 * @param formula The state formula to check
 	 * @returns The set of states satisfying the formula, represented by a bit vector
 	 */
-	mrmc::storage::BitVector* checkStateFormula(const mrmc::formula::PCTLStateFormula<Type>& formula) const {
+	mrmc::storage::BitVector* checkStateFormula(const mrmc::formula::PctlStateFormula<Type>& formula) const {
 		return formula.check(*this);
 	}
 
@@ -117,16 +117,16 @@ public:
 	/*!
 	 * The check method for a formula with an AP node as root in its formula tree
 	 *
-	 * @param formula The AP state formula to check
+	 * @param formula The Ap state formula to check
 	 * @returns The set of states satisfying the formula, represented by a bit vector
 	 */
-	mrmc::storage::BitVector* checkAP(const mrmc::formula::AP<Type>& formula) const {
-		if (formula.getAP().compare("true") == 0) {
+	mrmc::storage::BitVector* checkAp(const mrmc::formula::Ap<Type>& formula) const {
+		if (formula.getAp().compare("true") == 0) {
 			return new mrmc::storage::BitVector(model->getNumberOfStates(), 1);
-		} else if (formula.getAP().compare("false") == 0) {
+		} else if (formula.getAp().compare("false") == 0) {
 			return new mrmc::storage::BitVector(model->getNumberOfStates());
 		}
-		return new mrmc::storage::BitVector(*model->getLabeledStates(formula.getAP()));
+		return new mrmc::storage::BitVector(*model->getLabeledStates(formula.getAp()));
 	}
 
 	/*!
@@ -226,7 +226,7 @@ public:
 	 * @param formula The path formula to check
 	 * @returns for each state the probability that the path formula holds.
 	 */
-	std::vector<Type>* checkPathFormula(const mrmc::formula::PCTLPathFormula<Type>& formula) const {
+	std::vector<Type>* checkPathFormula(const mrmc::formula::PctlPathFormula<Type>& formula) const {
 		return formula.check(*this);
 	}
 
diff --git a/src/parser/PrctlParser.cpp b/src/parser/PrctlParser.cpp
index 695d64a78..f1a23077a 100644
--- a/src/parser/PrctlParser.cpp
+++ b/src/parser/PrctlParser.cpp
@@ -58,7 +58,7 @@ namespace
 		/*!
 		 *	@brief Resulting formula.
 		 */
-		mrmc::formula::PCTLFormula<double>* result;
+		mrmc::formula::PctlFormula<double>* result;
 		
 		struct dump
 		{
diff --git a/src/parser/PrctlParser.h b/src/parser/PrctlParser.h
index 0cd5ee7cf..24dc746bb 100644
--- a/src/parser/PrctlParser.h
+++ b/src/parser/PrctlParser.h
@@ -1,7 +1,7 @@
 #ifndef MRMC_PARSER_PRCTLPARSER_H_
 #define MRMC_PARSER_PRCTLPARSER_H_
 
-#include "src/formula/PCTLformula.h"
+#include "src/formula/PctlFormula.h"
 #include "src/parser/Parser.h"
 
 namespace mrmc {
@@ -18,13 +18,13 @@ class PrctlParser : Parser
 		/*!
 		 *	@brief return formula object parsed from file.
 		 */
-		mrmc::formula::PCTLFormula<double>* getFormula()
+		mrmc::formula::PctlFormula<double>* getFormula()
 		{
 			return this->formula;
 		}
 	
 	private:
-		mrmc::formula::PCTLFormula<double>* formula;
+		mrmc::formula::PctlFormula<double>* formula;
 };
 
 } // namespace parser