In today’s world the sensors of mobile devices increasingly allow applications for both sensing and reacting based on the surrounding environment. One very promising application of sensor data is the prediction of future contexts. But today’s existing technologies for context prediction often are rather computationally expensive and not very well suited to the requirements of this new field. Research in the field of context prediction is currently limited to predicting the next possible contexts in time that a user may enter. So more expressive predictions that deal with complex behaviour in future context are currently not yet being dealt with. This thesis aims to extend these limits and to enable more complex predictions by using Model Checking methods. Model checking is an efficient tool to validate systems against formal specifications. In this thesis context prediction is being treated as a probabilistic Model Checking problem. In order to accomplish this we formulate queries in temporal logics that allow predictions about future contexts. These queries formulated in temporal logics will then be computed using a learned behaviour model of a user and evaluated using probabilistic methods.