With the emergence of service orientation as a major business driver, companies crucially depend on understanding the flow of their services from the user’s perspective. Models of these user journeys help to create a common understanding, but in practice their availability is limited. Process mining addresses the challenge of creating models that enable processes to be analyzed. Our goal is to mine user journey models. In this paper, we use automata learning algorithms to create behavioral models of stochastic user behavior from a given data set. The initially learned automaton is annotated with time and cost variables to capture aspects of the user experience. In a game scenario, we can model check properties of these enriched automata regarding the user behavior. Using Uppaal, we can synthesize strategies for nudging users into a different behavior. The approach is illustrated in a case study with a large dataset describing user behavior for a well-known music streaming application. Can we synthesize a strategy that nudges a computer science professor to take a path on the wild side of the usual listening habits?