diff --git a/src/formula/AP.h b/src/formula/AP.h
new file mode 100644
index 000000000..6305dfebf
--- /dev/null
+++ b/src/formula/AP.h
@@ -0,0 +1,46 @@
+/*
+ * AP.h
+ *
+ *  Created on: 19.10.2012
+ *      Author: Thomas Heinemann
+ */
+
+#ifndef AP_H_
+#define AP_H_
+
+#include "PCTLStateFormula.h"
+
+namespace mrmc {
+
+namespace formula {
+
+class AP : public PCTLStateFormula {
+   private:
+   std::string ap;
+   public:
+      AP(std::string ap) {
+         this->ap = ap;
+      }
+
+      AP(char* ap) {
+         this->ap = ap;
+      }
+
+      std::string getAP() {
+         return ap;
+      }
+
+      std::string toString() {
+         return getAP();
+      }
+
+      virtual enum stateFormulaTypes type() {
+            return stateFormulaTypes::AP;
+      }
+};
+
+} //namespace formula
+
+} //namespace mrmc
+
+#endif /* AP_H_ */
diff --git a/src/formula/And.h b/src/formula/And.h
new file mode 100644
index 000000000..9d09c526e
--- /dev/null
+++ b/src/formula/And.h
@@ -0,0 +1,66 @@
+/*
+ * And.h
+ *
+ *  Created on: 19.10.2012
+ *      Author: Thomas Heinemann
+ */
+
+#ifndef AND_H_
+#define AND_H_
+
+#include "PCTLStateFormula.h"
+#include <string>
+
+namespace mrmc {
+
+namespace formula {
+
+class And : public PCTLStateFormula {
+   private:
+      PCTLStateFormula* left;
+      PCTLStateFormula* right;
+   public:
+      And() {
+         left = NULL;
+         right = NULL;
+      }
+      And(PCTLStateFormula* left, PCTLStateFormula* right) {
+         this->left = left;
+         this->right = right;
+      }
+
+      void setLeft(PCTLStateFormula* newLeft) {
+         left = newLeft;
+      }
+
+      void setRight(PCTLStateFormula* newRight) {
+         right = newRight;
+      }
+
+      PCTLStateFormula* getLeft() {
+         return left;
+      }
+
+      PCTLStateFormula* getRight() {
+         return right;
+      }
+
+      std::string toString() {
+         std::string result = "(";
+         result += left->toString();
+         result += " && ";
+         result += right->toString();
+         result += ")";
+         return result;
+      }
+
+      virtual enum stateFormulaTypes type() {
+            return AND;
+      }
+};
+
+} //namespace formula
+
+} //namespace mrmc
+
+#endif /* AND_H_ */
diff --git a/src/formula/BoundedUntil.h b/src/formula/BoundedUntil.h
new file mode 100644
index 000000000..bc1510fe3
--- /dev/null
+++ b/src/formula/BoundedUntil.h
@@ -0,0 +1,81 @@
+/*
+ * BoundedUntil.h
+ *
+ *  Created on: 19.10.2012
+ *      Author: Thomas Heinemann
+ */
+
+#ifndef BOUNDEDUNTIL_H_
+#define BOUNDEDUNTIL_H_
+
+#include "PCTLPathFormula.h"
+
+namespace mrmc {
+
+namespace formula {
+
+class BoundedUntil : public PCTLPathFormula {
+      PCTLStateFormula* left;
+      PCTLStateFormula* right;
+      uint_fast64_t bound;
+   public:
+      BoundedUntil() {
+         this->left = NULL;
+         this->right = NULL;
+         bound = 0;
+      }
+
+      BoundedUntil(PCTLStateFormula* left, PCTLStateFormula* right,
+                   uint_fast64_t bound) {
+         this->left = left;
+         this->right = right;
+         this->bound = bound;
+      }
+
+      virtual ~BoundedUntil();
+
+      void setLeft(PCTLStateFormula* newLeft) {
+         left = newLeft;
+      }
+
+      void setRight(PCTLStateFormula* newRight) {
+         right = newRight;
+      }
+
+      PCTLStateFormula* getLeft() {
+         return left;
+      }
+
+      PCTLStateFormula* getRight() {
+         return right;
+      }
+
+      uint_fast64_t getBound() {
+         return bound;
+      }
+
+      void setBound(uint_fast64_t bound) {
+         this->bound = bound;
+      }
+
+      std::string toString() {
+         std::string result = "(";
+         result += left->toString();
+         result += " U<=";
+         result += bound;
+         result += " ";
+         result += right->toString();
+         result += ")";
+         return result;
+      }
+
+      virtual enum pathFormulaTypes type() {
+            return BOUNDED_UNTIL;
+      }
+};
+
+} //namespace formula
+
+} //namespace mrmc
+
+#endif /* BOUNDEDUNTIL_H_ */
diff --git a/src/formula/Next.h b/src/formula/Next.h
new file mode 100644
index 000000000..2fa5e1d02
--- /dev/null
+++ b/src/formula/Next.h
@@ -0,0 +1,56 @@
+/*
+ * Next.h
+ *
+ *  Created on: 19.10.2012
+ *      Author: Thomas Heinemann
+ */
+
+#ifndef NEXT_H_
+#define NEXT_H_
+
+#include "PCTLPathFormula.h"
+#include "PCTLStateFormula.h"
+
+namespace mrmc {
+
+namespace formula {
+
+
+class Next : public PCTLPathFormula {
+   private:
+      PCTLStateFormula* child;
+   public:
+      Next() {
+         this->child = NULL;
+      }
+
+      Next(PCTLStateFormula* child) {
+         this->child = child;
+      }
+
+      PCTLStateFormula* getChild() {
+         return child;
+      }
+
+      void setChild(PCTLStateFormula* child) {
+         this->child = child;
+      }
+
+      std::string toString() {
+         std::string result = "(";
+         result += " X ";
+         result += child->toString();
+         result += ")";
+         return result;
+      }
+
+      virtual enum pathFormulaTypes type() {
+            return NEXT;
+      }
+};
+
+} //namespace formula
+
+} //namespace mrmc
+
+#endif /* NEXT_H_ */
diff --git a/src/formula/Not.h b/src/formula/Not.h
new file mode 100644
index 000000000..36993c18a
--- /dev/null
+++ b/src/formula/Not.h
@@ -0,0 +1,56 @@
+/*
+ * Not.h
+ *
+ *  Created on: 19.10.2012
+ *      Author: Thomas Heinemann
+ */
+
+#ifndef NOT_H_
+#define NOT_H_
+
+namespace mrmc {
+
+namespace formula {
+
+#include "PCTLStateFormula.h"
+
+class Not : public PCTLStateFormula {
+   private:
+      PCTLStateFormula* child;
+   public:
+      Not() {
+         this->child = NULL;
+      }
+
+      Not(PCTLStateFormula* child) {
+         this->child = child;
+      }
+
+      virtual ~Not() {
+
+      }
+
+      PCTLStateFormula* getChild() {
+         return child;
+      }
+
+      void setChild(PCTLStateFormula* child) {
+         this->child = child;
+      }
+
+      std::string toString() {
+         std::string result = "!";
+         result += child->toString();
+         return result;
+      }
+
+      virtual enum stateFormulaTypes type() {
+            return NOT;
+      }
+};
+
+} //namespace formula
+
+} //namespace MRMC
+
+#endif /* NOT_H_ */
diff --git a/src/formula/Or.h b/src/formula/Or.h
new file mode 100644
index 000000000..6559d36aa
--- /dev/null
+++ b/src/formula/Or.h
@@ -0,0 +1,65 @@
+/*
+ * Or.h
+ *
+ *  Created on: 19.10.2012
+ *      Author: Thomas Heinemann
+ */
+
+#ifndef OR_H_
+#define OR_H_
+
+#include "PCTLStateFormula.h"
+
+namespace mrmc {
+
+namespace formula {
+
+class Or : public PCTLStateFormula {
+   private:
+      PCTLStateFormula* left;
+      PCTLStateFormula* right;
+   public:
+      Or() {
+         left = NULL;
+         right = NULL;
+      }
+      Or(PCTLStateFormula* left, PCTLStateFormula* right) {
+         this->left = left;
+         this->right = right;
+      }
+
+      void setLeft(PCTLStateFormula* newLeft) {
+         left = newLeft;
+      }
+
+      void setRight(PCTLStateFormula* newRight) {
+         right = newRight;
+      }
+
+      PCTLStateFormula* getLeft() {
+         return left;
+      }
+
+      PCTLStateFormula* getRight() {
+         return right;
+      }
+
+      std::string toString() {
+         std::string result = "(";
+         result += left->toString();
+         result += " || ";
+         result += right->toString();
+         result += ")";
+         return result;
+      }
+
+      virtual enum stateFormulaTypes type() {
+            return OR;
+      }
+};
+
+} //namespace formula
+
+} //namespace mrmc
+
+#endif /* OR_H_ */
diff --git a/src/formula/PCTLPathFormula.h b/src/formula/PCTLPathFormula.h
new file mode 100644
index 000000000..7114caca9
--- /dev/null
+++ b/src/formula/PCTLPathFormula.h
@@ -0,0 +1,28 @@
+/*
+ * PCTLPathFormula.h
+ *
+ *  Created on: 19.10.2012
+ *      Author: Thomas Heinemann
+ */
+
+#ifndef PCTLPATHFORMULA_H_
+#define PCTLPATHFORMULA_H_
+
+#include "PCTLformula.h"
+#include "formulaTypes.h"
+
+namespace mrmc {
+
+namespace formula {
+
+//abstract
+class PCTLPathFormula : public PCTLFormula {
+   public:
+      virtual enum pathFormulaTypes type() = 0;
+};
+
+} //namespace formula
+
+} //namespace mrmc
+
+#endif /* PCTLPATHFORMULA_H_ */
diff --git a/src/formula/PCTLStateFormula.h b/src/formula/PCTLStateFormula.h
new file mode 100644
index 000000000..3361a11a4
--- /dev/null
+++ b/src/formula/PCTLStateFormula.h
@@ -0,0 +1,30 @@
+/*
+ * PCTLStateFormula.h
+ *
+ *  Created on: 19.10.2012
+ *      Author: Thomas Heinemann
+ */
+
+#ifndef PCTLSTATEFORMULA_H_
+#define PCTLSTATEFORMULA_H_
+
+#include "PCTLformula.h"
+#include "formulaTypes.h"
+
+namespace mrmc {
+
+namespace formula {
+
+//abstract
+class PCTLStateFormula : public PCTLFormula {
+   public:
+      virtual enum stateFormulaTypes type() = 0;
+
+};
+
+} //namespace formula
+
+} //namespace mrmc
+
+
+#endif /* PCTLSTATEFORMULA_H_ */
diff --git a/src/formula/PCTLformula.h b/src/formula/PCTLformula.h
new file mode 100644
index 000000000..996416a2c
--- /dev/null
+++ b/src/formula/PCTLformula.h
@@ -0,0 +1,28 @@
+/*
+ * PCTLformula.h
+ *
+ *  Created on: 19.10.2012
+ *      Author: Thomas Heinemann
+ */
+
+#ifndef PCTLFORMULA_H_
+#define PCTLFORMULA_H_
+
+#include <string>
+
+namespace mrmc {
+
+namespace formula {
+
+
+//abstract
+class PCTLFormula {
+   public:
+      virtual std::string toString() = 0;
+};
+
+} //namespace formula
+
+} //namespace mrmc
+
+#endif /* PCTLFORMULA_H_ */
diff --git a/src/formula/ProbabilisticOperator.h b/src/formula/ProbabilisticOperator.h
new file mode 100644
index 000000000..bd83a1431
--- /dev/null
+++ b/src/formula/ProbabilisticOperator.h
@@ -0,0 +1,75 @@
+/*
+ * ProbabilisticOperator.h
+ *
+ *  Created on: 19.10.2012
+ *      Author: Thomas Heinemann
+ */
+
+#ifndef PROBABILISTICOPERATOR_H_
+#define PROBABILISTICOPERATOR_H_
+
+#include "PCTLStateFormula.h"
+
+namespace mrmc {
+
+namespace formula {
+
+template<class T>
+class ProbabilisticOperator : public PCTLStateFormula {
+      T lower;
+      T upper;
+      PCTLPathFormula* pathFormula;
+   public:
+      ProbabilisticOperator(T lowerBound, T upperBound, PCTLPathFormula* pathFormula=NULL) {
+         this->lower = lowerBound;
+         this->upper = upperBound;
+         this->pathFormula = pathFormula;
+      }
+
+      virtual ~ProbabilisticOperator() {
+         delete pathFormula;
+      }
+
+      PCTLPathFormula* getPathFormula () {
+         return pathFormula;
+      }
+
+      T getLowerBound() {
+         return lower;
+      }
+
+      T getUpperBound() {
+         return upper;
+      }
+
+      void setPathFormula(PCTLPathFormula* pathFormula) {
+         this->pathFormula = pathFormula;
+      }
+
+      void setInterval(T lowerBound, T upperBound) {
+         this->lower = lowerBound;
+         this->upper = upperBound;
+      }
+
+      std::string toString() {
+         std::string result = "(";
+         result += " P[";
+         result += lower;
+         result += ";";
+         result += upper;
+         result += "] ";
+         result += pathFormula->toString();
+         result += ")";
+         return result;
+      }
+
+      virtual enum stateFormulaTypes type() {
+            return PROBABILISTIC;
+      }
+};
+
+} //namespace formula
+
+} //namespace mrmc
+
+#endif /* PROBABILISTICOPERATOR_H_ */
diff --git a/src/formula/Until.h b/src/formula/Until.h
new file mode 100644
index 000000000..d12f6ed78
--- /dev/null
+++ b/src/formula/Until.h
@@ -0,0 +1,67 @@
+/*
+ * Until.h
+ *
+ *  Created on: 19.10.2012
+ *      Author: Thomas Heinemann
+ */
+
+#ifndef UNTIL_H_
+#define UNTIL_H_
+
+#include "PCTLPathFormula.h"
+#include "PCTLStateFormula.h"
+
+namespace mrmc {
+
+namespace formula {
+
+class Until : public PCTLPathFormula {
+      PCTLStateFormula* left;
+      PCTLStateFormula* right;
+   public:
+      Until() {
+         this->left = NULL;
+         this->right = NULL;
+      }
+
+      Until(PCTLStateFormula* left, PCTLStateFormula* right) {
+         this->left = left;
+         this->right = right;
+      }
+      virtual ~Until();
+
+      void setLeft(PCTLStateFormula* newLeft) {
+         left = newLeft;
+      }
+
+      void setRight(PCTLStateFormula* newRight) {
+         right = newRight;
+      }
+
+      PCTLStateFormula* getLeft() {
+         return left;
+      }
+
+      PCTLStateFormula* getRight() {
+         return right;
+      }
+
+      std::string toString() {
+         std::string result = "(";
+         result += left->toString();
+         result += " U ";
+         result += right->toString();
+         result += ")";
+         return result;
+      }
+
+      virtual enum pathFormulaTypes type() {
+            return UNTIL;
+      }
+};
+
+} //namespace formula
+
+} //namespace mrmc
+
+#endif /* UNTIL_H_ */
diff --git a/src/formula/formulaTypes.h b/src/formula/formulaTypes.h
new file mode 100644
index 000000000..41f245fa3
--- /dev/null
+++ b/src/formula/formulaTypes.h
@@ -0,0 +1,27 @@
+/*
+ * formulaTypes.h
+ *
+ *  Created on: 21.10.2012
+ *      Author: Thomas Heinemann
+ */
+
+#ifndef FORMULATYPES_H_
+#define FORMULATYPES_H_
+
+enum stateFormulaTypes {
+      AND,
+      AP,
+      NOT,
+      OR,
+      PROBABILISTIC
+};
+
+enum pathFormulaTypes {
+      NEXT,
+      UNTIL,
+      BOUNDED_UNTIL,
+      EVENTUALLY,
+      ALWAYS
+};
+
+#endif /* FORMULATYPES_H_ */
diff --git a/src/modelChecker/DtmcPrctlModelChecker.cpp b/src/modelChecker/DtmcPrctlModelChecker.cpp
new file mode 100644
index 000000000..d308005cf
--- /dev/null
+++ b/src/modelChecker/DtmcPrctlModelChecker.cpp
@@ -0,0 +1,27 @@
+/*
+ * DtmcPrctlModelChecker.cpp
+ *
+ *  Created on: 22.10.2012
+ *      Author: Thomas Heinemann
+ */
+
+#include "DtmcPrctlModelChecker.h"
+
+namespace mrmc {
+
+namespace modelChecker {
+
+template<class T>
+DtmcPrctlModelChecker<T>::DtmcPrctlModelChecker(mrmc::models::Dtmc<T>* DTMC) {
+   this->DTMC = DTMC;
+}
+
+template<class T>
+DtmcPrctlModelChecker<T>::~DtmcPrctlModelChecker() {
+   delete this->dtmc;
+}
+
+
+} //namespace modelChecker
+
+} //namespace mrmc
diff --git a/src/modelChecker/DtmcPrctlModelChecker.h b/src/modelChecker/DtmcPrctlModelChecker.h
new file mode 100644
index 000000000..c947d511f
--- /dev/null
+++ b/src/modelChecker/DtmcPrctlModelChecker.h
@@ -0,0 +1,93 @@
+/*
+ * DtmcPrctlModelChecker.h
+ *
+ *  Created on: 22.10.2012
+ *      Author: Thomas Heinemann
+ */
+
+#ifndef DTMCPRCTLMODELCHECKER_H_
+#define DTMCPRCTLMODELCHECKER_H_
+
+#include "src/formula/And.h"
+#include "src/formula/AP.h"
+#include "src/formula/BoundedUntil.h"
+#include "src/formula/Next.h"
+#include "src/formula/Not.h"
+#include "src/formula/Or.h"
+#include "src/formula/ProbabilisticOperator.h"
+#include "src/formula/Until.h"
+
+#include "src/models/dtmc.h"
+#include "src/vector/bitvector.h"
+#include <vector>
+
+namespace mrmc {
+
+namespace modelChecker {
+
+template<class T>
+class DtmcPrctlModelChecker {
+   private:
+      mrmc::models::Dtmc<T>* dtmc;
+
+   protected:
+      mrmc::models::Dtmc<T>* getDtmc() const {
+         return this->dtmc;
+      }
+
+   public:
+      explicit DtmcPrctlModelChecker(mrmc::models::Dtmc<T>* DTMC);
+      ~DtmcPrctlModelChecker();
+
+      virtual void makeAbsorbing(mrmc::vector::BitVector*) = 0;
+      virtual mrmc::vector::BitVector getStatesSatisying(mrmc::models::SingleAtomicPropositionLabeling*) = 0;
+      virtual std::vector<T> multiplyMatrixVector(std::vector<T>*) = 0;
+
+      virtual mrmc::vector::BitVector checkStateFormula(mrmc::formula::PCTLStateFormula* formula) {
+         if (formula->type() == AND) {
+            return checkAnd(static_cast<mrmc::formula::And*>(formula));
+         }
+         if (formula->type() == stateFormulaTypes::AP) {
+            return checkAP(static_cast<mrmc::formula::AP*>(formula));
+         }
+         if (formula->type() == NOT) {
+            return checkNot(static_cast<mrmc::formula::Not*>(formula));
+         }
+         if (formula->type() == OR) {
+            return checkOr(static_cast<mrmc::formula::Or*>(formula));
+         }
+         if (formula->type() == PROBABILISTIC) {
+            return checkProbabilisticOperator(
+                  static_cast<mrmc::formula::ProbabilisticOperator<T>*>(formula));
+         }
+      }
+
+
+      virtual mrmc::vector::BitVector checkAnd(mrmc::formula::And*) = 0;
+      virtual mrmc::vector::BitVector checkAP(mrmc::formula::AP*) = 0;
+      virtual mrmc::vector::BitVector checkNot(mrmc::formula::Not*) = 0;
+      virtual mrmc::vector::BitVector checkOr(mrmc::formula::Or*) = 0;
+      virtual mrmc::vector::BitVector checkProbabilisticOperator(mrmc::formula::ProbabilisticOperator<T>*) = 0;
+
+      virtual std::vector<T> checkPathFormula(mrmc::formula::PCTLPathFormula* formula) {
+         if (formula->type() == NEXT) {
+            return checkNext(static_cast<mrmc::formula::Next*>(formula));
+         }
+         if (formula->type() == UNTIL) {
+            return checkUntil(static_cast<mrmc::formula::Until*>(formula));
+         }
+         if (formula->type() == BOUNDED_UNTIL) {
+            return checkBoundedUntil(static_cast<mrmc::formula::BoundedUntil*>(formula));
+         }
+      }
+
+      virtual std::vector<T> checkBoundedUntil(mrmc::formula::BoundedUntil*) = 0;
+      virtual std::vector<T> checkNext(mrmc::formula::Next*) = 0;
+      virtual std::vector<T> checkUntil(mrmc::formula::Until*) = 0;
+};
+
+} //namespace modelChecker
+
+} //namespace mrmc
+
+#endif /* DTMCPRCTLMODELCHECKER_H_ */
diff --git a/src/sparse/static_sparse_matrix.h b/src/sparse/static_sparse_matrix.h
index fdb73b814..43d71fce5 100644
--- a/src/sparse/static_sparse_matrix.h
+++ b/src/sparse/static_sparse_matrix.h
@@ -447,47 +447,6 @@ class StaticSparseMatrix {
 		return true;
 	}
 
