User journey games: automating user-centric analysis

Consider a company, Amend ltd., that offers document reviewing services: Users submit documents and meta-data to receive a professional review. To ensure user satisfaction, the company commissions a report on the users’ experience with the offered service. A team of analysts conducts interviews with selected users to manually create user journey maps that reveal unknown pain points in the service, which could cost the company users. When expanding and improving its services, Amend wants to integrate continuous user feedback, and wonders if the team could use system logs to avoid the cumbersome manual questionnaires and scale the feedback to all users. However, their current performance dashboards [1] only display recent server statistics without incorporating user-centric analysis. Methods and tools to analyze user experience based on such large-scale collected logs are currently lacking [2]. In this paper, we present a method to automatically analyze logs from the users’ perspective, based on weighted automata [3].

The scenario described above stems from the servitization of business [4], a concept of creating added value to products by offering services. Servitization of business is a major practice embraced by most (if not all) successful companies today. Companies are interested in the analysis of their services, which traditionally focus on the managerial perspective, where the service is analyzed with respect to the companies’ view. Recent trends shift the focus from the company’s to the end-users’ view, where a positive experience and impression that a user has while engaging in the service, has shown to have a positive impact on the financial reward of a company [5]. Thus, companies aim to analyze and improve their services, based on their users’ satisfaction.

User journeys (also called customer journeys) analyze services from the user perspective [6]: A user journey is inherently a goal-oriented process, because humans engage in a service with a goal in mind. The user moves through the journey by engaging in so-called touchpoints, which are either actions performed by the user or a communication event between the user and a service provider. We here assume that users only engage in one touchpoint of a service at a time.

Tools to analyze user journeys are currently lacking [2], which hinders their operational use. User journey diagrams are usually generated by hand, and the user perspective is derived from interviews with experts and users, e.g., [6, 7]. This process has been highly successful, discovering points of failure in the studied services and, as a result, providing advice to companies on how to improve their services. However, this manual process is best suited for relatively small services and a restricted number of users, and a particular point in time. For services with thousands of users, journey diagrams need to be automatically generated and analyzed. In particular, in business processes that change often, the impact of these changes needs to be evaluated as quickly as possible. Concept drift detection quantifies changes in an underlying business process [8]. However, not all observed changes are easy to detect, since they might originate from events out of the company’s reach, but are still perceived from the users’ point of view. Thus, systematic analysis techniques are needed to evaluate user journeys, and detect and stop unwanted trends.

This paper formalizes user journeys as weighted games [3, 9] between users and a service provider, and proposed a method to derive such games from system logs. Our aim is to use these games to analyze services and suggest service improvements such that service providers always have a strategy to guide their users toward a desired goal. The aim of our work is to reduce the gap toward fulfilling the analysis needs of companies such as Amend, the company of the motivating scenario above. In short, our contributions are: User journey games systematically capture the user perspective of services by means of so-called gas. The term is inspired by blockchain technology such as Ethereum, where gas refers to the cost necessary to perform a transaction on the network. In our work, the gas quantitatively reflects how moves in the user journey contribute to the users reaching their goal. Consequently, the moves in the derived games are weighted and accumulated into the gas of the journeys, which allows journeys to be analyzed and compared using model checkers such as [10] or PRISM-games [11], and to give strategic recommendations to service providers.

This is an extended version of a paper that appeared at SEFM 2022 [12]. Compared to that paper, we have here expanded the discussion of user journey games, introduced a time-driven analysis method for user journeys (henceforth called a sliding-window analysis) which extends the analysis pipeline based on user journey games, and expanded our experimental evaluation to a significantly bigger data set. A sliding-window analysis uses a series of automatically generated user journey games, where each game is automatically derived from a time window in the system log. We lift the model checking analysis to the series of games to uncover trends and changes over time.

Outline. Sect. 2 discusses related work. Section 3 provides background on weighted games and the model checking suite that we use for analysis. The formal model for user journeys is introduced in Sects. 4–6, model checked in Sect. 7, and extended to a sliding-window analysis in Sect. 8. Section 9 discusses the implementation, Sect. 10 evaluates our approach experimentally in terms of an industrial case study, Sect. 11 discusses our approach and Sect. 12 concludes the paper.

