diff --git a/src/storm/cli/cli.cpp b/src/storm/cli/cli.cpp
index 0f53aa2d3..fad3709af 100644
--- a/src/storm/cli/cli.cpp
+++ b/src/storm/cli/cli.cpp
@@ -353,15 +353,27 @@ namespace storm {
             return input;
         }
         
+        std::vector<std::shared_ptr<storm::logic::Formula const>> createFormulasToRespect(std::vector<storm::jani::Property> const& properties) {
+            std::vector<std::shared_ptr<storm::logic::Formula const>> result = storm::api::extractFormulasFromProperties(properties);
+            
+            for (auto const& property : properties) {
+                if (!property.getFilter().getStatesFormula()->isInitialFormula()) {
+                    result.push_back(property.getFilter().getStatesFormula());
+                }
+            }
+
+            return result;
+        }
+        
         template <storm::dd::DdType DdType, typename ValueType>
         std::shared_ptr<storm::models::ModelBase> buildModelDd(SymbolicInput const& input) {
-            return storm::api::buildSymbolicModel<DdType, ValueType>(input.model.get(), storm::api::extractFormulasFromProperties(input.properties));
+            return storm::api::buildSymbolicModel<DdType, ValueType>(input.model.get(), createFormulasToRespect(input.properties));
         }
 
         template <typename ValueType>
         std::shared_ptr<storm::models::ModelBase> buildModelSparse(SymbolicInput const& input, storm::settings::modules::IOSettings const& ioSettings) {
             auto counterexampleGeneratorSettings = storm::settings::getModule<storm::settings::modules::CounterexampleGeneratorSettings>();
-            return storm::api::buildSparseModel<ValueType>(input.model.get(), storm::api::extractFormulasFromProperties(input.properties), ioSettings.isBuildChoiceLabelsSet(), counterexampleGeneratorSettings.isMinimalCommandSetGenerationSet());
+            return storm::api::buildSparseModel<ValueType>(input.model.get(), createFormulasToRespect(input.properties), ioSettings.isBuildChoiceLabelsSet(), counterexampleGeneratorSettings.isMinimalCommandSetGenerationSet());
         }
 
         template <typename ValueType>
