diff --git a/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp b/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp
index 466cba537..3e1436ba7 100644
--- a/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp
+++ b/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp
@@ -325,7 +325,7 @@ namespace storm {
             // TODO Matthias: do not empty queue every time but break before
             while (!explorationQueue.empty()) {
                 // Get the first state in the queue
-                ExplorationHeuristicPointer currentExplorationHeuristic = explorationQueue.popTop();
+                ExplorationHeuristicPointer currentExplorationHeuristic = explorationQueue.pop();
                 StateType currentId = currentExplorationHeuristic->getId();
                 auto itFind = statesNotExplored.find(currentId);
                 STORM_LOG_ASSERT(itFind != statesNotExplored.end(), "Id " << currentId << " not found");
diff --git a/src/storm-dft/storage/BucketPriorityQueue.cpp b/src/storm-dft/storage/BucketPriorityQueue.cpp
index a591764ac..a0926e70c 100644
--- a/src/storm-dft/storage/BucketPriorityQueue.cpp
+++ b/src/storm-dft/storage/BucketPriorityQueue.cpp
@@ -7,29 +7,29 @@
 namespace storm {
     namespace storage {
 
-        template<typename ValueType>
-        BucketPriorityQueue<ValueType>::BucketPriorityQueue(size_t nrBuckets, double lowerValue, double ratio, bool higher) : lowerValue(lowerValue), higher(higher), logBase(std::log(ratio)), nrBuckets(nrBuckets), nrUnsortedItems(0), buckets(nrBuckets), currentBucket(nrBuckets) {
-            compare = ([](HeuristicPointer a, HeuristicPointer b) {
+        template<typename PriorityType>
+        BucketPriorityQueue<PriorityType>::BucketPriorityQueue(size_t nrBuckets, double lowerValue, double ratio, bool higher) : buckets(nrBuckets), currentBucket(nrBuckets), nrUnsortedItems(0), lowerValue(lowerValue), higher(higher), logBase(std::log(ratio)), nrBuckets(nrBuckets) {
+            compare = ([](PriorityTypePointer a, PriorityTypePointer b) {
                 return *a < *b;
             });
         }
 
-        template<typename ValueType>
-        void BucketPriorityQueue<ValueType>::fix() {
+        template<typename PriorityType>
+        void BucketPriorityQueue<PriorityType>::fix() {
             if (currentBucket < nrBuckets && nrUnsortedItems > buckets[currentBucket].size() / 10) {
-                // Fix current bucket
+                // Sort current bucket
                 std::make_heap(buckets[currentBucket].begin(), buckets[currentBucket].end(), compare);
                 nrUnsortedItems = 0;
             }
         }
 
-        template<typename ValueType>
-        bool BucketPriorityQueue<ValueType>::empty() const {
+        template<typename PriorityType>
+        bool BucketPriorityQueue<PriorityType>::empty() const {
             return currentBucket == nrBuckets && immediateBucket.empty();
         }
 
-        template<typename ValueType>
-        std::size_t BucketPriorityQueue<ValueType>::size() const {
+        template<typename PriorityType>
+        size_t BucketPriorityQueue<PriorityType>::size() const {
             size_t size = immediateBucket.size();
             for (size_t i = currentBucket; currentBucket < nrBuckets; ++i) {
                 size += buckets[i].size();
@@ -37,8 +37,8 @@ namespace storm {
             return size;
         }
 
-        template<typename ValueType>
-        typename BucketPriorityQueue<ValueType>::HeuristicPointer const& BucketPriorityQueue<ValueType>::top() const {
+        template<typename PriorityType>
+        typename BucketPriorityQueue<PriorityType>::PriorityTypePointer const& BucketPriorityQueue<PriorityType>::top() const {
             if (!immediateBucket.empty()) {
                 return immediateBucket.back();
             }
@@ -46,8 +46,8 @@ namespace storm {
             return buckets[currentBucket].front();
         }
 
-        template<typename ValueType>
-        void BucketPriorityQueue<ValueType>::push(HeuristicPointer const& item) {
+        template<typename PriorityType>
+        void BucketPriorityQueue<PriorityType>::push(PriorityTypePointer const& item) {
             if (item->isExpand()) {
                 immediateBucket.push_back(item);
                 return;
@@ -59,7 +59,7 @@ namespace storm {
             }
             buckets[bucket].push_back(item);
             if (bucket == currentBucket) {
-                // Insert in first bucket
+                // Inserted in first bucket
                 if (AUTOSORT) {
                     std::push_heap(buckets[currentBucket].begin(), buckets[currentBucket].end(), compare);
                 } else {
@@ -68,8 +68,8 @@ namespace storm {
             }
         }
 
-        template<typename ValueType>
-        void BucketPriorityQueue<ValueType>::update(HeuristicPointer const& item, double oldPriority) {
+        template<typename PriorityType>
+        void BucketPriorityQueue<PriorityType>::update(PriorityTypePointer const& item, double oldPriority) {
             STORM_LOG_ASSERT(!item->isExpand(), "Item is marked for expansion");
             size_t newBucket = getBucket(item->getPriority());
             size_t oldBucket = getBucket(oldPriority);
@@ -95,7 +95,7 @@ namespace storm {
                 // Remove old entry by swap-and-pop
                 if (buckets[oldBucket].size() >= 2) {
                     // Find old index by linear search
-                    // Notice: using a map to rememeber index was not efficient
+                    // Notice: using a map to remember index was not efficient
                     size_t oldIndex = 0;
                     for ( ; oldIndex < buckets[oldBucket].size(); ++oldIndex) {
                         if (buckets[oldBucket][oldIndex]->getId() == item->getId()) {
@@ -120,14 +120,16 @@ namespace storm {
         }
 
 
-        template<typename ValueType>
-        void BucketPriorityQueue<ValueType>::pop() {
+        template<typename PriorityType>
+        typename BucketPriorityQueue<PriorityType>::PriorityTypePointer BucketPriorityQueue<PriorityType>::pop() {
             if (!immediateBucket.empty()) {
+                PriorityTypePointer item = immediateBucket.back();
                 immediateBucket.pop_back();
-                return;
+                return item;
             }
             STORM_LOG_ASSERT(!empty(), "BucketPriorityQueue is empty");
             std::pop_heap(buckets[currentBucket].begin(), buckets[currentBucket].end(), compare);
+            PriorityTypePointer item = buckets[currentBucket].back();
             buckets[currentBucket].pop_back();
             if (buckets[currentBucket].empty()) {
                 // Find next bucket with elements
@@ -141,17 +143,11 @@ namespace storm {
                     }
                 }
             }
-        }
-
-        template<typename ValueType>
-        typename BucketPriorityQueue<ValueType>::HeuristicPointer BucketPriorityQueue<ValueType>::popTop() {
-            HeuristicPointer item = top();
-            pop();
             return item;
         }
 
-        template<typename ValueType>
-        size_t BucketPriorityQueue<ValueType>::getBucket(double priority) const {
+        template<typename PriorityType>
+        size_t BucketPriorityQueue<PriorityType>::getBucket(double priority) const {
             STORM_LOG_ASSERT(priority >= lowerValue, "Priority " << priority << " is too low");
 
             // For possible values greater 1
@@ -160,41 +156,39 @@ namespace storm {
             if (tmpBucket < 0) {
                 tmpBucket = 0;
             }
-            size_t newBucket = tmpBucket;
+            size_t newBucket = static_cast<size_t>(tmpBucket);
             // For values ensured to be lower 1
-            //size_t newBucket = std::log(priority - lowerValue) / logBase;
             if (newBucket >= nrBuckets) {
                 newBucket = nrBuckets - 1;
             }
             if (!higher) {
                 newBucket = nrBuckets-1 - newBucket;
             }
-            //std::cout << "get Bucket: " << priority << ", " << newBucket << std::endl;
             STORM_LOG_ASSERT(newBucket < nrBuckets, "Priority " << priority << " is too high");
             return newBucket;
         }
 
-        template<typename ValueType>
-        void BucketPriorityQueue<ValueType>::print(std::ostream& out) const {
+        template<typename PriorityType>
+        void BucketPriorityQueue<PriorityType>::print(std::ostream& out) const {
             out << "Bucket priority queue with size " << buckets.size() << ", lower value: " << lowerValue << " and logBase: " << logBase << std::endl;
             out << "Immediate bucket: ";
-            for (HeuristicPointer heuristic : immediateBucket) {
-                out << heuristic->getId() << ", ";
+            for (auto item : immediateBucket) {
+                out << item->getId() << ", ";
             }
             out << std::endl;
             out << "Current bucket (" << currentBucket << ") has " << nrUnsortedItems  << " unsorted items" << std::endl;
             for (size_t bucket = 0; bucket < buckets.size(); ++bucket) {
                 if (!buckets[bucket].empty()) {
                     out << "Bucket " << bucket << ":" << std::endl;
-                    for (HeuristicPointer heuristic : buckets[bucket]) {
-                        out << "\t" << heuristic->getId() << ": " << heuristic->getPriority() << std::endl;
+                    for (auto item : buckets[bucket]) {
+                        out << "\t" << item->getId() << ": " << item->getPriority() << std::endl;
                     }
                 }
             }
         }
 
-        template<typename ValueType>
-        void BucketPriorityQueue<ValueType>::printSizes(std::ostream& out) const {
+        template<typename PriorityType>
+        void BucketPriorityQueue<PriorityType>::printSizes(std::ostream& out) const {
             out << "Bucket sizes: " << immediateBucket.size() << " | ";
             for (size_t bucket = 0; bucket < buckets.size(); ++bucket) {
                 out << buckets[bucket].size() << " ";
@@ -203,10 +197,18 @@ namespace storm {
         }
 
         // Template instantiations
-        template class BucketPriorityQueue<double>;
+        template class BucketPriorityQueue<storm::builder::DFTExplorationHeuristic<double>>;
+        template class BucketPriorityQueue<storm::builder::DFTExplorationHeuristicNone<double>>;
+        template class BucketPriorityQueue<storm::builder::DFTExplorationHeuristicDepth<double>>;
+        template class BucketPriorityQueue<storm::builder::DFTExplorationHeuristicProbability<double>>;
+        template class BucketPriorityQueue<storm::builder::DFTExplorationHeuristicBoundDifference<double>>;
 
 #ifdef STORM_HAVE_CARL
-        template class BucketPriorityQueue<storm::RationalFunction>;
+        template class BucketPriorityQueue<storm::builder::DFTExplorationHeuristic<storm::RationalFunction>>;
+        template class BucketPriorityQueue<storm::builder::DFTExplorationHeuristicNone<storm::RationalFunction>>;
+        template class BucketPriorityQueue<storm::builder::DFTExplorationHeuristicDepth<storm::RationalFunction>>;
+        template class BucketPriorityQueue<storm::builder::DFTExplorationHeuristicProbability<storm::RationalFunction>>;
+        template class BucketPriorityQueue<storm::builder::DFTExplorationHeuristicBoundDifference<storm::RationalFunction>>;
 #endif
     }
 }
diff --git a/src/storm-dft/storage/BucketPriorityQueue.h b/src/storm-dft/storage/BucketPriorityQueue.h
index 10c753763..2c0c3cb37 100644
--- a/src/storm-dft/storage/BucketPriorityQueue.h
+++ b/src/storm-dft/storage/BucketPriorityQueue.h
@@ -10,38 +10,102 @@
 namespace storm {
     namespace storage {
 
-        template<typename ValueType>
+        /*!
+         * Priority queue based on buckets.
+         * Can be used to keep track of states during state space exploration.
+         * @tparam PriorityType Underlying priority data type
+         */
+        template<class PriorityType>
         class BucketPriorityQueue {
 
-            using HeuristicPointer = std::shared_ptr<storm::builder::DFTExplorationHeuristicDepth<ValueType>>;
+            using PriorityTypePointer = std::shared_ptr<PriorityType>;
 
         public:
+            /*!
+             * Create new priority queue.
+             * @param nrBuckets
+             * @param lowerValue
+             * @param ratio
+             * @param higher
+             */
             explicit BucketPriorityQueue(size_t nrBuckets, double lowerValue, double ratio, bool higher);
 
             void fix();
 
+            /*!
+             * Check whether queue is empty.
+             * @return True iff queue is empty.
+             */
             bool empty() const;
 
+            /*!
+             * Return number of entries.
+             * @return Size of queue.
+             */
             std::size_t size() const;
 
-            HeuristicPointer const& top() const;
+            /*!
+             * Get element with highest priority.
+             * @return Top element.
+             */
+            PriorityTypePointer const& top() const;
+
+            /*!
+             * Add element.
+             * @param item Element.
+             */
+            void push(PriorityTypePointer const& item);
+
+            /*!
+             * Update existing element.
+             * @param item Element with changes.
+             * @param oldPriority Old priority.
+             */
+            void update(PriorityTypePointer const& item, double oldPriority);
+
+            /*!
+             * Get element with highest priority and remove it from the queue.
+             * @return Top element.
+             */
+            PriorityTypePointer pop();
+
+            /*!
+             * Print info about priority queue.
+             * @param out Output stream.
+             */
+            void print(std::ostream& out) const;
 
-            void push(HeuristicPointer const& item);
+            /*!
+             * Print sizes of buckets.
+             * @param out Output stream.
+             */
+            void printSizes(std::ostream& out) const;
 
-            void update(HeuristicPointer const& item, double oldPriority);
+        private:
 
-            void pop();
+            /*!
+             * Get bucket for given priority.
+             * @param priority Priority.
+             * @return Bucket containing the priority.
+             */
+            size_t getBucket(double priority) const;
 
-            HeuristicPointer popTop();
+            // List of buckets
+            std::vector<std::vector<PriorityTypePointer>> buckets;
 
-            void print(std::ostream& out) const;
+            // Bucket containing all items which should be considered immediately
+            std::vector<PriorityTypePointer> immediateBucket;
 
-            void printSizes(std::ostream& out) const;
+            // Index of first bucket which contains items
+            size_t currentBucket;
 
-        private:
+            // Number of unsorted items in current bucket
+            size_t nrUnsortedItems;
 
-            size_t getBucket(double priority) const;
+            // Comparison function for priorities
+            std::function<bool(PriorityTypePointer, PriorityTypePointer)> compare;
 
+            // Minimal value
             const double lowerValue;
 
             const bool higher;
@@ -50,20 +114,10 @@ namespace storm {
 
             const double logBase;
 
+            // Number of available buckets
             const size_t nrBuckets;
 
-            size_t nrUnsortedItems;
-
-            // List of buckets
-            std::vector<std::vector<HeuristicPointer>> buckets;
-
-            // Bucket containing all items which should be considered immediately
-            std::vector<HeuristicPointer> immediateBucket;
-
-            // Index of first bucket which contains items
-            size_t currentBucket;
 
-            std::function<bool(HeuristicPointer, HeuristicPointer)> compare;
 
         };