We discuss related work on the modeling of user journeys and on using data-driven techniques to discover user journeys, Table 1 summarizes related work and positions our contributions. We are not aware of prior work that uses automatic verification methods to analyze user journeys.

User journeys aim to improve service design by describing how users interact with services [32, 33]. Modeling notations for user journeys aim to support the so-called blueprinting [13], i.e., to create an anticipated model of a service. There are various notations to create diagrams for user journeys [6, 14‐18]; these diagrams are mostly handmade and only limited digital support exists; for example, a semantic lifting into ontologies has been used to visualize fixed aspects of a model [15]: the data sent, the communication channels and devices used, etc. Berendes et al. propose in [16] the high street journey modeling language (HSJML) tailored to journeys in shopping streets. Razo-Zapata et al. propose the VIVA modeling language with focus on interactions [17]. In contrast, our work aims to use data-driven techniques [19] to automatically discover user journey diagrams and formal methods to automatically check properties of user journeys and derive recommendations for improving the service under analysis. The aim with our work is to automate the labor-intensive manual mapping that captures the user’s interaction with a service, thereby enabling scalability of user-centric analysis of complex services with many users.

The customer journey modeling language (CJML) [7, 34] captures the end-users’ point of view. CJML distinguishes planned and actual user journeys, which represent the journey as planned as part of the service design and as perceived by the user, respectively. Our work is part of a project [2] on tool support for data-driven user journey modeling in CJML. Whereas previous work on CJML manually quantifies user experience collected through user feedback questionnaires, our work aims to capture the journeys as perceived by the user in a data-driven manner, based on system logs.

Data-driven techniques for process discovery allow us to discover user journeys. Harbich et al. [20] use mixtures of Markov models to derive user journey maps. Bernard et al. [21, 22] study process mining [19] for user journeys, such as hierarchical clustering to explore large numbers of journeys [23] and process discovery techniques to generate user journey maps at different levels of granularity [24]. Terragni and Hassani [25] apply process mining to user journey web logs to build process models, and improve the results by clustering journeys. This work has been integrated with a recommender system to suggest service actions that maximize key performance indicators [26], e.g., how often the product page is visited. David et al. present TAPPAAL [27], a tool for analyzing timed-arc Petri nets, realized through mappings to UPPAAL. Bertolini et al. used TAPAAL for the verification of medical processes [28]. They focus on the graphical notation language Little-JIL, leaving the human aspect for future work. In contrast, our work focuses on the user-centric perspective, using games to model actual user behavior [12]. In this paper, we propose and use a data-driven method to automatically construct formal models of user-centric journeys with multiple actors. Complementing the work presented here, we have studied the scalability of the basic mining technique for user journey games [35] and the integration of the strategies derived from user journey games in an actor-based simulation framework for user journeys [36].

The above-mentioned work inherently assumes that the analyzed collection of journeys is generated from an unchanged process. Bose et al. define different types of process changes, so-called concept drifts, and propose their detection based on follows- and precedes-relations at the event level with hypothesis testing [8], recent developments on concept drift are surveyed by Sato et al. [29]. Banham et al. extend process models with periodically recorded numerical values to gain closer insights into exogenous influences on a process [30, 31]. In contrast, our proposed sliding-window analysis does not investigate changes at the event level, but quantifies changes in the user journey over time, abstracting from the business process, thereby enabling the service provider to quantify the impact of intented as well as unintended changes on the user journey.

We briefly summarize the formal notations and tools that we build on for the proposed user journey pipeline to analyze a service.

A transition system [37] is a tuple \(S=\langle \Gamma , A, E, s_0, T \rangle \) with a set \(\Gamma \) of states, a set A of actions (or labels), a transition relation \(E \subseteq \Gamma \times A \times \Gamma \), an initial state \(s_0\in \Gamma \) and a set \(T \subseteq \Gamma \) of final states. A weighted transition system [38] \({\mathcal {S}} = \langle S,w \rangle \) extends the transition system S with a weight function \(w: E \rightarrow {\mathbb {R}}\) that assigns weights to transitions.

