Keywords

1 Introduction

The use of process models for workflows has been studied for some decades now. It started back in 1979 with the work of Skip Ellis on office automation [9]. Still, it took two decades until notions such as workflow nets and soundness were defined [1] thus linking workflows to Petri nets. As a result of this link, a lot of existing Petri net theory (like [7, 14, 16, 18]) became instantly applicable to the workflow process model domain. Nevertheless, some other approaches to the verification of these models also still emerged, in which was used [19] another graph-like notation for processes in combination with dedicated graph reduction rules.

The application of Petri nets to the workflow domain [2, 3, 12] triggered a new line of research focussing on the soundness verification tool Woflan [28], different variations on soundness [5, 26], and extensions to the Petri net formalism (like EPCs [11, 24, 25], BPEL [15], and YAWL [29, 31]). Verbeek et al. [28] also introduced the concepts of the problematic runs (called sequences in that paper), which are used in this paper.

None of these approaches offered a comprehensive visualization of the problems using the process model of choice (YAWL, EPC, Petri net, etc.). For instance, the Woflan tool did not visualize the Petri net it was checking soundness on, but just showed a series of messages that included the labels of the nodes in the net. Nevertheless, the Woflan tool was later included in the process mining framework ProM [21, 25], which did allow this net to be visualized. As a result of this inclusion, selected markings (like deadlock markings) could be visualized by projecting them onto the net, and other Petri-net related properties (like invariants) could also be visualized. However, such visualization means are still limited and users struggle to diagnose real problems.

This paper takes this initial and rudimentary visualization of soundness problems in ProM some steps further by focusing on the visualization. Also, whereas Woflan requires a unique final marking (which should be reached to achieve success in the workflow), the approach in this paper allows for any collection of such final markings. By visualizing any problem that prevents the workflow from reaching any of these final markings, the user is guided towards correcting the root cause of these problems.

The concept of runs as shown by the visualization is known in the Petri net field, and originates from Desel [6]. An example tool that supports these runs is VipTool [4, 8]. VipTool can provide the user with information whether a given scenario (say, a partial trace) fits the Petri net at hand. In this paper, we assume that such a partial trace fits the net. If not, we can use alignments to find the closest path in the model [22]. This is not supported by the VipTool, but is supported by ProM. We are more interested in visualizing the execution of the fitting partial trace in the net. Apart from this, VipTool can also synthesize a Petri net from a collection of scenarios. This connects VipTool to the field of process mining [21], which is the natural habitat of ProM. However, we do not use that feature of the tool.

PSVis (Petri net Soundness Visualization) is a tool to spot problems in Petri nets by means of visualization. The tool aims at guiding expert users through the process models to get insight into the problems that cause the process model to be unsound.

2 Problem Definition

In this section we give definitions of the core concepts that our visualization tool needs to handle. We define the problem that we address, and present a set of tasks. We designed our visualization tool accordingly.

2.1 Problem Analysis

Process modelers tend to ensure the soundness property of the process models. However, it is fairly easy to break this property with only a small number of changes on the model. In addition, models which are derived by discovery algorithms do not always ensure this property. Well-known miners like the Alpha-miner and the Heuristic-miner often produce models that are not sound (e.g., have deadlocks).

Because of the dynamic nature of the behavior of the Petri nets, understanding where the problems occur and the context in which they happen plays a key role for process modelers.

In order to address this problem, we define the following tasks, which form the design basis of our tool:

 

T1 :

Obtain an overview of all or a subset of final states of a Petri net.

T2 :

Compare disjoint sets of transitions and/or places belonging to a specific area.

T3 :

Find problematic states.

T4 :

Explore paths that lead to a problematic state.

T5 :

Determine when the problem occurs for a specific problematic state.

T6 :

Analyze the runs for a selection of states.

T7 :

Examine concurrency, loops and causal order in runs.

 

This set of tasks has been composed in collaboration with experts in the area of process mining and Petri nets in order to address the problem on soundness validation. To support these tasks, we chose appropriate visual encodings and made an interaction design.

Fig. 1.
figure 1

Abstract representation of the concept of areas outlined by Verbeek et al. [27]. The state space is divided into three areas: Orange, Green and Red. Circles and arrows depict states of the state space and transitions, respectively. Two possible situations can occur in the Red area: deadlocks and livelocks, which are represented by circles without outgoing arrows and cycles. (Color figure online)

Full size image

2.2 Soundness Validation

We use an algorithm originally proposed by Verbeek [27] to compute the problematic states of a given Petri net. The output of the algorithm is used as input in our tool. The algorithm computes three sets of states, referred to as Orange, Green and Red areas. An abstraction of the resulting output of this algorithm is shown in Fig. 1.

