diff --git a/src/storm-parsers/parser/PrismParser.cpp b/src/storm-parsers/parser/PrismParser.cpp
index 4c0edbb34..f0ce8d71c 100644
--- a/src/storm-parsers/parser/PrismParser.cpp
+++ b/src/storm-parsers/parser/PrismParser.cpp
@@ -85,8 +85,6 @@ namespace storm {
             
             modelTypeDefinition %= modelType_;
             modelTypeDefinition.name("model type");
-
-
             
             undefinedBooleanConstantDefinition = ((qi::lit("const") >> qi::lit("bool")) > identifier > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createUndefinedBooleanConstant, phoenix::ref(*this), qi::_1)];
             undefinedBooleanConstantDefinition.name("undefined boolean constant declaration");
@@ -121,7 +119,10 @@ namespace storm {
             integerVariableDefinition = ((identifier >> qi::lit(":") >> qi::lit("[")) > expression_ > qi::lit("..") > expression_ > qi::lit("]") > -(qi::lit("init") > expression_[qi::_a = qi::_1]) > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createIntegerVariable, phoenix::ref(*this), qi::_1, qi::_2, qi::_3, qi::_a)];
             integerVariableDefinition.name("integer variable definition");
             
-            variableDefinition = (booleanVariableDefinition[phoenix::push_back(qi::_r1, qi::_1)] | integerVariableDefinition[phoenix::push_back(qi::_r2, qi::_1)]);
+            clockVariableDefinition = ((identifier >> qi::lit(":") >> qi::lit("clock")) > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createClockVariable, phoenix::ref(*this), qi::_1)];
+            clockVariableDefinition.name("clock variable definition");
+            
+            variableDefinition = (booleanVariableDefinition[phoenix::push_back(qi::_r1, qi::_1)] | integerVariableDefinition[phoenix::push_back(qi::_r2, qi::_1)] | clockVariableDefinition[phoenix::push_back(qi::_r3, qi::_1)]);
             variableDefinition.name("variable declaration");
             
             globalVariableDefinition = (qi::lit("global") > (booleanVariableDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::globalBooleanVariables, qi::_r1), qi::_1)] | integerVariableDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::globalIntegerVariables, qi::_r1), qi::_1)]));
@@ -150,6 +151,9 @@ namespace storm {
             observablesConstruct = (qi::lit("observables") > (identifier % qi::lit(",") )> qi::lit("endobservables"))[phoenix::bind(&PrismParser::createObservablesList, phoenix::ref(*this), qi::_1)];
             observablesConstruct.name("observables construct");
             
+            invariantConstruct = (qi::lit("invariant") > expression_ > qi::lit("endinvariant"))[qi::_val = qi::_1];
+            invariantConstruct.name("invariant construct");
+
             systemCompositionConstruct = (qi::lit("system") > parallelComposition > qi::lit("endsystem"))[phoenix::bind(&PrismParser::addSystemCompositionConstruct, phoenix::ref(*this), qi::_1, qi::_r1)];
             systemCompositionConstruct.name("system composition construct");
             
@@ -211,8 +215,8 @@ namespace storm {
                                  > +(qi::char_ - qi::lit(";"))
                                  > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createDummyCommand, phoenix::ref(*this), qi::_1, qi::_r1)];
             commandDefinition.name("command definition");
-            
-            moduleDefinition = ((qi::lit("module") >> identifier >> *(variableDefinition(qi::_a, qi::_b))) > *commandDefinition(qi::_r1) > qi::lit("endmodule"))[qi::_val = phoenix::bind(&PrismParser::createModule, phoenix::ref(*this), qi::_1, qi::_a, qi::_b, qi::_2, qi::_r1)];
+
+            moduleDefinition = ((qi::lit("module") >> identifier >> *(variableDefinition(qi::_a, qi::_b, qi::_c))) > -invariantConstruct > (*commandDefinition(qi::_r1)) > qi::lit("endmodule"))[qi::_val = phoenix::bind(&PrismParser::createModule, phoenix::ref(*this), qi::_1, qi::_a, qi::_b, qi::_c, qi::_2, qi::_3, qi::_r1)];
             moduleDefinition.name("module definition");
             
             moduleRenaming = ((qi::lit("module") >> identifier >> qi::lit("=")) > identifier > qi::lit("[")
@@ -249,6 +253,7 @@ namespace storm {
             qi::on_success(definedDoubleConstantDefinition, setLocationInfoFunction);
             qi::on_success(booleanVariableDefinition, setLocationInfoFunction);
             qi::on_success(integerVariableDefinition, setLocationInfoFunction);
+            qi::on_success(clockVariableDefinition, setLocationInfoFunction);
             qi::on_success(moduleDefinition, setLocationInfoFunction);
             qi::on_success(moduleRenaming, setLocationInfoFunction);
             qi::on_success(formulaDefinition, setLocationInfoFunction);
@@ -585,15 +590,36 @@ namespace storm {
 
             return storm::prism::IntegerVariable(manager->getVariable(variableName), lowerBoundExpression, upperBoundExpression, initialValueExpression, observable, this->getFilename());
         }
+        
+        storm::prism::ClockVariable PrismParser::createClockVariable(std::string const& variableName) const {
+            if (!this->secondRun) {
+                try {
+                    storm::expressions::Variable newVariable = manager->declareRationalVariable(variableName);
+                    this->identifiers_.add(variableName, newVariable.getExpression());
+                } catch (storm::exceptions::InvalidArgumentException const& e) {
+                    if (manager->hasVariable(variableName)) {
+                        STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Duplicate identifier '" << variableName << "'.");
+                    } else {
+                        STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": illegal identifier '" << variableName << "'.");
+                    }
+                }
+            }
+            bool observable = this->observables.count(variableName) > 0;
+            if(observable) {
+                this->observables.erase(variableName);
+            }
+
+            return storm::prism::ClockVariable(manager->getVariable(variableName), observable, this->getFilename());
+        }
 
         void PrismParser::createObservablesList(std::vector<std::string> const& observables) {
             this->observables.insert(observables.begin(), observables.end());
             // We need this list to be filled in both runs.
         }
         
-        storm::prism::Module PrismParser::createModule(std::string const& moduleName, std::vector<storm::prism::BooleanVariable> const& booleanVariables, std::vector<storm::prism::IntegerVariable> const& integerVariables, std::vector<storm::prism::Command> const& commands, GlobalProgramInformation& globalProgramInformation) const {
+        storm::prism::Module PrismParser::createModule(std::string const& moduleName, std::vector<storm::prism::BooleanVariable> const& booleanVariables, std::vector<storm::prism::IntegerVariable> const& integerVariables, std::vector<storm::prism::ClockVariable> const& clockVariables, boost::optional<storm::expressions::Expression> const& invariant, std::vector<storm::prism::Command> const& commands, GlobalProgramInformation& globalProgramInformation) const {
             globalProgramInformation.moduleToIndexMap[moduleName] = globalProgramInformation.modules.size();
-            return storm::prism::Module(moduleName, booleanVariables, integerVariables, commands, this->getFilename());
+            return storm::prism::Module(moduleName, booleanVariables, integerVariables, clockVariables, invariant.is_initialized()? invariant.get() : storm::expressions::Expression(), commands, this->getFilename());
         }
         
         storm::prism::Module PrismParser::createRenamedModule(std::string const& newModuleName, std::string const& oldModuleName, std::map<std::string, std::string> const& renaming, GlobalProgramInformation& globalProgramInformation) const {
@@ -622,6 +648,15 @@ namespace storm {
                         this->observables.erase(renamingPair->second);
                     }
                 }
+                for (auto const& variable : moduleToRename.getClockVariables()) {
+                    auto const& renamingPair = renaming.find(variable.getName());
+                    STORM_LOG_THROW(renamingPair != renaming.end(), storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Clock variable '" << variable.getName() << " was not renamed.");
+                    storm::expressions::Variable renamedVariable = manager->declareRationalVariable(renamingPair->second);
+                    this->identifiers_.add(renamingPair->second, renamedVariable.getExpression());
+                    if(this->observables.count(renamingPair->second) > 0) {
+                        this->observables.erase(renamingPair->second);
+                    }
+                }
                 
                 for (auto const& command : moduleToRename.getCommands()) {
                     std::string newActionName = command.getActionName();
@@ -677,6 +712,24 @@ namespace storm {
                     }
                     integerVariables.push_back(storm::prism::IntegerVariable(manager->getVariable(renamingPair->second), variable.getLowerBoundExpression().substitute(expressionRenaming), variable.getUpperBoundExpression().substitute(expressionRenaming), variable.hasInitialValue() ? variable.getInitialValueExpression().substitute(expressionRenaming) : variable.getInitialValueExpression(), observable, this->getFilename(), get_line(qi::_1)));
                 }
+
+                // Rename the clock variables.
+                std::vector<storm::prism::ClockVariable> clockVariables;
+                for (auto const& variable : moduleToRename.getClockVariables()) {
+                    auto const& renamingPair = renaming.find(variable.getName());
+                    STORM_LOG_THROW(renamingPair != renaming.end(), storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Clock variable '" << variable.getName() << " was not renamed.");
+                    bool observable = this->observables.count(renamingPair->second) > 0;
+                    if (observable) {
+                        this->observables.erase(renamingPair->second);
+                    }
+                    clockVariables.push_back(storm::prism::ClockVariable(manager->getVariable(renamingPair->second), observable, this->getFilename(), get_line(qi::_1)));
+                }
+                
+                // Rename invariant (if present)
+                storm::expressions::Expression invariant;
+                if (moduleToRename.hasInvariant()) {
+                    invariant = moduleToRename.getInvariant().substitute(expressionRenaming);
+                }
                 
                 // Rename commands.
                 std::vector<storm::prism::Command> commands;
@@ -716,7 +769,7 @@ namespace storm {
                     ++globalProgramInformation.currentCommandIndex;
                 }
                 
-                return storm::prism::Module(newModuleName, booleanVariables, integerVariables, commands, oldModuleName, renaming);
+                return storm::prism::Module(newModuleName, booleanVariables, integerVariables, clockVariables, invariant, commands, oldModuleName, renaming);
             }
         }
         
diff --git a/src/storm-parsers/parser/PrismParser.h b/src/storm-parsers/parser/PrismParser.h
index a5367d2c6..7a53bd359 100644
--- a/src/storm-parsers/parser/PrismParser.h
+++ b/src/storm-parsers/parser/PrismParser.h
@@ -98,7 +98,8 @@ namespace storm {
                     ("mdp", storm::prism::Program::ModelType::MDP)
                     ("ctmdp", storm::prism::Program::ModelType::CTMDP)
                     ("ma", storm::prism::Program::ModelType::MA)
-                    ("pomdp", storm::prism::Program::ModelType::POMDP);
+                    ("pomdp", storm::prism::Program::ModelType::POMDP)
+                    ("pta", storm::prism::Program::ModelType::PTA);
                 }
             };
             
@@ -111,21 +112,24 @@ namespace storm {
                     ("ctmdp", 4)
                     ("ma", 5)
                     ("pomdp", 6)
-                    ("const", 7)
-                    ("int", 8)
-                    ("bool", 9)
-                    ("module", 10)
-                    ("endmodule", 11)
-                    ("rewards", 12)
-                    ("endrewards", 13)
-                    ("true", 14)
-                    ("false", 15)
-                    ("min", 16)
-                    ("max", 17)
-                    ("floor", 18)
-                    ("ceil", 19)
-                    ("init", 20)
-                    ("endinit", 21);
+                    ("pta", 7)
+                    ("const", 8)
+                    ("int", 9)
+                    ("bool", 10)
+                    ("module", 11)
+                    ("endmodule", 12)
+                    ("rewards", 13)
+                    ("endrewards", 14)
+                    ("true", 15)
+                    ("false", 16)
+                    ("min", 17)
+                    ("max", 18)
+                    ("floor", 19)
+                    ("ceil", 20)
+                    ("init", 21)
+                    ("endinit", 22)
+                    ("invariant", 23)
+                    ("endinvariant", 24);
                 }
             };
             