Weighted games [9] are obtained from weighted transition systems by partitioning the actions A into controllable actions \(A_c\), and uncontrollable actions \(A_u\), where only actions in \(A_c\) can be controlled by the analyzer, while actions in \(A_u\) are nondeterministically decided by an adversarial environment. When analyzing games, we look for a strategy that guarantees a desired outcome, i.e., winning the game by reaching a certain state. The strategy is given by a partial function \(\Gamma \rightarrow Act_c \cup \{\lambda \}\) that decides on the action of the controller in a given state (here, \(\lambda \) denotes the “wait” action, letting the adversary move). [39] can be used to analyze reachability and safety properties for games expressed using (timed) transition systems, extending the model checker [40]. checks whether there is a strategy under which the behavior satisfies a control objective, denoted   for a property P. Property P is expressed in computational tree logic [41], an extension of propositional logic that is used to express properties along paths in a transition system. Recall that computational tree logic state properties \(\phi \) can be decided in a single state; while reachability properties \(\,\phi \) express that the formula \(\phi \) is satisfiable in some reachable state in a transition system; safety properties   \(\phi \) express that the formula \(\phi \) is always satisfied in all the states of some path in a transition system and \( \,\phi \) expresses that \(\phi \) is always satisfied in all the states of all paths of a transition system. Similarly, liveness properties express that the formula \(\phi \) will eventually be satisfied in all the paths in a transition system and the formula expresses that satisfying formula \(\phi \) leads to satisfying formula \(\psi \). [10] can be used to analyze and refine a strategy generated by with respect to a quantitative attribute like weights. is a statistical model checker [42]; it extends for stochastic priced timed games and combines simulations with hypothesis testing until statistical evidence can be deduced.

In user journey games, the edges E model the touchpoints, \(A_c\) the actions initiated by the service provider, \(A_u\) the actions initiated by the user, and \(T_s\) the successful goal states.

The process of deriving such user journey games from system logs is illustrated in Fig. 1. In a first step, we go from logs to a user journey model, expressed as a directly follows graph (DFG), and in a second step, the DFG is extended to a game. The derivation of weights for the transitions is discussed in Sect. 5.

We extend the games derived from system logs into weighted games by defining a gas function reflecting user feedback. The gas function will be automatically calculated and applied to the transitions of the game, depending on the traversal and entropy present in the system log. Informally, the gas function captures how much “steam” the consumer has left to continue the journey. With less steam, the user is more likely to abort the journey and with more steam, the user is more likely to complete the journey successfully. If the service provider attempts to provide the best possible service, its goal is to maximize gas in a journey. The adversarial user aims for the weaknesses in the journey and therefore minimizes the gas. Formally, the weight function \(w: E \rightarrow {\mathbb {R}}\) maps the transitions E of a game to weights, represented as reals. Given a log L and its corresponding game, we compute the weight for every transition \(e \in E\).

Since user journeys are inherently goal-oriented, we distinguish successful and unsuccessful journeys; the journeys that reach the goal are successful and the remaining journeys are unsuccessful. This is captured by a function \({{\,\textrm{majority}\,}}: E \times L \rightarrow \{-1,1\}\) that maps every transition \(e \in E\) to \(\{-1,1\}\), depending on whether the action in the transition appears in the majority of journeys in L that are unsuccessful or successful, respectively. Ties arbitrarily return \(-1\) or 1.

Many actions might be part of both successful and unsuccessful journeys. For this reason, we use Shannon’s notion of entropy [44]. Intuitively, if an action is always present in unsuccessful journeys and never in successful ones, there is certainty in this transition. The entropy is low, since we understand the context in which this transition occurs. In contrast, actions involved in both successful and unsuccessful journeys have high entropy. The entropy is calculated using The entropy H of transition e given the system log L is now defined asThe weight function w that computes the weights of the transitions can now be defined in terms of the entropy function, inspired by decision tree learning [45]. Given a system log L, the weight of a transition e is given byThe constant C represents an aversion bias and is learned from the training set. It is used to model a basic aversion against continuous interactions. The sign of a transition depends on its majority. If the transition is mostly traversed on successful journeys, it is positive. Otherwise, it is negative. The inverse entropy factor quantifies the uncertainty of transitions. The constant M scales the energy weight to integer sizes (our implementation currently requires integer values, see Sect. 9).