In our tool, we focus on the border states, that is, the states which depict a transition from the Orange area to the either Green or Red area. In Fig. 1, the border states are linked by black-dotted arrows. Notice that there may be cases in which the same transition leads to different areas depending on the source state (e.g., t1 leads to Green and Red areas). These states correspond to parts of the Petri net in which everything becomes right (henceforth, all reachable states are Green) or everything becomes wrong (henceforth, all reachable states are Red).

The Red area contains all those states from which is not possible to reach any final state. Clearly, all reachable states from a Red state are Red states too. Thus, states within this area are considered as wrong states. On the other hand, the Green area represents those states from which a final state can always be reached. Similar to the Red states, from a Green state only Green states can be reached. Lastly, the Orange area comprises states from which some Red, Green and Orange states can be reached.

Within the Red area, two major problems can be present: deadlocks and livelocks. In Fig. 1, two problems are indicated with circles. Deadlocks occur when a state from which no transition can be fired is reached, and it is not a final state. This can be seen in Fig. 1 as the state has no outgoing edges, that is, no transition can be fired at that state. Livelocks happen when a cycle is found, which means that it is possible to iterate between a subset of states forever.

3 PSVis

In this section we introduce PSVis (Petri net Soundness Visualization), its components and how they interact in order to execute the tasks depicted in Sect. 2.1. An overview of all components is given in Fig. 3. Every component enables to perform a specific task or a set of tasks.

Our tool assumes that the state space is computable in a reasonable amount of time. If the state space contains unbounded places, it is infinite in size and cannot be computed. But even if all places are bounded, the state space may still be too big to be constructed within reasonable time [28]. To avoid having to spend unreasonable time in constructing the state space, our tool uses a threshold that operates on the number of tokens in a state. If the threshold is set to b, then only states where every place contains less than b tokens are expanded. This is related to the notion of b-boundedness introduced earlier. Thus, if all places are b-bounded in a net, then setting the threshold to b or higher does not change the state space. If the threshold is reached at some state, we assume that state is a problematic one.

3.1 Glyphs on the Petri Net

In order to support T1 (Obtain an overview of all or a subset of final states of a Petri net), process modelers need to visualize the number of tokens of a specific place, and the states that place belongs to. As a result, we introduce glyphs, which decorate places in a Petri net. Glyphs are visual representations of a piece of the data where visual attributes are dictated by data attributes [30].

The number of tokens in a place is represented as dot shapes contained in the place, numbers, or a combination of both. The main problem of this representation arises when we want to visualize more than one final state at the same time. A final state according to the definition is a multiset of places. This implies that a specific place can belong to more than one final state. With the current way of presenting this information, expert users are not able to know the number of tokens contained inside each place for each state and whether a place belongs to more than one state. Therefore, we propose a new way to visually encode this information. This new encode is shown in Fig. 4(b).

In our approach, the state with the highest number of unique places determines the color of the places. Glyphs are then colored with the remaining states. The initial state constitutes an exception and the places that belong to it are always colored accordingly. Figure 2 shows an example of how our approach works. When the user selects State 1, the two places that belong to it are colored red. Next, the user selects State 2 which has three unique places. Therefore, all the places are colored blue and two glyphs are created to present State 1. Lastly, when the user selects the initial state, two places are colored green and glyphs are created to show the remaining states.

If there is more than one token in a place, a label is attached to the glyph (or to the place) indicating the number of tokens. This label is colored dynamically depending on the brightness of the background color. Thus, labels can be colored black or white to make them readable.

Fig. 2.
figure 2

Assignment of colors to places when selecting states. From left to right, the evolution of the coloring of the places when a user selects states is shown. Glyphs decorating the places of the Petri net are created on demand. (Color figure online)

Full size image
Fig. 3.
figure 3

Overview of our tool. (1) displays a Petri net in which four places are colored: two in red, indicating the last state reached in the Red area, one in blue, indicating that token was consumed in order to reach the Red state, and one in golden, indicating the final state of the Petri net, which was selected in (1b). (2) shows all the available problematic states, some of them are highlighted indicating that the user selected those ones. Lastly, 3) shows the corresponding runs. (Color figure online)

Full size image
Fig. 4.
figure 4

Examples of the components of our tool: (a) component showing the initial and final states and their colors; (b) four different final states that involve the same place; (d) component showing a problematic state from which we can reach four different types of problems depending on the transition we fire. (Color figure online)

Full size image

3.2 Petri Net View

This is the main view of our tool. It presents the Petri net (see Fig. 3(1)) where circles and rectangles depict places and transitions. We implement a version of Sugiyama’s approach [20] to layout the Petri net since it gives a good understanding of the flow of the process. Some parameters of the layout algorithm can be modified through the toolbar at the top of the view. In addition, users can perform zooming, panning and dragging of elements directly on the view. Last but not least, nodes can be hovered in order to show the label of such element by using a tooltip.