-   /*!
-       Creates a DOT file which provides the graph of the transition structure
-       represented by the matrix.
-
-       @param  filename The Name of the file to write in. If the file already exists,
-                        it will be overwritten.
-
-    */
-   void toDOTFile(const char* filename) {
-      FILE *P;
-
-      P = fopen(filename, "w");
-
-      if (P == NULL) {
-         pantheios::log_ERROR("File could not be opened.");
-         throw mrmc::exceptions::file_IO_exception();
-      }
-
-      fprintf(P, "digraph dtmc {\n");
-
-      uint_fast64_t row = 0;
-
-      for (uint_fast64_t i = 0; i < non_zero_entry_count; i++ ) {
-         //Check whether we have to switch to the new row
-         while (row_indications[row] <= i) {
-            ++row;
-            //write diagonal entry/self loop first
-            if (diagonal_storage[row] != 0) {
-               fprintf(P, "\t%Lu -> %Lu [label=%f]\n",
-                     row, row, diagonal_storage[row]);
-            }
-         }
-         fprintf(P, "\t%Lu -> %Lu [label=%f]\n",
-               row, column_indications[i], value_storage[i]);
-      }
-
-      fprintf(P, "}\n");
-
-      fclose(P);
-   }
-
    /*!
     * Returns the size of the matrix in memory measured in bytes.
     * @return The size of the matrix in memory measured in bytes.
diff --git a/src/utility/utility.cpp b/src/utility/utility.cpp
new file mode 100644
index 000000000..299600922
--- /dev/null
+++ b/src/utility/utility.cpp
@@ -0,0 +1,92 @@
+/*
+ * utility.cpp
+ *
+ *  Created on: 17.10.2012
+ *      Author: Thomas Heinemann
+ */
+
+#include "src/utility/utility.h"
+#include "src/parser/read_tra_file.h"
+#include "src/parser/read_lab_file.h"
+
+#include "src/sparse/static_sparse_matrix.h"
+#include "src/models/dtmc.h"
+
+namespace mrmc {
+
+namespace utility {
+
+void dtmcToDot(mrmc::models::DTMC<double>* dtmc, const char* filename) {
+   FILE *P;
+   mrmc::sparse::StaticSparseMatrix<double>* matrix = dtmc->getTransitions();
+   mrmc::dtmc::Labeling* labels = dtmc->getLabels();
+
+   uint_fast64_t* row_indications = matrix->getRowIndications();
+   uint_fast64_t* column_indications = matrix->getColumnIndications();
+   double* value_storage = matrix->getStoragePointer();
+   double* diagonal_storage = matrix->getDiagonalStorage();
+
+   P = fopen(filename, "w");
+
+   if (P == NULL) {
+      pantheios::log_ERROR("File could not be opened.");
+      throw mrmc::exceptions::file_IO_exception();
+   }
+
+   fprintf(P, "digraph dtmc {\n");
+
+   //Specify the nodes and their labels
+   for (uint_fast64_t i = 1; i <= dtmc->getNodeCount(); i++) {
+      fprintf(P, "\t%Lu[label=\"%Lu\\n{", i, i);
+      char komma=' ';
+      for(auto it = labels->getPropositionMap()->begin();
+               it != labels->getPropositionMap()->end();
+               it++) {
+         if(labels->nodeHasProposition(it->first, i)) {
+            fprintf(P, "%c%s", komma, (it->first).c_str());
+         }
+         char komma=',';
+      }
+
+      fprintf(P, " }\"];\n");
+   }
+
+   uint_fast64_t row = 0;
+
+   for (uint_fast64_t i = 0; i < matrix->getNonZeroEntryCount(); i++ ) {
+      //Check whether we have to switch to the new row
+      while (row_indications[row] <= i) {
+         ++row;
+         //write diagonal entry/self loop first
+         if (diagonal_storage[row] != 0) {
+            fprintf(P, "\t%Lu -> %Lu [label=%f]\n",
+                  row, row, diagonal_storage[row]);
+         }
+      }
+      fprintf(P, "\t%Lu -> %Lu [label=%f]\n",
+            row, column_indications[i], value_storage[i]);
+   }
+
+
+
+   fprintf(P, "}\n");
+
+   fclose(P);
+}
+
+mrmc::models::Dtmc<double>* parseDTMC(const char* tra_file, const char* lab_file) {
+   mrmc::sparse::StaticSparseMatrix<double>* transition_matrix =
+         mrmc::parser::read_tra_file(tra_file);
+   uint_fast64_t node_count = transition_matrix->getRowCount();
+
+   mrmc::dtmc::Labeling* labeling =
+         mrmc::parser::read_lab_file(node_count, lab_file);
+
+   mrmc::models::Dtmc<double>* result =
+         new mrmc::models::Dtmc<double>(transition_matrix, labeling);
+   return result;
+}
+
+}
+
+}
diff --git a/src/utility/utility.h b/src/utility/utility.h
new file mode 100644
index 000000000..464ccecb6
--- /dev/null
+++ b/src/utility/utility.h
@@ -0,0 +1,45 @@
+/*
+ * utility.h
+ *
+ *  Created on: 17.10.2012
+ *      Author: Thomas Heinemann
+ */
+
+#ifndef UTILITY_H_
+#define UTILITY_H_
+
+#include "src/models/dtmc.h"
+
+namespace mrmc  {
+
+namespace utility {
+
+/*!
+    Creates a DOT file which provides the graph of the DTMC.
+
+    Currently, only a version for DTMCs using probabilities of type double is provided.
+    Adaptions for other types may be included later.
+
+    @param  dtmc     The DTMC to output
+    @param  filename The Name of the file to write in. If the file already exists,
+                     it will be overwritten.
+
+ */
+void dtmcToDot(mrmc::models::Dtmc<double>* dtmc, const char* filename);
+
+/*!
+    Parses a transition file and a labeling file and produces a DTMC out of them.
+    Note that the labeling file may have at most as many nodes as the transition file!
+
+    @param tra_file String containing the location of the transition file (....tra)
+    @param lab_file String containing the location of the labeling file (....lab)
+    @returns The DTMC described by the two files.
+
+ */
+mrmc::models::Dtmc<double>* parseDTMC(const char* tra_file, const char* lab_file);
+
+} //namespace utility
+
+} //namespace mrmc
+
+#endif /* UTILITY_H_ */