Smart systems need to plan ahead, for instance to decide when to charge your electric vehicle, when to heat your home or how to guide you to your destination. Algorithms for sequential decision making allow for smart decisions given an uncertain future, but require models of the system as input. This project combines machine learning and model checking to learn and evaluate such models based on historical data.