To the right of the Petri net view, there is a panel which shows the initial and final states of the model. Each state is presented in the tool by two components: a button and a colored rectangle, which are interactive. This component can be seen in Fig. 4(a). The example shows one single initial and five final states. Users can (de)select states with this component and change the assigned colors. When a state is selected, the Petri net view reacts by showing the current selection of states. Given the fact that a single place can be present in multiple states, we use a new approach to represent that a place belongs to several states (see Fig. 2). This feature directly relates to task T1 (Obtain an overview of all or a subset of final states of a Petri net).

The top part of this view (Fig. 3(1a)) shows two sets of buttons that are dedicated to perform a quick exploration of the problems that have been detected. These buttons enable users to explore places or transitions that belong to just one area. This is useful because it gives a quick overview of the parts of the Petri net that belong to the Green/Red/Orange area. In order to do this, users can select what they want to visualize (places/transitions) and which area they want to explore (Green/Red/Orange). Once the user selects one of these options, the Petri net view highlights those elements which belong to the selected area. This feature relates to task T2 (Compare disjoint sets of transitions and/or places belonging to a specific area).

3.3 States View

This component can be seen in more detail in Fig. 4(c) and it enables the exploration of the most important problematic states within the state space of the Petri net (T3 (Find problematic states)). Those states correspond to scenarios in which the process can lead from an Orange state to either a Green or Red state. This component only shows the border cases, which are derived from the relevant transitions of the state space (see Fig. 1).

Our approach uses a two-level tree to visualize the different states in which the net experiences a problem. The first indicates the states in which an Orange-to-Red or Orange-to-Green scenario was found, and the second level indicates the transition that is involved in the detected scenarios. For each state, the user can find a variable number of transitions that could trigger a step in the state space leading from an Orange state to a Green state, or a Red state in which two situations can ultimately happen: deadlock or livelock. This part relates to T5 (Determine when the problem occurs for a specific problematic state) since they show where (state and transition) problems occur.

In some cases, the algorithm that our tool uses detects a problem only because of the threshold that it uses. In those cases, this component indicates that by marking the problematic state with an asterisk. In this way, users can easily differentiate those states that are always problematic from those that are problematic because the algorithm did not continue exploring.

We use icons to give a quick overview of the scenarios found by the algorithm. They indicate the scenario for a specific state (aggregated view) and for a specific transition (specific view). Therefore, the first level of the tree might display multiple icons indicating all the possible scenarios that can be reached through that state. Seven scenarios are possible: (1) reaching a Green state; (2) a Red state that eventually leads to a deadlock is reached; (3) a Red state that eventually leads to a livelock is reached; (4) a Red state from which a deadlock and livelock can be reached; (5) either a Green state or a Red deadlocking state can be reached; (6) either a Green or a Red livelocking state can be reached; and (7) either a Green or Red dead/live-locking state can be reached.

The nodes of the tree can be sorted by three different criteria. By clicking on the corresponding radio buttons, the view sorts the states by the criterion chosen by the user. Thus, users can sort states by the type of scenario that they represent (either Green or Red) and the cardinality of the states.

Next to the sorting functions there is a spinner, which is used to set the threshold used by the algorithm that computes the state space. By default, this parameter is set to 1. When the user interacts with the spinner, the tool recomputes the state space, partitions the recomputed state space into Green, Red and Orange, and recomputes all the relevant information related to them, such as runs or disjoint sets of states and transitions.

Users can interact with the nodes of the tree to explore the different scenarios. This way, the nodes can be selected to be displayed in the Petri net view. When a node from the first level of the tree is selected, the main view shows all the available scenarios for that specific state by coloring the nodes of the Petri net that are involved in that specific state. In Fig. 3 state {p_ocancel, p4} is selected. The places that define the selected state are colored blue, while the transitions that can be triggered leading the process to a Green or Red state are colored green and red.

Once users select a (set of) state(s), it is possible to interact with the main view to explore the behavior of the net. This is done by enabling users to click on the transitions that have been colored to show the paths that lead to the selected state, and the final marking reached by triggering that transition. This feature connects this view and the runs view, which is described below.

3.4 Runs View

This view helps users perform tasks T4 (Explore paths that lead to a problematic state) and T6 (Analyze the runs for a selection of states). An example is shown in Fig. 3(3). Runs are displayed as disconnected graphs, which can be projected as paths in the Petri net view. When users select a state from the states view, this component shows the runs that lead to the chosen states. Then, two major interactions are provided: nodes hovering, and path selection. On the one hand, the first interaction aids users in linking nodes of the runs to nodes of the Petri net view. On the other hand, the second interaction assists in visualizing the path that goes from the initial state to the selected state directly on the Petri net.

