The servitisation of business is moving industry to business models driven by customer demand. Customer satisfaction is connected with financial rewards, forcing companies to investigate in their users’ experience. User journeys describe how users manoeuvre through a service. Today, user journeys are typically modelled graphically, and lack formalisation and analysis support. This paper proposes to formalise user journeys as weighted games between the user and the service provider. We further propose a data-driven construction of such games, derived from system logs using process mining techniques. As user journeys may contain cycles, we bound the number of iterations in each cycle and develop an algorithm to unfold user journeys into acyclic weighted games. These can be model checked using Stratego to uncover potential challenges in how a company interacts with its users and to derive company strategies to guide users better in their journeys. Our analysis pipeline was evaluated on an industrial case study; it revealed design challenges within the studied service and could be used to derive suitable recommendations for improvement.