The gas quantitatively reflects the history of a journey, allowing us to not only compare the weights of transitions but also to compare (partial) journeys. The gas \({\mathcal {G}}\) of a journey \(J = \langle a_0, \dots , a_n \rangle \) with transitions \(e_0, \dots e_{n-1}\) is defined as the sum of the weights along the traversed transitions:

The generated weighted games may contain loops, which capture unrealistic journeys (since no user endures indefinitely in a service) and hinder model checking. Therefore, the weighted games with loops are transformed into acyclic weighted games using a breadth-first search loop unrolling strategy bounded in the number of iterations per loop. The transformation is implemented in an algorithm that preserves the original decision structure and adds no additional final states.

The algorithm for k-bounded loop unrolling (shown in Algorithm 1) returns an acyclic weighted game, where each loop is traversed at most k times. The unrolling algorithm utilizes a breadth-first search from the initial state \(s_0\) in combination with loop counting to build an acyclic weighted game. In the algorithm, the state s denotes the current state that is being traversed. To traverse the paths in the weighted game, we use a queue Q to store the states that need to be traversed, a set C containing all the cycles in the graph (where each cycle is a sequence of states), and the function allSimplePaths \(\textsc {(G,s,T)}\) that returns all paths in the weighted game G from s to any final state \(t \in T\). The extended graph is stored in the acyclic game \(G'\). A state in a cycle can be traversed if it has been visited less than k times (see Lines 9–10). The function repetitions checks the number of traversals. If the counter for one cycle is k, the algorithm checks whether the cycle can be partially traversed (see Lines 11–16).

Partial traversals guarantee that we reach a final state without closing another loop. The partial traversal does not increase the count of another cycle to \(k+1\) (Lines 14–16). Every state stores its history (a sequence of visited states), which can be retrieved using the function history. Line 14 increases the current history by including a (partial) path through the loop. This check iterates through all paths from the current state to any final state. If state t can be traversed, it is added to the acyclic game (Lines 17–20). A copy \(t'\) of t is added to the queue Q, the transition \((s, t')\), its weight and actor are added to \(G'\) using the function addTransition. If a final state is copied, the new set of final states is updated (i.e., \(T' \leftarrow T' \cup \{ t'\}\)). The resulting weighted game can be reduced. All copies of states outside a cycle can be merged into the same state. This can either be done after unrolling the whole game or on the fly while unrolling.

In this section we describe how to model check properties for user journeys and generate strategies to improve user journeys, using acyclic weighted games. The analysis of a weighted game gives formal insights into the performance of a service. We introduce generic properties that capture the user’s point of view on a user journey. The analysis in this paper uses the Stratego extension for [10], which supports non-deterministic priced games and stochastic model checking. Stratego allows to model check reachability properties within a finite number of steps, when following a strategy (therefore the need for acyclic games). Stratego constructs a strategy that satisfies a property P, so that the controller cannot be defeated by the non-deterministic environment. We detail some strategies and properties of interest for games derived from user journeys.

The analyses discussed in the previous sections inherently assume that the system logs are generated from an unchanged process; i.e., the data is recorded under equivalent system settings. In a fast-paced business setting, changes and updates are constantly developed, integrated, and evaluated. Recorded data may no longer be representative of the current state of the system. Nevertheless, practitioners are interested in the effectiveness and impact of their changes, motivating the need for time-driven user journey analysis. The recorded data cannot be interpreted as one, coherent data set but must be analyzed in correspondence with their temporal information. Journey records before and after system-level changes are not recorded from the same process: issues observed in earlier journeys might be resolved at later stages and other issues only appear in later journeys. When analyzing massive system logs collected over a long time, the impact of architectural changes might be buried. Mixing journeys from different data-generation processes skews the evaluation of changes and newly introduced features in a system.