@@ -379,6 +391,9 @@ namespace storm {
         std::shared_ptr<storm::models::ModelBase> buildModel(storm::settings::modules::CoreSettings::Engine const& engine, SymbolicInput const& input, storm::settings::modules::IOSettings const& ioSettings) {
             storm::utility::Stopwatch modelBuildingWatch(true);
 
+            
+            // Make sure that states in filter are built as label. ALso for bisimulation.
+            
             std::shared_ptr<storm::models::ModelBase> result;
             if (input.model) {
                 if (engine == storm::settings::modules::CoreSettings::Engine::Dd || engine == storm::settings::modules::CoreSettings::Engine::Hybrid) {
@@ -622,11 +637,11 @@ namespace storm {
         };
         
         template<typename ValueType>
-        void verifyProperties(std::vector<storm::jani::Property> const& properties, std::function<std::unique_ptr<storm::modelchecker::CheckResult>(std::shared_ptr<storm::logic::Formula const> const& formula)> const& verificationCallback, std::function<void(std::unique_ptr<storm::modelchecker::CheckResult> const&)> const& postprocessingCallback = PostprocessingIdentity()) {
+        void verifyProperties(std::vector<storm::jani::Property> const& properties, std::function<std::unique_ptr<storm::modelchecker::CheckResult>(std::shared_ptr<storm::logic::Formula const> const& formula, std::shared_ptr<storm::logic::Formula const> const& states)> const& verificationCallback, std::function<void(std::unique_ptr<storm::modelchecker::CheckResult> const&)> const& postprocessingCallback = PostprocessingIdentity()) {
             for (auto const& property : properties) {
                 printModelCheckingProperty(property);
                 storm::utility::Stopwatch watch(true);
-                std::unique_ptr<storm::modelchecker::CheckResult> result = verificationCallback(property.getRawFormula());
+                std::unique_ptr<storm::modelchecker::CheckResult> result = verificationCallback(property.getRawFormula(), property.getFilter().getStatesFormula());
                 watch.stop();
                 printInitialStatesResult<ValueType>(result, property, &watch);
                 postprocessingCallback(result);
@@ -636,7 +651,8 @@ namespace storm {
         template <storm::dd::DdType DdType, typename ValueType>
         void verifyWithAbstractionRefinementEngine(SymbolicInput const& input) {
             STORM_LOG_ASSERT(input.model, "Expected symbolic model description.");
-            verifyProperties<ValueType>(input.properties, [&input] (std::shared_ptr<storm::logic::Formula const> const& formula) {
+            verifyProperties<ValueType>(input.properties, [&input] (std::shared_ptr<storm::logic::Formula const> const& formula, std::shared_ptr<storm::logic::Formula const> const& states) {
+                STORM_LOG_THROW(states->isInitialFormula(), storm::exceptions::NotSupportedException, "Abstraction-refinement can only filter initial states.");
                 return storm::api::verifyWithAbstractionRefinementEngine<DdType, ValueType>(input.model.get(), storm::api::createTask<ValueType>(formula, true));
             });
         }
@@ -645,7 +661,8 @@ namespace storm {
         void verifyWithExplorationEngine(SymbolicInput const& input) {
             STORM_LOG_ASSERT(input.model, "Expected symbolic model description.");
             STORM_LOG_THROW((std::is_same<ValueType, double>::value), storm::exceptions::NotSupportedException, "Exploration does not support other data-types than floating points.");
-            verifyProperties<ValueType>(input.properties, [&input] (std::shared_ptr<storm::logic::Formula const> const& formula) {
+            verifyProperties<ValueType>(input.properties, [&input] (std::shared_ptr<storm::logic::Formula const> const& formula, std::shared_ptr<storm::logic::Formula const> const& states) {
+                STORM_LOG_THROW(states->isInitialFormula(), storm::exceptions::NotSupportedException, "Exploration can only filter initial states.");
                 return storm::api::verifyWithExplorationEngine<ValueType>(input.model.get(), storm::api::createTask<ValueType>(formula, true));
             });
         }
@@ -654,9 +671,18 @@ namespace storm {
         void verifyWithSparseEngine(std::shared_ptr<storm::models::ModelBase> const& model, SymbolicInput const& input) {
             auto sparseModel = model->as<storm::models::sparse::Model<ValueType>>();
             verifyProperties<ValueType>(input.properties,
-                                        [&sparseModel] (std::shared_ptr<storm::logic::Formula const> const& formula) {
-                                            std::unique_ptr<storm::modelchecker::CheckResult> result = storm::api::verifyWithSparseEngine<ValueType>(sparseModel, storm::api::createTask<ValueType>(formula, true));
-                                            result->filter(storm::modelchecker::ExplicitQualitativeCheckResult(sparseModel->getInitialStates()));
+                                        [&sparseModel] (std::shared_ptr<storm::logic::Formula const> const& formula, std::shared_ptr<storm::logic::Formula const> const& states) {
+                                            bool filterForInitialStates = states->isInitialFormula();
+                                            auto task = storm::api::createTask<ValueType>(formula, filterForInitialStates);
+                                            std::unique_ptr<storm::modelchecker::CheckResult> result = storm::api::verifyWithSparseEngine<ValueType>(sparseModel, task);
+                                            
+                                            std::unique_ptr<storm::modelchecker::CheckResult> filter;
+                                            if (filterForInitialStates) {
+                                                filter = std::make_unique<storm::modelchecker::ExplicitQualitativeCheckResult>(sparseModel->getInitialStates());
+                                            } else {
+                                                filter = storm::api::verifyWithSparseEngine<ValueType>(sparseModel, storm::api::createTask<ValueType>(states, false));
+                                            }
+                                            result->filter(filter->asQualitativeCheckResult());
                                             return result;
                                         },
                                         [&sparseModel] (std::unique_ptr<storm::modelchecker::CheckResult> const& result) {
@@ -670,20 +696,42 @@ namespace storm {
 
         template <storm::dd::DdType DdType, typename ValueType>
         void verifyWithHybridEngine(std::shared_ptr<storm::models::ModelBase> const& model, SymbolicInput const& input) {
-            verifyProperties<ValueType>(input.properties, [&model] (std::shared_ptr<storm::logic::Formula const> const& formula) {
+            verifyProperties<ValueType>(input.properties, [&model] (std::shared_ptr<storm::logic::Formula const> const& formula, std::shared_ptr<storm::logic::Formula const> const& states) {
+                bool filterForInitialStates = states->isInitialFormula();
+                auto task = storm::api::createTask<ValueType>(formula, filterForInitialStates);
+                
                 auto symbolicModel = model->as<storm::models::symbolic::Model<DdType, ValueType>>();
-                std::unique_ptr<storm::modelchecker::CheckResult> result = storm::api::verifyWithHybridEngine<DdType, ValueType>(symbolicModel, storm::api::createTask<ValueType>(formula, true));
-                result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<DdType>(symbolicModel->getReachableStates(), symbolicModel->getInitialStates()));
+                std::unique_ptr<storm::modelchecker::CheckResult> result = storm::api::verifyWithHybridEngine<DdType, ValueType>(symbolicModel, task);
+                
+                std::unique_ptr<storm::modelchecker::CheckResult> filter;
+                if (filterForInitialStates) {
+                    filter = std::make_unique<storm::modelchecker::SymbolicQualitativeCheckResult<DdType>>(symbolicModel->getReachableStates(), symbolicModel->getInitialStates());
+                } else {
+                    filter = storm::api::verifyWithHybridEngine<DdType, ValueType>(symbolicModel, storm::api::createTask<ValueType>(states, false));
+                }
+                
+                result->filter(filter->asQualitativeCheckResult());
                 return result;
             });
         }
 
         template <storm::dd::DdType DdType, typename ValueType>
         void verifyWithDdEngine(std::shared_ptr<storm::models::ModelBase> const& model, SymbolicInput const& input) {
-            verifyProperties<ValueType>(input.properties, [&model] (std::shared_ptr<storm::logic::Formula const> const& formula) {
+            verifyProperties<ValueType>(input.properties, [&model] (std::shared_ptr<storm::logic::Formula const> const& formula, std::shared_ptr<storm::logic::Formula const> const& states) {
+                bool filterForInitialStates = states->isInitialFormula();
+                auto task = storm::api::createTask<ValueType>(formula, filterForInitialStates);
+
                 auto symbolicModel = model->as<storm::models::symbolic::Model<DdType, ValueType>>();
                 std::unique_ptr<storm::modelchecker::CheckResult> result = storm::api::verifyWithDdEngine<DdType, ValueType>(model->as<storm::models::symbolic::Model<DdType, ValueType>>(), storm::api::createTask<ValueType>(formula, true));
-                result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<DdType>(symbolicModel->getReachableStates(), symbolicModel->getInitialStates()));
+
+                std::unique_ptr<storm::modelchecker::CheckResult> filter;
+                if (filterForInitialStates) {
+                    filter = std::make_unique<storm::modelchecker::SymbolicQualitativeCheckResult<DdType>>(symbolicModel->getReachableStates(), symbolicModel->getInitialStates());
+                } else {
+                    filter = storm::api::verifyWithDdEngine<DdType, ValueType>(symbolicModel, storm::api::createTask<ValueType>(states, false));
+                }
+                
+                result->filter(filter->asQualitativeCheckResult());
                 return result;
             });
         }
diff --git a/src/storm/logic/Formula.cpp b/src/storm/logic/Formula.cpp
index 9038a2307..3f871908e 100644
--- a/src/storm/logic/Formula.cpp
+++ b/src/storm/logic/Formula.cpp
@@ -175,6 +175,10 @@ namespace storm {
             return std::shared_ptr<Formula const>(new BooleanLiteralFormula(true));
         }
         
+        bool Formula::isInitialFormula() const {
+            return this->isAtomicLabelFormula() && this->asAtomicLabelFormula().getLabel() == "init";
+        }
+        
         PathFormula& Formula::asPathFormula() {
             return dynamic_cast<PathFormula&>(*this);
         }
diff --git a/src/storm/logic/Formula.h b/src/storm/logic/Formula.h
index 2ad5e9477..a76dd0ef7 100644
--- a/src/storm/logic/Formula.h
+++ b/src/storm/logic/Formula.h
@@ -93,10 +93,12 @@ namespace storm {
             
             bool isInFragment(FragmentSpecification const& fragment) const;
             FormulaInformation info() const;
-            
+
             virtual boost::any accept(FormulaVisitor const& visitor, boost::any const& data = boost::any()) const = 0;
             
             static std::shared_ptr<Formula const> getTrueFormula();
+
+            bool isInitialFormula() const;
             
             PathFormula& asPathFormula();
             PathFormula const& asPathFormula() const;
diff --git a/src/storm/parser/FormulaParserGrammar.cpp b/src/storm/parser/FormulaParserGrammar.cpp
index bee6b5117..78102f859 100644
--- a/src/storm/parser/FormulaParserGrammar.cpp
+++ b/src/storm/parser/FormulaParserGrammar.cpp
@@ -128,7 +128,7 @@ namespace storm {
 #pragma clang diagnostic push
 #pragma clang diagnostic ignored "-Woverloaded-shift-op-parentheses"
             
-            filterProperty = (-formulaName >> qi::lit("filter") > qi::lit("(") > filterType_ > qi::lit(",") > stateFormula > -(qi::lit(",") > qi::lit("\"init\"") > qi::lit(")")))[qi::_val = phoenix::bind(&FormulaParserGrammar::createProperty, phoenix::ref(*this), qi::_1, qi::_2, qi::_3)] | (-formulaName >> stateFormula)[qi::_val = phoenix::bind(&FormulaParserGrammar::createPropertyWithDefaultFilterType, phoenix::ref(*this), qi::_1, qi::_2)];
+            filterProperty = (-formulaName >> qi::lit("filter") > qi::lit("(") > filterType_ > qi::lit(",") > stateFormula > qi::lit(",") > stateFormula > qi::lit(")"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createProperty, phoenix::ref(*this), qi::_1, qi::_2, qi::_3, qi::_4)] | (-formulaName >> stateFormula)[qi::_val = phoenix::bind(&FormulaParserGrammar::createPropertyWithDefaultFilterTypeAndStates, phoenix::ref(*this), qi::_1, qi::_2)];
             filterProperty.name("filter property");
 
 #pragma clang diagnostic pop
@@ -332,8 +332,8 @@ namespace storm {
             return std::shared_ptr<storm::logic::Formula const>(new storm::logic::MultiObjectiveFormula(subformulas));
         }
                                                
-        storm::jani::Property FormulaParserGrammar::createProperty(boost::optional<std::string> const& propertyName, storm::modelchecker::FilterType const& filterType, std::shared_ptr<storm::logic::Formula const> const& formula) {
-            storm::jani::FilterExpression filterExpression(formula, filterType);
+        storm::jani::Property FormulaParserGrammar::createProperty(boost::optional<std::string> const& propertyName, storm::modelchecker::FilterType const& filterType, std::shared_ptr<storm::logic::Formula const> const& formula, std::shared_ptr<storm::logic::Formula const> const& states) {
+            storm::jani::FilterExpression filterExpression(formula, filterType, states);
             
             ++propertyCount;
             if (propertyName) {
@@ -343,7 +343,7 @@ namespace storm {
             }
         }
                                                
-        storm::jani::Property FormulaParserGrammar::createPropertyWithDefaultFilterType(boost::optional<std::string> const& propertyName, std::shared_ptr<storm::logic::Formula const> const& formula) {
+        storm::jani::Property FormulaParserGrammar::createPropertyWithDefaultFilterTypeAndStates(boost::optional<std::string> const& propertyName, std::shared_ptr<storm::logic::Formula const> const& formula) {
             ++propertyCount;
             if (propertyName) {
                 return storm::jani::Property(propertyName.get(), formula);
diff --git a/src/storm/parser/FormulaParserGrammar.h b/src/storm/parser/FormulaParserGrammar.h
index 79b272246..7ae6740b8 100644
--- a/src/storm/parser/FormulaParserGrammar.h
+++ b/src/storm/parser/FormulaParserGrammar.h
@@ -223,8 +223,8 @@ namespace storm {
             std::shared_ptr<storm::logic::Formula const> createUnaryBooleanStateFormula(std::shared_ptr<storm::logic::Formula const> const& subformula, boost::optional<storm::logic::UnaryBooleanStateFormula::OperatorType> const& operatorType);
             std::shared_ptr<storm::logic::Formula const> createMultiObjectiveFormula(std::vector<std::shared_ptr<storm::logic::Formula const>> const& subformulas);
             
-            storm::jani::Property createProperty(boost::optional<std::string> const& propertyName, storm::modelchecker::FilterType const& filterType, std::shared_ptr<storm::logic::Formula const> const& formula);
-            storm::jani::Property createPropertyWithDefaultFilterType(boost::optional<std::string> const& propertyName, std::shared_ptr<storm::logic::Formula const> const& formula);
+            storm::jani::Property createProperty(boost::optional<std::string> const& propertyName, storm::modelchecker::FilterType const& filterType, std::shared_ptr<storm::logic::Formula const> const& formula, std::shared_ptr<storm::logic::Formula const> const& states);
+            storm::jani::Property createPropertyWithDefaultFilterTypeAndStates(boost::optional<std::string> const& propertyName, std::shared_ptr<storm::logic::Formula const> const& formula);
             
             // An error handler function.
             phoenix::function<SpiritErrorHandler> handler;
diff --git a/src/storm/storage/jani/Property.cpp b/src/storm/storage/jani/Property.cpp
index e46d2ee50..73c6d0dec 100644
--- a/src/storm/storage/jani/Property.cpp
+++ b/src/storm/storage/jani/Property.cpp
@@ -5,19 +5,17 @@ namespace storm {
         
         
         std::ostream& operator<<(std::ostream& os, FilterExpression const& fe) {
-            return os << "Obtain " << toString(fe.getFilterType()) << " of the 'initial'-states with values described by '" << *fe.getFormula() << "'";
+            return os << "Obtain " << toString(fe.getFilterType()) << " of the '" << fe.getStatesFormula() << "'-states with values described by '" << *fe.getFormula() << "'";
         }
         
         Property::Property(std::string const& name, std::shared_ptr<storm::logic::Formula const> const& formula, std::string const& comment)
-        : name(name), comment(comment), filterExpression(FilterExpression(formula))
-        {
-
+        : name(name), comment(comment), filterExpression(FilterExpression(formula)) {
+            // Intentionally left empty.
         }
         
         Property::Property(std::string const& name, FilterExpression const& fe, std::string const& comment)
-        : name(name), comment(comment), filterExpression(fe)
-        {
-            
+        : name(name), comment(comment), filterExpression(fe) {
+            // Intentionally left empty.
         }
 
         std::string const& Property::getName() const {
@@ -48,6 +46,5 @@ namespace storm {
             return os << "(" << p.getName() << ") : " << p.getFilter();
         }
         
-
     }
 }
diff --git a/src/storm/storage/jani/Property.h b/src/storm/storage/jani/Property.h
index 52db07fef..74aceab5c 100644
--- a/src/storm/storage/jani/Property.h
+++ b/src/storm/storage/jani/Property.h
@@ -2,6 +2,10 @@
 
 #include "storm/modelchecker/results/FilterType.h"
 #include "storm/logic/Formulas.h"
+#include "storm/logic/FragmentSpecification.h"
+
+#include "storm/utility/macros.h"
+#include "storm/exceptions/InvalidArgumentException.h"
 
 namespace storm {
     namespace jani {
@@ -30,28 +34,35 @@ namespace storm {
         public:
             FilterExpression() = default;
             
-            explicit FilterExpression(std::shared_ptr<storm::logic::Formula const> formula, storm::modelchecker::FilterType ft = storm::modelchecker::FilterType::VALUES) : formula(formula), ft(ft) {}
+            explicit FilterExpression(std::shared_ptr<storm::logic::Formula const> formula, storm::modelchecker::FilterType ft = storm::modelchecker::FilterType::VALUES, std::shared_ptr<storm::logic::Formula const> const& statesFormula = std::make_shared<storm::logic::AtomicLabelFormula>("init")) : formula(formula), ft(ft), statesFormula(statesFormula) {
+                STORM_LOG_THROW(statesFormula->isInFragment(storm::logic::propositional()), storm::exceptions::InvalidArgumentException, "Can only filter by propositional formula.");
+            }
             
             std::shared_ptr<storm::logic::Formula const> const& getFormula() const {
                 return formula;
             }
             
+            std::shared_ptr<storm::logic::Formula const> const& getStatesFormula() const {
+                return statesFormula;
+            }
+
             storm::modelchecker::FilterType getFilterType() const {
                 return ft;
             }
             
             FilterExpression substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const {
-                return FilterExpression(formula->substitute(substitution), ft);
+                return FilterExpression(formula->substitute(substitution), ft, statesFormula->substitute(substitution));
             }
             
             FilterExpression substituteLabels(std::map<std::string, std::string> const& labelSubstitution) const {
-                return FilterExpression(formula->substitute(labelSubstitution), ft);
+                return FilterExpression(formula->substitute(labelSubstitution), ft, statesFormula->substitute(labelSubstitution));
             }
 
         private:
             // For now, we assume that the states are always the initial states.
             std::shared_ptr<storm::logic::Formula const> formula;
             storm::modelchecker::FilterType ft;
+            std::shared_ptr<storm::logic::Formula const> statesFormula;
         };