@@ -213,13 +217,14 @@ namespace storm {
             
             // Rules for modules definition.
             qi::rule<Iterator, std::vector<storm::prism::Module>(GlobalProgramInformation&), Skipper> moduleDefinitionList;
-            qi::rule<Iterator, storm::prism::Module(GlobalProgramInformation&), qi::locals<std::vector<storm::prism::BooleanVariable>, std::vector<storm::prism::IntegerVariable>>, Skipper> moduleDefinition;
+            qi::rule<Iterator, storm::prism::Module(GlobalProgramInformation&), qi::locals<std::vector<storm::prism::BooleanVariable>, std::vector<storm::prism::IntegerVariable>, std::vector<storm::prism::ClockVariable>>, Skipper> moduleDefinition;
             qi::rule<Iterator, storm::prism::Module(GlobalProgramInformation&), qi::locals<std::map<std::string, std::string>>, Skipper> moduleRenaming;
             
             // Rules for variable definitions.
-            qi::rule<Iterator, qi::unused_type(std::vector<storm::prism::BooleanVariable>&, std::vector<storm::prism::IntegerVariable>&), Skipper> variableDefinition;
+            qi::rule<Iterator, qi::unused_type(std::vector<storm::prism::BooleanVariable>&, std::vector<storm::prism::IntegerVariable>&, std::vector<storm::prism::ClockVariable>&), Skipper> variableDefinition;
             qi::rule<Iterator, storm::prism::BooleanVariable(), qi::locals<storm::expressions::Expression>, Skipper> booleanVariableDefinition;
             qi::rule<Iterator, storm::prism::IntegerVariable(), qi::locals<storm::expressions::Expression>, Skipper> integerVariableDefinition;
+            qi::rule<Iterator, storm::prism::ClockVariable(), qi::locals<storm::expressions::Expression>, Skipper> clockVariableDefinition;
             
             // Rules for command definitions.
             qi::rule<Iterator, storm::prism::Command(GlobalProgramInformation&), qi::locals<bool>, Skipper> commandDefinition;
@@ -238,6 +243,9 @@ namespace storm {
             qi::rule<Iterator, qi::unused_type(GlobalProgramInformation&), Skipper> initialStatesConstruct;
 
             qi::rule<Iterator, qi::unused_type(), Skipper> observablesConstruct;
+            
+            // Rules for invariant constructs
+            qi::rule<Iterator, storm::expressions::Expression(), Skipper> invariantConstruct;
 
             // Rules for the system composition.
             qi::rule<Iterator, qi::unused_type(GlobalProgramInformation&), Skipper> systemCompositionConstruct;
@@ -303,7 +311,8 @@ namespace storm {
             storm::prism::Command createDummyCommand(boost::optional<std::string> const& actionName, GlobalProgramInformation& globalProgramInformation) const;
             storm::prism::BooleanVariable createBooleanVariable(std::string const& variableName, storm::expressions::Expression initialValueExpression) const;
             storm::prism::IntegerVariable createIntegerVariable(std::string const& variableName, storm::expressions::Expression lowerBoundExpression, storm::expressions::Expression upperBoundExpression, storm::expressions::Expression initialValueExpression) const;
-            storm::prism::Module createModule(std::string const& moduleName, std::vector<storm::prism::BooleanVariable> const& booleanVariables, std::vector<storm::prism::IntegerVariable> const& integerVariables, std::vector<storm::prism::Command> const& commands, GlobalProgramInformation& globalProgramInformation) const;
+            storm::prism::ClockVariable createClockVariable(std::string const& variableName) const;
+            storm::prism::Module createModule(std::string const& moduleName, std::vector<storm::prism::BooleanVariable> const& booleanVariables, std::vector<storm::prism::IntegerVariable> const& integerVariables, std::vector<storm::prism::ClockVariable> const& clockVariables, boost::optional<storm::expressions::Expression> const& invariant, std::vector<storm::prism::Command> const& commands, GlobalProgramInformation& globalProgramInformation) const;
             storm::prism::Module createRenamedModule(std::string const& newModuleName, std::string const& oldModuleName, std::map<std::string, std::string> const& renaming, GlobalProgramInformation& globalProgramInformation) const;
             storm::prism::Program createProgram(GlobalProgramInformation const& globalProgramInformation) const;
             void createObservablesList(std::vector<std::string> const& observables);
diff --git a/src/storm/storage/jani/ArrayEliminator.cpp b/src/storm/storage/jani/ArrayEliminator.cpp
index 244eaa0b5..4e5c975b0 100644
--- a/src/storm/storage/jani/ArrayEliminator.cpp
+++ b/src/storm/storage/jani/ArrayEliminator.cpp
@@ -404,6 +404,7 @@ namespace storm {
             public:
 
                 typedef ArrayEliminatorData ResultType;
+                using JaniTraverser::traverse;
                 
                 ArrayVariableReplacer(storm::expressions::ExpressionManager& expressionManager, bool keepNonTrivialArrayAccess, std::unordered_map<storm::expressions::Variable, std::size_t> const& arrayVarToSizesMap) : expressionManager(expressionManager) , keepNonTrivialArrayAccess(keepNonTrivialArrayAccess), arraySizes(arrayVarToSizesMap) {}
                 
@@ -470,19 +471,27 @@ namespace storm {
                     arrayExprEliminator = std::make_unique<ArrayExpressionEliminationVisitor>(replacements, arraySizes);
                     
                     for (auto& loc : automaton.getLocations()) {
-                        JaniTraverser::traverse(loc, data);
+                        traverse(loc, data);
                     }
-                    JaniTraverser::traverse(automaton.getEdgeContainer(), data);
+                    traverse(automaton.getEdgeContainer(), data);
                     
                     if (automaton.hasInitialStatesRestriction()) {
                         automaton.setInitialStatesRestriction(arrayExprEliminator->eliminate(automaton.getInitialStatesRestriction()));
                     }
                 }
-         
+
+                virtual void traverse(Location& location, boost::any const& data) override {
+                    traverse(location.getAssignments(), data);
+                    if (location.hasTimeProgressInvariant()) {
+                        location.setTimeProgressInvariant(arrayExprEliminator->eliminate(location.getTimeProgressInvariant()));
+                        traverse(location.getTimeProgressInvariant(), data);
+                    }
+                }
+
                 void traverse(TemplateEdge& templateEdge, boost::any const& data) override {
                     templateEdge.setGuard(arrayExprEliminator->eliminate(templateEdge.getGuard()));
                     for (auto& dest : templateEdge.getDestinations()) {
-                        JaniTraverser::traverse(dest, data);
+                        traverse(dest, data);
                     }
                     traverse(templateEdge.getAssignments(), data);
                 }
@@ -493,7 +502,7 @@ namespace storm {
                         edge.setRate(arrayExprEliminator->eliminate(edge.getRate()));
                     }
                     for (auto& dest : edge.getDestinations()) {
-                        JaniTraverser::traverse(dest, data);
+                        traverse(dest, data);
                     }
                 }
                 
diff --git a/src/storm/storage/jani/Automaton.cpp b/src/storm/storage/jani/Automaton.cpp
index 37924c221..beba4b92e 100644
--- a/src/storm/storage/jani/Automaton.cpp
+++ b/src/storm/storage/jani/Automaton.cpp
@@ -36,6 +36,8 @@ namespace storm {
                 return addVariable(variable.asRealVariable());
             } else if (variable.isArrayVariable()) {
                 return addVariable(variable.asArrayVariable());
+            } else if (variable.isClockVariable()) {
+                return addVariable(variable.asClockVariable());
             } else {
                 STORM_LOG_THROW(false, storm::exceptions::InvalidTypeException, "Variable has invalid type.");
             }
@@ -60,6 +62,10 @@ namespace storm {
         ArrayVariable const& Automaton::addVariable(ArrayVariable const& variable) {
             return variables.addVariable(variable);
         }
+        
+        ClockVariable const& Automaton::addVariable(ClockVariable const& variable) {
+            return variables.addVariable(variable);
+        }
 
         bool Automaton::hasVariable(std::string const& name) const {
             return variables.hasVariable(name);
@@ -440,6 +446,9 @@ namespace storm {
             for (auto& variable : this->getVariables().getArrayVariables()) {
                 variable.substitute(substitution);
             }
+            for (auto& variable : this->getVariables().getClockVariables()) {
+                variable.substitute(substitution);
+            }
             
             for (auto& location : this->getLocations()) {
                 location.substitute(substitution);
diff --git a/src/storm/storage/jani/Automaton.h b/src/storm/storage/jani/Automaton.h
index 0dd74eeb9..809ddb1cc 100644
--- a/src/storm/storage/jani/Automaton.h
+++ b/src/storm/storage/jani/Automaton.h
@@ -75,6 +75,11 @@ namespace storm {
              */
             ArrayVariable const& addVariable(ArrayVariable const& variable);
 
+            /*!
+             * Adds the given array variable to this automaton.
+             */
+            ClockVariable const& addVariable(ClockVariable const& variable);
+
             /*!
              * Retrieves the variables of this automaton.
              */
diff --git a/src/storm/storage/jani/ClockVariable.cpp b/src/storm/storage/jani/ClockVariable.cpp
new file mode 100644
index 000000000..17340892a
--- /dev/null
+++ b/src/storm/storage/jani/ClockVariable.cpp
@@ -0,0 +1,32 @@
+#include "storm/storage/jani/ClockVariable.h"
+
+namespace storm {
+    namespace jani {
+        
+        ClockVariable::ClockVariable(std::string const& name, storm::expressions::Variable const& variable) : Variable(name, variable) {
+            // Intentionally left empty.
+        }
+        
+        ClockVariable::ClockVariable(std::string const& name, storm::expressions::Variable const& variable, storm::expressions::Expression const& initValue, bool transient) : Variable(name, variable, initValue, transient) {
+            // Intentionally left empty.
+        }
+        
+        std::unique_ptr<Variable> ClockVariable::clone() const {
+            return std::make_unique<ClockVariable>(*this);
+        }
+        
+        bool ClockVariable::isClockVariable() const {
+            return true;
+        }
+        
+        std::shared_ptr<ClockVariable> makeClockVariable(std::string const& name, storm::expressions::Variable const& variable, boost::optional<storm::expressions::Expression> initValue, bool transient) {
+            if (initValue) {
+                return std::make_shared<ClockVariable>(name, variable, initValue.get(), transient);
+            } else {
+                assert(!transient);
+                return std::make_shared<ClockVariable>(name, variable);
+            }
+        }
+        
+    }
+}
diff --git a/src/storm/storage/jani/ClockVariable.h b/src/storm/storage/jani/ClockVariable.h
new file mode 100644
index 000000000..cf32a6b24
--- /dev/null
+++ b/src/storm/storage/jani/ClockVariable.h
@@ -0,0 +1,32 @@
+#pragma once
+
+#include "storm/storage/jani/Variable.h"
+
+namespace storm {
+    namespace jani {
+        
+        class ClockVariable : public Variable {
+        public:
+            
+            /*!
+             * Creates a clock variable
+             */
+            ClockVariable(std::string const& name, storm::expressions::Variable const& variable);
+            
+            /*!
+             * Creates a clock variable with initial value
+             */
+            ClockVariable(std::string const& name, storm::expressions::Variable const& variable, storm::expressions::Expression const& initialValue, bool transient=false);
+            
+            virtual std::unique_ptr<Variable> clone() const override;
+            
+            virtual bool isClockVariable() const override;
+        };
+        
+        /**
+         * Convenience function to call the appropriate constructor and return a shared pointer to the variable.
+         */
+        std::shared_ptr<ClockVariable> makeClockVariable(std::string const& name, storm::expressions::Variable const& variable, boost::optional<storm::expressions::Expression> initValue, bool transient);
+        
+    }
+}
diff --git a/src/storm/storage/jani/FunctionEliminator.cpp b/src/storm/storage/jani/FunctionEliminator.cpp
index 32a9895de..c81ffbeae 100644
--- a/src/storm/storage/jani/FunctionEliminator.cpp
+++ b/src/storm/storage/jani/FunctionEliminator.cpp
@@ -200,6 +200,8 @@ namespace storm {
 
             class FunctionEliminatorTraverser : public JaniTraverser {
             public:
+                
+                using JaniTraverser::traverse;
 
                 FunctionEliminatorTraverser() = default;
                 
@@ -277,7 +279,7 @@ namespace storm {
                     for (auto& c : model.getConstants()) {
                         traverse(c, &globalFunctionEliminationVisitor);
                     }
-                    JaniTraverser::traverse(model.getGlobalVariables(), &globalFunctionEliminationVisitor);
+                    traverse(model.getGlobalVariables(), &globalFunctionEliminationVisitor);
                     for (auto& aut : model.getAutomata()) {
                         traverse(aut, &globalFunctionEliminationVisitor);
                     }
@@ -295,16 +297,24 @@ namespace storm {
                     eliminateFunctionsInFunctionBodies(functionEliminationVisitor, automaton.getFunctionDefinitions());
                     
                     // Now run through the remaining components
-                    JaniTraverser::traverse(automaton.getVariables(), &functionEliminationVisitor);
+                    traverse(automaton.getVariables(), &functionEliminationVisitor);
                     for (auto& loc : automaton.getLocations()) {
-                        JaniTraverser::traverse(loc, &functionEliminationVisitor);
+                        traverse(loc, &functionEliminationVisitor);
                     }
-                    JaniTraverser::traverse(automaton.getEdgeContainer(), &functionEliminationVisitor);
+                    traverse(automaton.getEdgeContainer(), &functionEliminationVisitor);
                     if (automaton.hasInitialStatesRestriction()) {
                         automaton.setInitialStatesRestriction(functionEliminationVisitor.eliminate(automaton.getInitialStatesRestriction()));
                     }
                 }
                 
+                void traverse(Location& location, boost::any const& data) override {
+                    traverse(location.getAssignments(), data);
+                    if (location.hasTimeProgressInvariant()) {
+                        FunctionEliminationExpressionVisitor* functionEliminationVisitor = boost::any_cast<FunctionEliminationExpressionVisitor*>(data);
+                        location.setTimeProgressInvariant(functionEliminationVisitor->eliminate(location.getTimeProgressInvariant()));
+                    }
+                }
+                
                 void traverse(Constant& constant, boost::any const& data) override {
                     if (constant.isDefined()) {
                         FunctionEliminationExpressionVisitor* functionEliminationVisitor = boost::any_cast<FunctionEliminationExpressionVisitor*>(data);
@@ -355,13 +365,20 @@ namespace storm {
                     }
                 }
                 
+                void traverse(ClockVariable& variable, boost::any const& data) override {
+                    FunctionEliminationExpressionVisitor* functionEliminationVisitor = boost::any_cast<FunctionEliminationExpressionVisitor*>(data);
+                    if (variable.hasInitExpression()) {
+                        variable.setInitExpression(functionEliminationVisitor->eliminate(variable.getInitExpression()));
+                    }
+                }
+                
                 void traverse(TemplateEdge& templateEdge, boost::any const& data) override {
                     FunctionEliminationExpressionVisitor* functionEliminationVisitor = boost::any_cast<FunctionEliminationExpressionVisitor*>(data);
                     templateEdge.setGuard(functionEliminationVisitor->eliminate(templateEdge.getGuard()));
                     for (auto& dest : templateEdge.getDestinations()) {
-                        JaniTraverser::traverse(dest, data);
+                        traverse(dest, data);
                     }
-                    JaniTraverser::traverse(templateEdge.getAssignments(), data);
+                    traverse(templateEdge.getAssignments(), data);
                 }
                 
                 void traverse(Edge& edge, boost::any const& data) override {
diff --git a/src/storm/storage/jani/JSONExporter.cpp b/src/storm/storage/jani/JSONExporter.cpp
index d5e43af93..27797c4bd 100644
--- a/src/storm/storage/jani/JSONExporter.cpp
+++ b/src/storm/storage/jani/JSONExporter.cpp
@@ -811,7 +811,7 @@ namespace storm {
         
         
         modernjson::json buildVariablesArray(storm::jani::VariableSet const& varSet, std::vector<storm::jani::Constant> const& constants, VariableSet const& globalVariables, VariableSet const& localVariables = VariableSet()) {
-            modernjson::json variableDeclarations;
+            modernjson::json variableDeclarations = std::vector<modernjson::json>();
             for(auto const& variable : varSet) {
                 modernjson::json varEntry;
                 varEntry["name"] = variable.getName();
@@ -830,8 +830,7 @@ namespace storm {
                     typeDesc["base"] = "int";
                     typeDesc["lower-bound"] = buildExpression(variable.asBoundedIntegerVariable().getLowerBound(), constants, globalVariables, localVariables);
                     typeDesc["upper-bound"] = buildExpression(variable.asBoundedIntegerVariable().getUpperBound(), constants, globalVariables, localVariables);
-                } else {
-                    assert(variable.isArrayVariable());
+                } else if (variable.isArrayVariable()) {
                     typeDesc["kind"] = "array";
                     switch (variable.asArrayVariable().getElementType()) {
                         case storm::jani::ArrayVariable::ElementType::Bool:
@@ -857,6 +856,9 @@ namespace storm {
                             }
                             break;
                     }
+                } else {
+                    assert(variable.isClockVariable());
+                    typeDesc = "clock";
                 }
                 varEntry["type"] = typeDesc;
                 if (variable.hasInitExpression()) {
@@ -885,7 +887,7 @@ namespace storm {
         }
         
         modernjson::json buildFunctionsArray(std::unordered_map<std::string, FunctionDefinition> const& functionDefinitions, std::vector<storm::jani::Constant> const& constants, VariableSet const& globalVariables, VariableSet const& localVariables = VariableSet()) {
-            modernjson::json functionDeclarations;
+            modernjson::json functionDeclarations = std::vector<modernjson::json>();
             for (auto const& nameFunDef : functionDefinitions) {
                 storm::jani::FunctionDefinition const& funDef = nameFunDef.second;
                 modernjson::json funDefJson;
@@ -908,7 +910,7 @@ namespace storm {
         }
         
         modernjson::json buildAssignmentArray(storm::jani::OrderedAssignments const& orderedAssignments, std::vector<storm::jani::Constant> const& constants, VariableSet const& globalVariables, VariableSet const& localVariables, bool commentExpressions) {
-            modernjson::json assignmentDeclarations;
+            modernjson::json assignmentDeclarations = std::vector<modernjson::json>();
             bool addIndex = orderedAssignments.hasMultipleLevels();
             for(auto const& assignment : orderedAssignments) {
                 modernjson::json assignmentEntry;
@@ -935,11 +937,18 @@ namespace storm {
         }
         
         modernjson::json buildLocationsArray(std::vector<storm::jani::Location> const& locations, std::vector<storm::jani::Constant> const& constants, VariableSet const& globalVariables, VariableSet const& localVariables, bool commentExpressions) {
-            modernjson::json locationDeclarations;
+            modernjson::json locationDeclarations = std::vector<modernjson::json>();
             for(auto const& location : locations) {
                 modernjson::json locEntry;
                 locEntry["name"] = location.getName();
-                // TODO support invariants?
+                if (location.hasTimeProgressInvariant()) {
+                    modernjson::json timeProg;
+                    timeProg["exp"] = buildExpression(location.getTimeProgressInvariant(), constants, globalVariables, localVariables);
+                    if (commentExpressions) {
+                        timeProg["comment"] = location.getTimeProgressInvariant().toString();
+                    }
+                    locEntry["time-progress"] = std::move(timeProg);
+                }
                 if (!location.getAssignments().empty()) {
                     locEntry["transient-values"] = buildAssignmentArray(location.getAssignments(), constants, globalVariables, localVariables, commentExpressions);
                 }
diff --git a/src/storm/storage/jani/Location.cpp b/src/storm/storage/jani/Location.cpp
index 7831436a7..89c8dc846 100644
--- a/src/storm/storage/jani/Location.cpp
+++ b/src/storm/storage/jani/Location.cpp
@@ -1,5 +1,6 @@
 #include "storm/storage/jani/Location.h"
 
+#include "storm/storage/jani/expressions/JaniExpressionSubstitutionVisitor.h"
 #include "storm/utility/macros.h"
 #include "storm/exceptions/InvalidJaniException.h"
 #include "storm/exceptions/InvalidArgumentException.h"
@@ -32,10 +33,25 @@ namespace storm {
             assignments.add(assignment);
         }
         
+        bool Location::hasTimeProgressInvariant() const {
+            return timeProgressInvariant.isInitialized();
+        }
+        
+        storm::expressions::Expression const& Location::getTimeProgressInvariant() const {
+            return timeProgressInvariant;
+        }
+        
+        void Location::setTimeProgressInvariant(storm::expressions::Expression const& expression) {
+            timeProgressInvariant = expression;
+        }
+        
         void Location::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) {
             for (auto& assignment : assignments) {
                 assignment.substitute(substitution);
             }
+            if (hasTimeProgressInvariant()) {
+                setTimeProgressInvariant(substituteJaniExpression(getTimeProgressInvariant(), substitution));
+            }
         }
         
         void Location::changeAssignmentVariables(std::map<Variable const*, std::reference_wrapper<Variable const>> const& remapping) {
diff --git a/src/storm/storage/jani/Location.h b/src/storm/storage/jani/Location.h
index 1fc3cd65d..a18f9c0b6 100644
--- a/src/storm/storage/jani/Location.h
+++ b/src/storm/storage/jani/Location.h
@@ -40,6 +40,22 @@ namespace storm {
              */
             void addTransientAssignment(storm::jani::Assignment const& assignment);
   
+            /*!
+             * Retrieves whether a time progress invariant is attached to this location
+             */
+            bool hasTimeProgressInvariant() const;
+            
+            /*!
+             * Retrieves the time progress invariant
+             */
+            storm::expressions::Expression const& getTimeProgressInvariant() const;
+            
+            /*!
+             * Sets the time progress invariant of this location
+             * @param expression the location invariant (type bool)
+             */
+            void setTimeProgressInvariant(storm::expressions::Expression const& expression);
+            
             /*!
              * Substitutes all variables in all expressions according to the given substitution.
              */
@@ -66,6 +82,9 @@ namespace storm {
             
             /// The transient assignments made in this location.
             OrderedAssignments assignments;
+            
+            // The location's time progress condition
+            storm::expressions::Expression timeProgressInvariant;
         };
         
     }
diff --git a/src/storm/storage/jani/Model.cpp b/src/storm/storage/jani/Model.cpp
index bc8c687c7..7e690d059 100644
--- a/src/storm/storage/jani/Model.cpp
+++ b/src/storm/storage/jani/Model.cpp
@@ -687,6 +687,8 @@ namespace storm {
                 return addVariable(variable.asRealVariable());
             } else if (variable.isArrayVariable()) {
                 return addVariable(variable.asArrayVariable());
+            } else if (variable.isClockVariable()) {
+                return addVariable(variable.asClockVariable());
             } else {
                 STORM_LOG_THROW(false, storm::exceptions::InvalidTypeException, "Variable has invalid type.");
             }
@@ -711,6 +713,10 @@ namespace storm {
         ArrayVariable const& Model::addVariable(ArrayVariable const& variable) {
             return globalVariables.addVariable(variable);
         }
+        
+        ClockVariable const& Model::addVariable(ClockVariable const& variable) {
+            return globalVariables.addVariable(variable);
+        }
 
         VariableSet& Model::getGlobalVariables() {
             return globalVariables;
@@ -1033,6 +1039,9 @@ namespace storm {
             for (auto& variable : result.getGlobalVariables().getArrayVariables()) {
                 variable.substitute(constantSubstitution);
             }
+            for (auto& variable : result.getGlobalVariables().getClockVariables()) {
+                variable.substitute(constantSubstitution);
+            }
             
             // Substitute constants in initial states expression.
             result.setInitialStatesRestriction(substituteJaniExpression(this->getInitialStatesRestriction(), constantSubstitution));
@@ -1086,6 +1095,9 @@ namespace storm {
             for (auto& variable : this->getGlobalVariables().getArrayVariables()) {
                 variable.substitute(substitution);
             }
+            for (auto& variable : this->getGlobalVariables().getClockVariables()) {
+                variable.substitute(substitution);
+            }
             
             // Substitute in initial states expression.
             this->setInitialStatesRestriction(substituteJaniExpression(this->getInitialStatesRestriction(), substitution));
diff --git a/src/storm/storage/jani/Model.h b/src/storm/storage/jani/Model.h
index 656003853..5db1551d5 100644
--- a/src/storm/storage/jani/Model.h
+++ b/src/storm/storage/jani/Model.h
@@ -221,6 +221,11 @@ namespace storm {
              */
             ArrayVariable const& addVariable(ArrayVariable const& variable);
 
+            /*!
+             * Adds the given array variable to this model.
+             */
+            ClockVariable const& addVariable(ClockVariable const& variable);
+
             /*!
              * Retrieves the variables of this automaton.
              */
diff --git a/src/storm/storage/jani/Variable.cpp b/src/storm/storage/jani/Variable.cpp
index 50fae165b..6d4c611c3 100644
--- a/src/storm/storage/jani/Variable.cpp
+++ b/src/storm/storage/jani/Variable.cpp
@@ -5,6 +5,7 @@
 #include "storm/storage/jani/UnboundedIntegerVariable.h"
 #include "storm/storage/jani/RealVariable.h"
 #include "storm/storage/jani/ArrayVariable.h"
+#include "storm/storage/jani/ClockVariable.h"
 #include "storm/storage/jani/expressions/JaniExpressionSubstitutionVisitor.h"
 
 namespace storm {
@@ -54,6 +55,10 @@ namespace storm {
             return false;
         }
         
+        bool Variable::isClockVariable() const {
+            return false;
+        }
+        
         bool Variable::isTransient() const {
             return transient;
         }
@@ -110,6 +115,14 @@ namespace storm {
             return static_cast<ArrayVariable const&>(*this);
         }
         
+        ClockVariable& Variable::asClockVariable() {
+            return static_cast<ClockVariable&>(*this);
+        }
+        
+        ClockVariable const& Variable::asClockVariable() const {
+            return static_cast<ClockVariable const&>(*this);
+        }
+        
         void Variable::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) {
             if (this->hasInitExpression()) {
                 this->setInitExpression(substituteJaniExpression(this->getInitExpression(), substitution));
diff --git a/src/storm/storage/jani/Variable.h b/src/storm/storage/jani/Variable.h
index ab4bf80c1..d7e3a4b9a 100644
--- a/src/storm/storage/jani/Variable.h
+++ b/src/storm/storage/jani/Variable.h
@@ -15,6 +15,7 @@ namespace storm {
         class UnboundedIntegerVariable;
         class RealVariable;
         class ArrayVariable;
+        class ClockVariable;
         
         class Variable {
         public:
@@ -74,6 +75,7 @@ namespace storm {
             virtual bool isUnboundedIntegerVariable() const;
             virtual bool isRealVariable() const;
             virtual bool isArrayVariable() const;
+            virtual bool isClockVariable() const;
 
             virtual bool isTransient() const;
             
@@ -88,6 +90,8 @@ namespace storm {
             RealVariable const& asRealVariable() const;
             ArrayVariable& asArrayVariable();
             ArrayVariable const& asArrayVariable() const;
+            ClockVariable& asClockVariable();
+            ClockVariable const& asClockVariable() const;
             
             /*!
              * Substitutes all variables in all expressions according to the given substitution.
diff --git a/src/storm/storage/jani/VariableSet.cpp b/src/storm/storage/jani/VariableSet.cpp
index a3af625d5..83ef34bdb 100644
--- a/src/storm/storage/jani/VariableSet.cpp
+++ b/src/storm/storage/jani/VariableSet.cpp
@@ -52,6 +52,14 @@ namespace storm {
             return detail::ConstVariables<ArrayVariable>(arrayVariables.begin(), arrayVariables.end());
         }
         
+        detail::Variables<ClockVariable> VariableSet::getClockVariables() {
+            return detail::Variables<ClockVariable>(clockVariables.begin(), clockVariables.end());
+        }
+        
+        detail::ConstVariables<ClockVariable> VariableSet::getClockVariables() const {
+            return detail::ConstVariables<ClockVariable>(clockVariables.begin(), clockVariables.end());
+        }
+        
         Variable const& VariableSet::addVariable(Variable const& variable) {
             if (variable.isBooleanVariable()) {
                 return addVariable(variable.asBooleanVariable());
@@ -63,6 +71,8 @@ namespace storm {
                 return addVariable(variable.asRealVariable());
             } else if (variable.isArrayVariable()) {
                 return addVariable(variable.asArrayVariable());
+            } else if (variable.isClockVariable()) {
+                return addVariable(variable.asClockVariable());
             }
             STORM_LOG_THROW(false, storm::exceptions::InvalidTypeException, "Cannot add variable of unknown type.");
         }
@@ -132,6 +142,19 @@ namespace storm {
             return *newVariable;
         }
         
+        ClockVariable const& VariableSet::addVariable(ClockVariable const& variable) {
+            STORM_LOG_THROW(!this->hasVariable(variable.getName()), storm::exceptions::WrongFormatException, "Cannot add variable with name '" << variable.getName() << "', because a variable with that name already exists.");
+            std::shared_ptr<ClockVariable> newVariable = std::make_shared<ClockVariable>(variable);
+            variables.push_back(newVariable);
+            clockVariables.push_back(newVariable);
+            if (variable.isTransient()) {
+                transientVariables.push_back(newVariable);
+            }
+            nameToVariable.emplace(variable.getName(), variable.getExpressionVariable());
+            variableToVariable.emplace(variable.getExpressionVariable(), newVariable);
+            return *newVariable;
+        }
+        
         std::vector<std::shared_ptr<ArrayVariable>> VariableSet::dropAllArrayVariables() {
             if (!arrayVariables.empty()) {
                 for (auto const& arrVar : arrayVariables) {
@@ -228,6 +251,10 @@ namespace storm {
             return !arrayVariables.empty();
         }
         
+        bool VariableSet::containsClockVariables() const {
+            return !clockVariables.empty();
+        }
+        
         bool VariableSet::containsNonTransientRealVariables() const {
             for (auto const& variable : realVariables) {
                 if (!variable->isTransient()) {
@@ -247,7 +274,7 @@ namespace storm {
         }
         
         bool VariableSet::empty() const {
-            return !(containsBooleanVariable() || containsBoundedIntegerVariable() || containsUnboundedIntegerVariables() || containsRealVariables() || containsArrayVariables());
+            return !(containsBooleanVariable() || containsBoundedIntegerVariable() || containsUnboundedIntegerVariables() || containsRealVariables() || containsArrayVariables() || containsClockVariables());
         }
         
         uint_fast64_t VariableSet::getNumberOfTransientVariables() const {
@@ -332,6 +359,13 @@ namespace storm {
                     }
                 }
             }
+            for (auto const& clockVariable : this->getClockVariables()) {
+                if (clockVariable.hasInitExpression()) {
+                    if (clockVariable.getInitExpression().containsVariable(variables)) {
+                        return true;
+                    }
+                }
+            }
             return false;
         }
         
diff --git a/src/storm/storage/jani/VariableSet.h b/src/storm/storage/jani/VariableSet.h
index 4e4d2d511..af63c949d 100644
--- a/src/storm/storage/jani/VariableSet.h
+++ b/src/storm/storage/jani/VariableSet.h
@@ -10,6 +10,7 @@
 #include "storm/storage/jani/BoundedIntegerVariable.h"
 #include "storm/storage/jani/RealVariable.h"
 #include "storm/storage/jani/ArrayVariable.h"
+#include "storm/storage/jani/ClockVariable.h"
 
 namespace storm {
     namespace jani {
@@ -78,6 +79,16 @@ namespace storm {
              * Retrieves the Array variables in this set.
              */
             detail::ConstVariables<ArrayVariable> getArrayVariables() const;
+            
+            /*!
+             * Retrieves the clock variables in this set.
+             */
+            detail::Variables<ClockVariable> getClockVariables();
+            
+            /*!
+             * Retrieves the clock variables in this set.
+             */
+            detail::ConstVariables<ClockVariable> getClockVariables() const;
 
             /*!
              * Adds the given variable to this set.
@@ -105,7 +116,7 @@ namespace storm {
             RealVariable const& addVariable(RealVariable const& variable);
 
             /*!
-             * Adds the given real variable to this set.
+             * Adds the given array variable to this set.
              */
             ArrayVariable const& addVariable(ArrayVariable const& variable);
 
@@ -113,6 +124,11 @@ namespace storm {
              * Removes all array variables in this set
              */
             std::vector<std::shared_ptr<ArrayVariable>> dropAllArrayVariables();
+ 
+            /*!
+             * Adds the given clock variable to this set.
+             */
+            ClockVariable const& addVariable(ClockVariable const& variable);
             
             /*!
              * Retrieves whether this variable set contains a variable with the given name.
@@ -188,6 +204,11 @@ namespace storm {
              */
             bool containsArrayVariables() const;
 
+            /*!
+             * Retrieves whether the set of variables contains a clock variable.
+             */
+            bool containsClockVariables() const;
+
             /*!
              * Retrieves whether the set of variables contains a non-transient real variable.
              */
@@ -258,6 +279,9 @@ namespace storm {
             /// The array variables in this set.
             std::vector<std::shared_ptr<ArrayVariable>> arrayVariables;
             
+            /// The clock variables in this set.
+            std::vector<std::shared_ptr<ClockVariable>> clockVariables;
+            
             /// The transient variables in this set.
             std::vector<std::shared_ptr<Variable>> transientVariables;
             
diff --git a/src/storm/storage/jani/traverser/JaniTraverser.cpp b/src/storm/storage/jani/traverser/JaniTraverser.cpp
index e77377a15..dc403479a 100644
--- a/src/storm/storage/jani/traverser/JaniTraverser.cpp
+++ b/src/storm/storage/jani/traverser/JaniTraverser.cpp
@@ -70,10 +70,16 @@ namespace storm {
             for (auto& v : variableSet.getArrayVariables()) {
                 traverse(v, data);
             }
+            for (auto& v : variableSet.getClockVariables()) {
+                traverse(v, data);
+            }
         }
         
         void JaniTraverser::traverse(Location& location, boost::any const& data) {
             traverse(location.getAssignments(), data);
+            if (location.hasTimeProgressInvariant()) {
+                traverse(location.getTimeProgressInvariant(), data);
+            }
         }
         
         void JaniTraverser::traverse(BooleanVariable& variable, boost::any const& data) {
@@ -114,6 +120,12 @@ namespace storm {
             }
         }
         
+        void JaniTraverser::traverse(ClockVariable& variable, boost::any const& data) {
+            if (variable.hasInitExpression()) {
+                traverse(variable.getInitExpression(), data);
+            }
+        }
+        
         void JaniTraverser::traverse(EdgeContainer& edgeContainer, boost::any const& data) {
             for (auto& templateEdge : edgeContainer.getTemplateEdges()) {
                 traverse(*templateEdge, data);
@@ -236,10 +248,16 @@ namespace storm {
             for (auto const& v : variableSet.getArrayVariables()) {
                 traverse(v, data);
             }
+            for (auto const& v : variableSet.getClockVariables()) {
+                traverse(v, data);
+            }
         }
         
         void ConstJaniTraverser::traverse(Location const& location, boost::any const& data) {
             traverse(location.getAssignments(), data);
+            if (location.hasTimeProgressInvariant()) {
+                traverse(location.getTimeProgressInvariant(), data);
+            }
         }
         
         void ConstJaniTraverser::traverse(BooleanVariable const& variable, boost::any const& data) {
@@ -280,6 +298,12 @@ namespace storm {
             }
         }
         
+        void ConstJaniTraverser::traverse(ClockVariable const& variable, boost::any const& data) {
+            if (variable.hasInitExpression()) {
+                traverse(variable.getInitExpression(), data);
+            }
+        }
+        
         void ConstJaniTraverser::traverse(EdgeContainer const& edgeContainer, boost::any const& data) {
             for (auto const& templateEdge : edgeContainer.getTemplateEdges()) {
                 traverse(*templateEdge, data);
diff --git a/src/storm/storage/jani/traverser/JaniTraverser.h b/src/storm/storage/jani/traverser/JaniTraverser.h
index a7da8bc6f..3d2310458 100644
--- a/src/storm/storage/jani/traverser/JaniTraverser.h
+++ b/src/storm/storage/jani/traverser/JaniTraverser.h
@@ -24,6 +24,7 @@ namespace storm {
             virtual void traverse(UnboundedIntegerVariable& variable, boost::any const& data);
             virtual void traverse(RealVariable& variable, boost::any const& data);
             virtual void traverse(ArrayVariable& variable, boost::any const& data);
+            virtual void traverse(ClockVariable& variable, boost::any const& data);
             virtual void traverse(EdgeContainer& edgeContainer, boost::any const& data);
             virtual void traverse(TemplateEdge& templateEdge, boost::any const& data);
             virtual void traverse(TemplateEdgeDestination& templateEdgeDestination, boost::any const& data);
@@ -52,6 +53,7 @@ namespace storm {
             virtual void traverse(UnboundedIntegerVariable const& variable, boost::any const& data);
             virtual void traverse(RealVariable const& variable, boost::any const& data);
             virtual void traverse(ArrayVariable const& variable, boost::any const& data);
+            virtual void traverse(ClockVariable const& variable, boost::any const& data);
             virtual void traverse(EdgeContainer const& edgeContainer, boost::any const& data);
             virtual void traverse(TemplateEdge const& templateEdge, boost::any const& data);
             virtual void traverse(TemplateEdgeDestination const& templateEdgeDestination, boost::any const& data);
diff --git a/src/storm/storage/prism/ClockVariable.cpp b/src/storm/storage/prism/ClockVariable.cpp
new file mode 100644
index 000000000..96984babc
--- /dev/null
+++ b/src/storm/storage/prism/ClockVariable.cpp
@@ -0,0 +1,24 @@
+#include "storm/storage/prism/ClockVariable.h"
+
+#include "storm/storage/expressions/ExpressionManager.h"
+#include "storm/utility/constants.h"
+
+namespace storm {
+    namespace prism {
+        ClockVariable::ClockVariable(storm::expressions::Variable const& variable, bool observable, std::string const& filename, uint_fast64_t lineNumber) : Variable(variable, variable.getManager().rational(storm::utility::zero<storm::RationalNumber>()), observable, filename, lineNumber) {
+            // Nothing to do here.
+        }
+        
+        void ClockVariable::createMissingInitialValue() {
+            if (!this->hasInitialValue()) {
+                this->setInitialValueExpression(this->getExpressionVariable().getManager().rational(storm::utility::zero<storm::RationalNumber>()));
+            }
+        }
+        
+        std::ostream& operator<<(std::ostream& stream, ClockVariable const& variable) {
+            stream << variable.getName() << ": clock" << ";";
+            return stream;
+        }
+        
+    } // namespace prism
+} // namespace storm
diff --git a/src/storm/storage/prism/ClockVariable.h b/src/storm/storage/prism/ClockVariable.h
new file mode 100644
index 000000000..8cba64f58
--- /dev/null
+++ b/src/storm/storage/prism/ClockVariable.h
@@ -0,0 +1,37 @@
+#pragma once
+
+#include <map>
+
+#include "storm/storage/prism/Variable.h"
+
+namespace storm {
+    namespace prism {
+        class ClockVariable : public Variable {
+        public:
+            // Create default implementations of constructors/assignment.
+            ClockVariable() = default;
+            ClockVariable(ClockVariable const& other) = default;
+            ClockVariable& operator=(ClockVariable const& other)= default;
+            ClockVariable(ClockVariable&& other) = default;
+            ClockVariable& operator=(ClockVariable&& other) = default;
+
+            /*!
+             * Creates a clock variable
+             *
+             * @param variable The expression variable associated with this variable.
+             * @param filename The filename in which the variable is defined.
+             * @param lineNumber The line number in which the variable is defined.
+             */
+            ClockVariable(storm::expressions::Variable const& variable, bool observable, std::string const& filename = "", uint_fast64_t lineNumber = 0);
+            
+            /*!
+             * Sets a missing initial value (note that for clock variables, this is always zero)
+             */
+            virtual void createMissingInitialValue() override;
+            
+            friend std::ostream& operator<<(std::ostream& stream, ClockVariable const& variable);
+        };
+        
+    } // namespace prism
+} // namespace storm
+
diff --git a/src/storm/storage/prism/Module.cpp b/src/storm/storage/prism/Module.cpp
index 33d8258f7..a47021959 100644
--- a/src/storm/storage/prism/Module.cpp
+++ b/src/storm/storage/prism/Module.cpp
@@ -6,11 +6,11 @@
 
 namespace storm {
     namespace prism {
-        Module::Module(std::string const& moduleName, std::vector<storm::prism::BooleanVariable> const& booleanVariables, std::vector<storm::prism::IntegerVariable> const& integerVariables, std::vector<storm::prism::Command> const& commands, std::string const& filename, uint_fast64_t lineNumber) : Module(moduleName, booleanVariables, integerVariables, commands, "", std::map<std::string, std::string>(), filename, lineNumber) {
+        Module::Module(std::string const& moduleName, std::vector<storm::prism::BooleanVariable> const& booleanVariables, std::vector<storm::prism::IntegerVariable> const& integerVariables, std::vector<storm::prism::ClockVariable> const& clockVariables, storm::expressions::Expression const& invariant, std::vector<storm::prism::Command> const& commands, std::string const& filename, uint_fast64_t lineNumber) : Module(moduleName, booleanVariables, integerVariables, clockVariables, invariant, commands, "", std::map<std::string, std::string>(), filename, lineNumber) {
             // Intentionally left empty.
         }
         
-        Module::Module(std::string const& moduleName, std::vector<storm::prism::BooleanVariable> const& booleanVariables, std::vector<storm::prism::IntegerVariable> const& integerVariables, std::vector<storm::prism::Command> const& commands, std::string const& renamedFromModule, std::map<std::string, std::string> const& renaming, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), moduleName(moduleName), booleanVariables(booleanVariables), booleanVariableToIndexMap(), integerVariables(integerVariables), integerVariableToIndexMap(), commands(commands), synchronizingActionIndices(), actionIndicesToCommandIndexMap(), renamedFromModule(renamedFromModule), renaming(renaming) {
+        Module::Module(std::string const& moduleName, std::vector<storm::prism::BooleanVariable> const& booleanVariables, std::vector<storm::prism::IntegerVariable> const& integerVariables, std::vector<storm::prism::ClockVariable> const& clockVariables, storm::expressions::Expression const& invariant, std::vector<storm::prism::Command> const& commands, std::string const& renamedFromModule, std::map<std::string, std::string> const& renaming, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), moduleName(moduleName), booleanVariables(booleanVariables), booleanVariableToIndexMap(), integerVariables(integerVariables), integerVariableToIndexMap(), clockVariables(clockVariables), clockVariableToIndexMap(), invariant(invariant), commands(commands), synchronizingActionIndices(), actionIndicesToCommandIndexMap(), renamedFromModule(renamedFromModule), renaming(renaming) {
             // Initialize the internal mappings for fast information retrieval.
             this->createMappings();
         }
@@ -42,6 +42,20 @@ namespace storm {
         std::vector<storm::prism::IntegerVariable> const& Module::getIntegerVariables() const {
             return this->integerVariables;
         }
+        
+        std::size_t Module::getNumberOfClockVariables() const {
+            return this->clockVariables.size();
+        }
+        
+        storm::prism::ClockVariable const& Module::getClockVariable(std::string const& variableName) const {
+            auto const& nameIndexPair = this->clockVariableToIndexMap.find(variableName);
+            STORM_LOG_THROW(nameIndexPair != this->clockVariableToIndexMap.end(), storm::exceptions::InvalidArgumentException, "Unknown clock variable '" << variableName << "'.");
+            return this->getClockVariables()[nameIndexPair->second];
+        }
+        
+        std::vector<storm::prism::ClockVariable> const& Module::getClockVariables() const {
+            return this->clockVariables;
+        }
 
         std::set<storm::expressions::Variable> Module::getAllExpressionVariables() const {
             std::set<storm::expressions::Variable> result;
@@ -51,6 +65,9 @@ namespace storm {
             for (auto const& var : this->getIntegerVariables()) {
                 result.insert(var.getExpressionVariable());
             }
+            for (auto const& var : this->getClockVariables()) {
+                result.insert(var.getExpressionVariable());
+            }
             return result;
         }
         
@@ -134,6 +151,9 @@ namespace storm {
             for (uint_fast64_t i = 0; i < this->integerVariables.size(); ++i) {
                 this->integerVariableToIndexMap[this->getIntegerVariables()[i].getName()] = i;
             }
+            for (uint_fast64_t i = 0; i < this->clockVariables.size(); ++i) {
+                this->booleanVariableToIndexMap[this->getClockVariables()[i].getName()] = i;
+            }
             
             // Add the mapping for all commands.
             for (uint_fast64_t i = 0; i < this->commands.size(); i++) {
@@ -169,7 +189,7 @@ namespace storm {
                 }
             }
             
-            return Module(this->getName(), this->getBooleanVariables(), this->getIntegerVariables(), newCommands);
+            return Module(this->getName(), this->getBooleanVariables(), this->getIntegerVariables(), this->getClockVariables(), this->getInvariant(), newCommands);
         }
         
         Module Module::restrictActionIndices(boost::container::flat_set<uint_fast64_t> const& actionIndices) const {
@@ -181,7 +201,7 @@ namespace storm {
                 }
             }
             
-            return Module(this->getName(), this->getBooleanVariables(), this->getIntegerVariables(), newCommands);
+            return Module(this->getName(), this->getBooleanVariables(), this->getIntegerVariables(), this->getClockVariables(), this->getInvariant(), newCommands);
         }
         
         Module Module::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const {
@@ -203,7 +223,7 @@ namespace storm {
                 newCommands.emplace_back(command.substitute(substitution));
             }
             
-            return Module(this->getName(), newBooleanVariables, newIntegerVariables, newCommands, this->getFilename(), this->getLineNumber());
+            return Module(this->getName(), newBooleanVariables, newIntegerVariables, this->getClockVariables(), this->getInvariant(), newCommands, this->getFilename(), this->getLineNumber());
         }
         
         bool Module::containsVariablesOnlyInUpdateProbabilities(std::set<storm::expressions::Variable> const& undefinedConstantVariables) const {
@@ -240,8 +260,19 @@ namespace storm {
             for (auto& variable : integerVariables) {
                 variable.createMissingInitialValue();
             }
+            for (auto& variable : clockVariables) {
+                variable.createMissingInitialValue();
+            }
         }
         
+        bool Module::hasInvariant() const {
+            return this->invariant.isInitialized();
+        }
+
+        storm::expressions::Expression const& Module::getInvariant() const {
+            return this->invariant;
+        }
+
         std::ostream& operator<<(std::ostream& stream, Module const& module) {
             stream << "module " << module.getName() << std::endl;
             for (auto const& booleanVariable : module.getBooleanVariables()) {
@@ -250,6 +281,9 @@ namespace storm {
             for (auto const& integerVariable : module.getIntegerVariables()) {
                 stream << "\t" << integerVariable << std::endl;
             }
+            for (auto const& clockVariable : module.getClockVariables()) {
+                stream << "\t" << clockVariable << std::endl;
+            }
             for (auto const& command : module.getCommands()) {
                 stream << "\t" << command << std::endl;
             }
diff --git a/src/storm/storage/prism/Module.h b/src/storm/storage/prism/Module.h
index 9c1286805..970304ab5 100644
--- a/src/storm/storage/prism/Module.h
+++ b/src/storm/storage/prism/Module.h
@@ -10,6 +10,7 @@
 
 #include "storm/storage/prism/BooleanVariable.h"
 #include "storm/storage/prism/IntegerVariable.h"
+#include "storm/storage/prism/ClockVariable.h"
 #include "storm/storage/prism/Command.h"
 #include "storm/utility/OsDetection.h"
 
@@ -23,11 +24,13 @@ namespace storm {
              * @param moduleName The name of the module.
              * @param booleanVariables The boolean variables defined by the module.
              * @param integerVariables The integer variables defined by the module.
+             * @param clockVariables The clock variables defined by the module (only for PTA models).
+             * @param invariant An invariant that is used to restrict the values of the clock variables (only for PTA models).
              * @param commands The commands of the module.
              * @param filename The filename in which the module is defined.
              * @param lineNumber The line number in which the module is defined.
              */
-            Module(std::string const& moduleName, std::vector<storm::prism::BooleanVariable> const& booleanVariables, std::vector<storm::prism::IntegerVariable> const& integerVariables, std::vector<storm::prism::Command> const& commands, std::string const& filename = "", uint_fast64_t lineNumber = 0);
+            Module(std::string const& moduleName, std::vector<storm::prism::BooleanVariable> const& booleanVariables, std::vector<storm::prism::IntegerVariable> const& integerVariables, std::vector<storm::prism::ClockVariable> const& clockVariables, storm::expressions::Expression const& invariant, std::vector<storm::prism::Command> const& commands, std::string const& filename = "", uint_fast64_t lineNumber = 0);
 
             /*!
              * Creates a module with the given name, variables and commands that is marked as being renamed from the
@@ -36,13 +39,15 @@ namespace storm {
              * @param moduleName The name of the module.
              * @param booleanVariables The boolean variables defined by the module.
              * @param integerVariables The integer variables defined by the module.
+             * @param clockVariables The clock variables defined by the module (only for PTA models).
+             * @param invariant An invariant that is used to restrict the values of the clock variables (only for PTA models).
              * @param commands The commands of the module.
              * @param renamedFromModule The name of the module from which this module was renamed.
              * @param renaming The renaming of identifiers used to create this module.
              * @param filename The filename in which the module is defined.
              * @param lineNumber The line number in which the module is defined.
              */
-            Module(std::string const& moduleName, std::vector<storm::prism::BooleanVariable> const& booleanVariables, std::vector<storm::prism::IntegerVariable> const& integerVariables, std::vector<storm::prism::Command> const& commands, std::string const& renamedFromModule, std::map<std::string, std::string> const& renaming, std::string const& filename = "", uint_fast64_t lineNumber = 0);
+            Module(std::string const& moduleName, std::vector<storm::prism::BooleanVariable> const& booleanVariables, std::vector<storm::prism::IntegerVariable> const& integerVariables, std::vector<storm::prism::ClockVariable> const& clockVariables, storm::expressions::Expression const& invariant, std::vector<storm::prism::Command> const& commands, std::string const& renamedFromModule, std::map<std::string, std::string> const& renaming, std::string const& filename = "", uint_fast64_t lineNumber = 0);
 
             // Create default implementations of constructors/assignment.
             Module() = default;
@@ -94,7 +99,29 @@ namespace storm {
              * @return The integer variables of the module.
              */
             std::vector<storm::prism::IntegerVariable> const& getIntegerVariables() const;
-
+            
+            /*!
+             * Retrieves the number of clock variables in the module.
+             *
+             * @return the number of clock variables in the module.
+             */
+            std::size_t getNumberOfClockVariables() const;
+            
+            /*!
+             * Retrieves a reference to the clock variable with the given name.
+             *
+             * @param variableName The name of the clock variable to retrieve.
+             * @return A reference to the clock variable with the given name.
+             */
+            storm::prism::ClockVariable const& getClockVariable(std::string const& variableName) const;
+            
+            /*!
+             * Retrieves the clock variables of the module.
+             *
+             * @return The clock variables of the module.
+             */
+            std::vector<storm::prism::ClockVariable> const& getClockVariables() const;
+            
             /*!
              * Retrieves all expression variables used by this module.
              *
@@ -236,6 +263,16 @@ namespace storm {
              */
             void createMissingInitialValues();
             
+            /*!
+             * Returns true, if an invariant was specified (only relevant for PTA models)
+             */
+            bool hasInvariant() const;
+            
+            /*!
+             * Returns the specified invariant (only relevant for PTA models)
+             */
+             storm::expressions::Expression const& getInvariant() const;
+            
             friend std::ostream& operator<<(std::ostream& stream, Module const& module);
 
         private:
@@ -258,6 +295,15 @@ namespace storm {
 
             // A mapping from integer variables to the corresponding indices in the vector.
             std::map<std::string, uint_fast64_t> integerVariableToIndexMap;
+            
+            // A list of clock variables.
+            std::vector<storm::prism::ClockVariable> clockVariables;
+
+            // A mapping from clock variables to the corresponding indices in the vector.
+            std::map<std::string, uint_fast64_t> clockVariableToIndexMap;
+            
+            // An invariant (only for PTA models)
+            storm::expressions::Expression invariant;
 
             // The commands associated with the module.
             std::vector<storm::prism::Command> commands;
diff --git a/src/storm/storage/prism/Program.cpp b/src/storm/storage/prism/Program.cpp
index e9f6f8ecb..a0b32175a 100644
--- a/src/storm/storage/prism/Program.cpp
+++ b/src/storm/storage/prism/Program.cpp
@@ -810,9 +810,12 @@ namespace storm {
                 for (auto const& booleanVariable : module.getBooleanVariables()) {
                     this->variableToModuleIndexMap[booleanVariable.getName()] = moduleIndex;
                 }
-                for (auto const& integerVariable : module.getBooleanVariables()) {
+                for (auto const& integerVariable : module.getIntegerVariables()) {
                     this->variableToModuleIndexMap[integerVariable.getName()] = moduleIndex;
                 }
+                for (auto const& clockVariable : module.getClockVariables()) {
+                    this->variableToModuleIndexMap[clockVariable.getName()] = moduleIndex;
+                }
             }
             
         }
@@ -1104,6 +1107,12 @@ namespace storm {
                     variables.insert(variable.getExpressionVariable());
                     all.insert(variable.getExpressionVariable());
                 }
+                
+                for (auto const& variable : module.getClockVariables()) {
+                    // Record the new identifier for future checks.
+                    variables.insert(variable.getExpressionVariable());
+                    all.insert(variable.getExpressionVariable());
+                }
             }
             
             // Create the set of valid identifiers for future checks.
@@ -1121,7 +1130,7 @@ namespace storm {
                 }
             }
             
-            // Check the commands of the modules.
+            // Check the commands and invariants of the modules.
             bool hasProbabilisticCommand = false;
             bool hasMarkovianCommand = false;
             bool hasLabeledMarkovianCommand = false;
@@ -1133,6 +1142,24 @@ namespace storm {
                 for (auto const& variable : module.getIntegerVariables()) {
                     legalVariables.insert(variable.getExpressionVariable());
                 }
+                for (auto const& variable : module.getClockVariables()) {
+                    legalVariables.insert(variable.getExpressionVariable());
+                }
+                
+                if (module.hasInvariant()) {
+                    std::set<storm::expressions::Variable> containedVariables = module.getInvariant().getVariables();
+                    std::set<storm::expressions::Variable> illegalVariables;
+                    std::set_difference(containedVariables.begin(), containedVariables.end(), variablesAndConstants.begin(), variablesAndConstants.end(), std::inserter(illegalVariables, illegalVariables.begin()));
+                    bool isValid = illegalVariables.empty();
+                    if (!isValid) {
+                        std::vector<std::string> illegalVariableNames;
+                        for (auto const& var : illegalVariables) {
+                            illegalVariableNames.push_back(var.getName());
+                        }
+                        STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << module.getFilename() << ", line " << module.getLineNumber() << ": invariant " << module.getInvariant()  << " refers to unknown identifiers: " << boost::algorithm::join(illegalVariableNames, ",") << ".");
+                    }
+                    STORM_LOG_THROW(module.getInvariant().hasBooleanType(), storm::exceptions::WrongFormatException, "Error in " << module.getFilename() << ", line " << module.getLineNumber() << ": invariant " << module.getInvariant() << " must evaluate to type 'bool'.");
+                }
                 
                 for (auto& command : module.getCommands()) {
                     // Check the guard.
@@ -1189,7 +1216,7 @@ namespace storm {
                                 }
                             }
                             STORM_LOG_THROW(alreadyAssignedVariables.find(assignedVariable) == alreadyAssignedVariables.end(), storm::exceptions::WrongFormatException, "Error in " << command.getFilename() << ", line " << command.getLineNumber() << ": duplicate assignment to variable '" << assignment.getVariableName() << "'.");
-                            STORM_LOG_THROW(assignedVariable.getType() == assignment.getExpression().getType(), storm::exceptions::WrongFormatException, "Error in " << command.getFilename() << ", line " << command.getLineNumber() << ": illegally assigning a value of type '" << assignment.getExpression().getType() << "' to variable '" << assignment.getVariableName() << "' of type '" << assignedVariable.getType() << "'.");
+                            STORM_LOG_THROW(assignedVariable.getType() == assignment.getExpression().getType() || (assignedVariable.getType().isRationalType() && assignment.getExpression().getType().isNumericalType()), storm::exceptions::WrongFormatException, "Error in " << command.getFilename() << ", line " << command.getLineNumber() << ": illegally assigning a value of type '" << assignment.getExpression().getType() << "' to variable '" << assignment.getVariableName() << "' of type '" << assignedVariable.getType() << "'.");
                             
                             containedVariables = assignment.getExpression().getVariables();
                             illegalVariables.clear();
@@ -1409,7 +1436,8 @@ namespace storm {
                     }
                 }
                 
-                newModules.emplace_back(module.getName(), newBooleanVars, newIntegerVars, newCommands);
+                // we currently do not simplify clock variables or invariants
+                newModules.emplace_back(module.getName(), newBooleanVars, newIntegerVars, module.getClockVariables(), module.getInvariant(), newCommands);
                 
                 // Determine the set of action indices that have been deleted entirely.
                 std::set_difference(module.getSynchronizingActionIndices().begin(), module.getSynchronizingActionIndices().end(), newModules.back().getSynchronizingActionIndices().begin(), newModules.back().getSynchronizingActionIndices().end(), std::inserter(actionIndicesToDelete, actionIndicesToDelete.begin()));
@@ -1464,6 +1492,7 @@ namespace storm {
             std::stringstream newModuleName;
             std::vector<storm::prism::BooleanVariable> allBooleanVariables;
             std::vector<storm::prism::IntegerVariable> allIntegerVariables;
+            std::vector<storm::prism::ClockVariable> allClockVariables;
             std::vector<storm::prism::Command> newCommands;
             uint_fast64_t nextCommandIndex = 0;
             uint_fast64_t nextUpdateIndex = 0;
@@ -1489,6 +1518,7 @@ namespace storm {
             // this is just for simplicity and is not needed.
             allBooleanVariables.insert(allBooleanVariables.end(), this->getGlobalBooleanVariables().begin(), this->getGlobalBooleanVariables().end());
             allIntegerVariables.insert(allIntegerVariables.end(), this->getGlobalIntegerVariables().begin(), this->getGlobalIntegerVariables().end());
+            storm::expressions::Expression newInvariant;
             
             // Now go through the modules, gather the variables, construct the name of the new module and assert the
             // bounds of the discovered variables.
@@ -1496,12 +1526,17 @@ namespace storm {
                 newModuleName << module.getName() << "_";
                 allBooleanVariables.insert(allBooleanVariables.end(), module.getBooleanVariables().begin(), module.getBooleanVariables().end());
                 allIntegerVariables.insert(allIntegerVariables.end(), module.getIntegerVariables().begin(), module.getIntegerVariables().end());
+                allClockVariables.insert(allClockVariables.end(), module.getClockVariables().begin(), module.getClockVariables().end());
                 
                 for (auto const& variable : module.getIntegerVariables()) {
                     solver->add(variable.getExpression() >= variable.getLowerBoundExpression());
                     solver->add(variable.getExpression() <= variable.getUpperBoundExpression());
                 }
                 
+                if (module.hasInvariant()) {
+                    newInvariant = newInvariant.isInitialized() ? (newInvariant && module.getInvariant()) : module.getInvariant();
+                }
+                
                 // The commands without a synchronizing action name, can simply be copied (plus adjusting the global
                 // indices of the command and its updates).
                 for (auto const& command : module.getCommands()) {
@@ -1643,7 +1678,7 @@ namespace storm {
             }
             
             // Finally, we can create the module and the program and return it.
-            storm::prism::Module singleModule(newModuleName.str(), allBooleanVariables, allIntegerVariables, newCommands, this->getFilename(), 0);
+            storm::prism::Module singleModule(newModuleName.str(), allBooleanVariables, allIntegerVariables, allClockVariables, newInvariant, newCommands, this->getFilename(), 0);
             
             return Program(manager, this->getModelType(), this->getConstants(), std::vector<storm::prism::BooleanVariable>(), std::vector<storm::prism::IntegerVariable>(), this->getFormulas(), {singleModule}, actionToIndexMap, this->getRewardModels(), this->getLabels(), this->getOptionalInitialConstruct(), this->getOptionalSystemCompositionConstruct(), prismCompatibility, this->getFilename(), 0, true);
         }
@@ -1852,6 +1887,7 @@ namespace storm {
                 case Program::ModelType::CTMDP: out << "ctmdp"; break;
                 case Program::ModelType::MA: out << "ma"; break;
                 case Program::ModelType::POMDP: out << "pomdp"; break;
+                case Program::ModelType::PTA: out << "pta"; break;
             }
             return out;
         }
diff --git a/src/storm/storage/prism/Program.h b/src/storm/storage/prism/Program.h
index 3958c5155..8b6cb1eb1 100644
--- a/src/storm/storage/prism/Program.h
+++ b/src/storm/storage/prism/Program.h
@@ -31,7 +31,7 @@ namespace storm {
             /*!
              * An enum for the different model types.
              */
-            enum class ModelType {UNDEFINED, DTMC, CTMC, MDP, CTMDP, MA, POMDP};
+            enum class ModelType {UNDEFINED, DTMC, CTMC, MDP, CTMDP, MA, POMDP, PTA};
             
             enum class ValidityCheckLevel  : unsigned {VALIDINPUT = 0, READYFORPROCESSING = 1};
             
diff --git a/src/storm/storage/prism/ToJaniConverter.cpp b/src/storm/storage/prism/ToJaniConverter.cpp
index a780200f2..855ece20c 100644
--- a/src/storm/storage/prism/ToJaniConverter.cpp
+++ b/src/storm/storage/prism/ToJaniConverter.cpp
@@ -38,6 +38,8 @@ namespace storm {
                     break;
                 case Program::ModelType::MA: modelType = storm::jani::ModelType::MA;
                     break;
+                case Program::ModelType::PTA: modelType = storm::jani::ModelType::PTA;
+                    break;
                 default: modelType = storm::jani::ModelType::UNDEFINED;
             }
             storm::jani::Model janiModel("jani_from_prism", modelType, 1, manager);
@@ -359,12 +361,29 @@ namespace storm {
                         STORM_LOG_INFO("Variable " << variable.getName() << " is declared but never used.");
                     }
                 }
+                for (auto const& variable : module.getClockVariables()) {
+                    storm::jani::ClockVariable newClockVariable = *storm::jani::makeClockVariable(variable.getName(), variable.getExpressionVariable(), variable.hasInitialValue() ? boost::make_optional(variable.getInitialValueExpression()) : boost::none, false);
+                    auto findRes = variablesToMakeGlobal.find(variable.getExpressionVariable());
+                    if (findRes != variablesToMakeGlobal.end()) {
+                        bool makeVarGlobal = findRes->second;
+                        storm::jani::ClockVariable const& createdVariable = makeVarGlobal ? janiModel.addVariable(newClockVariable) : automaton.addVariable(newClockVariable);
+                        variableToVariableMap.emplace(variable.getExpressionVariable(), createdVariable);
+                    } else {
+                        STORM_LOG_INFO("Variable " << variable.getName() << " is declared but never used.");
+                    }
+                }
+                
                 automaton.setInitialStatesRestriction(manager->boolean(true));
                 
                 // Create a single location that will have all the edges.
                 uint64_t onlyLocationIndex = automaton.addLocation(storm::jani::Location("l"));
                 automaton.addInitialLocation(onlyLocationIndex);
                 
+                if (module.hasInvariant()) {
+                    storm::jani::Location& onlyLocation = automaton.getLocation(onlyLocationIndex);
+                    onlyLocation.setTimeProgressInvariant(module.getInvariant());
+                }
+                
                 // If we are translating the first module that has the action, we need to add the transient assignments to the location.
                 // However, in standard compliant JANI, there are no state rewards
                 if (firstModule) {