We now introduce steps to leverage the previous analysis method into a time-driven analysis and consider points in time over the time domain \({\mathbb {R}}^+\). Hence, we define time points for every user journey, e.g., the start of the journey, and split the log into sub-logs containing only journeys in the same interval, e.g., all journeys starting within 10 days. For every sub-log, an individual user journey game is generated and stored in a sequence of games. Model checking the sequence of games individually returns a time series over the single model checking results, revealing the impact of changes in the user journey over time. Given a log L, let \({\mathcal {I}} \subset {\mathbb {R}}^+\) be a finite sequence of time-points \({\mathcal {I}} = \langle {{\,\textrm{tp}\,}}_1, \dots , {{\,\textrm{tp}\,}}_n \rangle \) with \({{\,\textrm{tp}\,}}_i \in {\mathbb {R}}^+\); e.g., \({\mathcal {I}}_{{{\,\textrm{days}\,}}}\) contains time-points for every 24 hours between the first and last day of the timestamps present in L (mapped into the domain of \( {\mathbb {R}}^+\)). Given a constant window size \(\mu \in {\mathbb {R}}^+\), we let \(W_i = [ {{\,\textrm{tp}\,}}_i, {{\,\textrm{tp}\,}}_i + \mu ]\) denote a window that represents a time interval spanning from time-point \({{\,\textrm{tp}\,}}_i \in {\mathcal {I}}\) to \({{\,\textrm{tp}\,}}_i + \mu \).

Given an event a in a journey J, the time function \(\delta (J,a)\) denotes the timestamp of a in J (mapped into the domain of \({\mathbb {R}}^+\)); e.g., the timestamp of the first or last event in a journey. The sliding-window analysis can be adapted to focus on different events by selecting other events as the second argument to \(\delta \); e.g., users finishing their journeys in the same window or users experiencing a particular event in the same window. We ignore the second argument to the function \(\delta \) if we use the first event in a journey \({a_0}\) to select the timestamp of the initial event in a journey \(J = \langle a_0, \dots , a_n \rangle \). In the sequel, we focus on sliding-window analysis based on the initial event of the journeys, and therefore, we write \(\delta (J)\) when the second argument is \(a_0\).

The sub-log \(L_i \subset L\), defined over the window \(W_i\), includes all journeys in L that are contained in \(W_i\), formally \(L_i = \{J \in L \mid \delta (J) \in W_i\}\). Thus, a journey \(J \in L\) is in \(L_i\) if \(\delta (J)\) is in the window \(W_i\). We define a sliding-window log \({{\,\mathrm{{\mathbb {L}}^{\mathcal {I}}_\mu }\,}}= \langle L_1, \dots , L_{|{\mathcal {I}} |} \rangle \) to be a sequence of sub-logs over L, where journeys are grouped based on the windows \(W_i\) ranging over time stamps \({\mathcal {I}}\) and window size \(\mu \).¹ Observe that sliding-window logs contain complete journeys; i.e., journeys are not split by the window size if they are not completed within a window. Figure 3 shows (in red) the first sub-log \(L_1\) of the sliding-window log \(W_1\) grouped by journey start time (the timestamp of the first event), the top-most journey (in white) is not in \(L_1\) as it starts outside the window size \(\mu \).

We analyze sliding-window logs to uncover changes over time from the user’s perspective. For every log \(L_i\) in a sliding-window log \({{\,\mathrm{{\mathbb {L}}^{\mathcal {I}}_\mu }\,}}\), we construct the corresponding user journey game; the resulting sequence of user journey games is denoted \({{\,\mathrm{{\mathbb {G}}^h}\,}}\), where h denotes the chosen h-sequence refinement. Each user journey game might contain loops and require unrolling to ensure that the analysis of queries terminates. Given an unrolling parameter k, we construct \({{\,\mathrm{{\mathbb {G}}^h_k}\,}}\), which contains the sequence of k-bounded loop-unrolled user journey games from \({{\,\mathrm{{\mathbb {G}}^h}\,}}\).