Through these two interactions, users can detect states that share similar segments of path, helping users get insights into the problematic scenarios of the model.

There is a third interaction which links directly with the Petri net view. When the user clicks on a transition that is involved in the problematic scenario that the user is exploring, the Petri net view takes the run that leads to the ultimate state reachable from the current state, that is, a deadlock or livelock, and shows the path. Providing the context in which the process ends up in a Red state helps the user to understand how the process led to that problem.

3.5 Design Decisions

The design decisions made in this work support some basic notions on human perception [13]. The usage of glyphs to represent the belonging of a place to different states is a natural way to show that type of information. They are located next to the elements for which they provide information, and they use a basic color code to show the state that they represent. We use this notation since it is known that the color is a cognitively effective visual variable [13]. Also, we use colors to display useful information on top of the Petri net. We consider this approach to be acceptable since the usage of other ones (e.g., shapes) would probably interfere with the Petri net notation itself. Even though color representations are a limitation for our tool, we consider satisfactory for the purposes of this work.

3.6 Implementation Details

Our tool is implemented as a plug-in within the ProM [23] framework using Java v6. Prefuse [10] is used to manage the graph structures and the visual properties of the visualization of the Petri net. The jBPT library [17] for Petri nets is used to compute the runs.

4 Use Cases

In this section we demonstrate how our tool can be used to assess Petri nets. We focus on two nets, which were designed by students who participated in the study developed in [28]. These nets include information on initial and final states.

The first case exposes an example in which no final state can be reached. Figure 5 summarizes this use case. It shows an overview of the Petri net and an area of interest in more detail. As can be seen, there are no problematic states in the states view. However, we observe that some of the places are colored red, which means that this place can contain tokens but that no final state can be reached from any state in which this place contains tokens, and some are not colored at all. The latter places do not appear in the state space, which means they are not reachable since if they were reachable, they would be either colored or present in the problematic states view. The final state is also not colored, and therefore the process can never reach the final state. Observe that all three input places of the book_hotel_... transition can contain tokens, but the single output place cannot. Apparently, not all input places of this transition can contain tokens at the same time. The source of this problem can be found in the second place from the left in the overall net, which corresponds to a three-way choice. If the highlighted path is chosen, then only one of the input places can contain a token, otherwise only the other two can contain tokens.

Fig. 5.
figure 5

Screenshots of the usage of the tool for a dataset. (Color figure online)

Full size image
Fig. 6.
figure 6

Screenshots of the usage of the tool for a dataset. (Color figure online)

Full size image

The second use case (Fig. 6) depicts a Petri net in which several problematic scenarios have been found. Initially, we proceed by exploring the disjoint sets of places and transitions. We can easily spot some straightforward paths that lead to the final state as well as some paths that eventually finish in the Red area (Fig. 6(a)). Furthermore, we see some places and transitions that have not been colored. We now focus on those elements in order to explore what occurs there. By hovering on some of the places that have not been colored, we can see their labels. One interesting place is the one labeled as Status7 since it is present in three of the problematic states shown in the states view. We pick one of those states to explore the runs that lead to that problematic state. The tool shows two different runs (see Fig. 6(a)). By looking at these, we can see that they share some of the initial steps in the process, but that they divert at some point. Clicking a run visualizes the paths that those runs represent in the Petri net. If we compare the two runs in this way, we immediately see that they finish in the same problematic state, although they followed different paths. We can also see where the deadlock occurs by clicking on the transition colored red. Figure 6(b) shows the two paths (edges colored blue) for the two runs, as well as the deadlock that is reached (place colored red). The place colored blue indicates that the token must be consumed by firing the red transition.

5 Conclusion

We have presented PSVis, a tool to visually assess the soundness of a Petri net. We have formulated the most important analysis tasks, and have demonstrated the usage of our tool through the exploration of two Petri nets. The first use case showed a simple scenario in which we discovered why the final state was not reachable. The second use case represented a more complex example in which more actions were performed. Through different actions, we observed different aspects of the Petri net such as deadlocks and common paths that lead to them.

One of the main limitations of our tool is that it relies on the state space, which cannot not always be computed in reasonable time. Even though we have some workarounds (setting a threshold to limit the computation of branches), it may take a considerable amount of time to finish. We plan to study alternatives to compute the parts of the state space that are used in the analysis. One option might be to explore the state space incrementally by computing just portions of it.

In future work we aim to perform experiments to compare different approaches for displaying the runs since the current representation lacks of an explicit way to display loops and concurrency, which would help to perform task T7 (Examine concurrency, loops and causal order in runs).