The games of the sequence \({{\,\mathrm{{\mathbb {G}}^h_k}\,}}\) are individually model checked, resulting in a time-series of strategies and statistics describing the user journeys. Queries might depend on each other; e.g., properties using the strategy depend on its prior successful establishment. In case cannot be established, all depending queries are mapped by default to a predefined constant. As multiple queries from a sequence of queries Q can be used on every user journey game \(G_{L_i}^h \in {{\,\mathrm{{\mathbb {G}}^h_k}\,}}\), the result is a series of vectors \(Q_{{{\,\mathrm{{\mathbb {G}}^h_k}\,}}}\) describing the analysis of the user journey games over time. Every query \(q_i \in Q\) has a well-defined solution space \(S_i\); e.g., queries return strategies that map states to actions, expectation queries return values in \({\mathbb {R}}^+\) (expectation values with confidence intervals). Thus, each result vector \(\nu \in Q_{{{\,\mathrm{{\mathbb {G}}^h_k}\,}}}\) has \(|Q |\) entries, one result for each query \(q_i\). The space of \(\nu \) is defined by the solution spaces \(S_i\) of the corresponding queries \(q_i\), therefore

\(\nu : S_1 \times \dots \times S_{|Q |}\). By comparing the analysis results in \(Q_{{{\,\mathrm{{\mathbb {G}}^h_k}\,}}}\), we can gain insights into the temporal changes occurring in the user journeys of a system.

This section describes the implementation of the analysis pipeline detailed in Sects. 4–8. We focus on the implementation decisions made along the pipeline to facilitate the analysis. A source repository for our work on user journey games is available online [46].

The pipeline is implemented in Python. The input to the pipeline is a system log of a service provided by a company, and optionally a window size and time-points. The output is either a single model or a sequence of models (if the window size and time-points are given). Sequences of models are generated by repeatedly calling the single window construction for all sub-logs. The returned models can be model checked by either the proposed properties in Sect. 7 or by other custom-made properties using .

In this section we evaluate the pipeline for user journey analysis from Sect. 9 experimentally. We aim to answer the following research questions:The evaluation was done on an industrial case study from the company GrepS. We describe the context for the system logs provided by GrepS in Sect. 10.1, the experimental design and setup for our experiments in Sect. 10.2 and the results we obtained in Sect. 10.3. The results are discussed from the industrial perspective of GrepS in Sect. 10.4 and threats to validity are considered in Sect. 10.5.

In this section, we discuss two perspectives on the work reported in this paper. First, its possible implications on industrial practice and how practitioners work with user journeys. Second, its possible implications on theory development and how researchers work with formal methods. In summary, we believe that automated analyses techniques open for novel and less labor-intensive ways of working with user journeys. We further believe that data-driven model construction combined with automated analysis techniques, as investigated in our work, open up novel ways of working with formal methods and novel application domains for the techniques of our community.

This paper introduces a novel analysis pipeline for user journeys, based on the data-driven generation of formal models. Our generated models are weighted games, where the weights reflect user experience. The model construction is not subject to human inference but is built from system logs. Both single games, derived from a log, and sequences of games, derived from a sliding-window view of a log, are considered. The paper proposes a method to automatically analyze derived models to gain insights into the user journeys of a service, by means of queries using the model checker. To the best of our knowledge, this is the first automatic analysis pipeline using formal methods in the context of service science and user journeys.

The proposed analysis pipeline was evaluated on an industrial case study and revealed challenges to the planned user journey of the service provider. The analysis of the derived game demonstrated that users’ experiences fall in their accumulated feedback during the initial phases of the service. Our recommendations were reviewed and approved by an expert on user feedback in the company. We further performed a sliding-window analysis on a system log spanning two years, which suggested that a number of changes had occurred in the user journey. The company expert reviewed the detected changes and found that they aligned with key moments in the company’s history. We finally showed that our analysis method can analyze user journeys for groups of users, filtering the log that generates the weighted games, to improve interaction with specific customer groups.

The work presented here opens many interesting possibilities for further work, both in formal methods and in service science. Our work so far has assumed that users and service providers have perfect knowledge of each other’s possible actions. On the formal methods side, we therefore plan to study imperfect information games for user journeys with incomplete knowledge about user actions in the setting of, e.g., PRISM-games [11]. Furthermore, our current work is restricted by a fixed bound on loop unrolling; it would be interesting to directly analyze cyclic models. On the service science side, we plan to integrate our work with existing modeling languages for user journeys, such as CJML [7, 34], to automate the analysis of user journey models that are manually reviewed today, and to provide feedback from our analysis in the visual language of these models. Finally, the analysis of sequences of formal models for concept drift [29] seems highly interesting to us; a starting point here could be methods for change point detection in a time-series by means of cost functions [50].