TY  - JOUR
A1  - Ihde, Sven
A1  - Pufahl, Luise
A1  - Völker, Maximilian
A1  - Goel, Asvin
A1  - Weske, Mathias
T1  - A framework for modeling and executing task
BT  - specific resource allocations in business processes
JF  - Computing : archives for informatics and numerical computation
N2  - As resources are valuable assets, organizations have to decide which resources to allocate to business process tasks in a way that the process is executed not only effectively but also efficiently. Traditional role-based resource allocation leads to effective process executions, since each task is performed by a resource that has the required skills and competencies to do so. However, the resulting allocations are typically not as efficient as they could be, since optimization techniques have yet to find their way in traditional business process management scenarios. On the other hand, operations research provides a rich set of analytical methods for supporting problem-specific decisions on resource allocation. This paper provides a novel framework for creating transparency on existing tasks and resources, supporting individualized allocations for each activity in a process, and the possibility to integrate problem-specific analytical methods of the operations research domain. To validate the framework, the paper reports on the design and prototypical implementation of a software architecture, which extends a traditional process engine with a dedicated resource management component. This component allows us to define specific resource allocation problems at design time, and it also facilitates optimized resource allocation at run time. The framework is evaluated using a real-world parcel delivery process. The evaluation shows that the quality of the allocation results increase significantly with a technique from operations research in contrast to the traditional applied rule-based approach.
KW  - Process Execution
KW  - Business Process Management
KW  - Resource Allocation
KW  - Resource Management
KW  - Activity-oriented Optimization
Y1  - 2022
U6  - https://doi.org/10.1007/s00607-022-01093-2
SN  - 0010-485X
SN  - 1436-5057
VL  - 104
SP  - 2405
EP  - 2429
PB  - Springer
CY  - Wien
ER  - 
TY  - JOUR
A1  - Yousfi, Alaaeddine
A1  - Batoulis, Kimon
A1  - Weske, Mathias
T1  - Achieving Business Process Improvement via Ubiquitous Decision-Aware Business Processes
JF  - ACM Transactions on Internet Technology
N2  - Business process improvement is an endless challenge for many organizations. As long as there is a process, it must he improved. Nowadays, improvement initiatives are driven by professionals. This is no longer practical because people cannot perceive the enormous data of current business environments. Here, we introduce ubiquitous decision-aware business processes. They pervade the physical space, analyze the ever-changing environments, and make decisions accordingly. We explain how they can be built and used for improvement. Our approach can be a valuable improvement option to alleviate the workload of participants by helping focus on the crucial rather than the menial tasks.
KW  - Business process improvement
KW  - ubiquitous decision-aware business process
KW  - ubiquitous decisions
KW  - context
KW  - uBPMN
KW  - DMN
Y1  - 2019
U6  - https://doi.org/10.1145/3298986
SN  - 1533-5399
SN  - 1557-6051
VL  - 19
IS  - 1
PB  - Association for Computing Machinery
CY  - New York
ER  - 
TY  - BOOK
A1  - Smirnov, Sergey
A1  - Weidlich, Matthias
A1  - Mendling, Jan
A1  - Weske, Mathias
T1  - Action patterns in business process models
N2  - Business process management experiences a large uptake by the industry, and process models play an important role in the analysis and improvement of processes. While an increasing number of staff becomes involved in actual modeling practice, it is crucial to assure model quality and homogeneity along with providing suitable aids for creating models. In this paper we consider the problem of offering recommendations to the user during the act of modeling. Our key contribution is a concept for defining and identifying so-called action patterns - chunks of actions often appearing together in business processes. In particular, we specify action patterns and demonstrate how they can be identified from existing process model repositories using association rule mining techniques. Action patterns can then be used to suggest additional actions for a process model. Our approach is challenged by applying it to the collection of process models from the SAP Reference Model.
N2  - Die zunehmende Bedeutung des Geschäftsprozessmanagements führt dazu, dass eine steigende Anzahl von Mitarbeitern eines Unternehmens mit der Erstellung von Prozessmodellen betraut ist. Um trotz dieser Tendenz die Qualität der Prozessmodelle, sowie ihre Homogenität sicherzustellen, sind entsprechende Modellierungshilfen unabdingbar. In diesem Bericht stellen wir einen Ansatz vor, welcher die Prozessmodellierung durch Empfehlungen unterstützt. Jene basieren auf sogenannten Aktionsmustern, welche typische Arbeitsblöcke darstellen. Neben der Definition dieser Aktionsmuster zeigen wir eine Methode zur Identifikation dieser Muster auf. Mittels Techniken der Assoziationsanalyse können die Muster automatisch aus einer Sammlung von Prozessmodellen extrahiert werden. Die Anwendbarkeit unseres Ansatzes wird durch eine Fallstudie auf Basis des SAP Referenzmodells illustriert.
T3  - Technische Berichte des Hasso-Plattner-Instituts für Digital Engineering an der Universität Potsdam - 30 
Y1  - 2009
U6  - http://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:kobv:517-opus-33586
SN  - 978-3-86956-009-0
PB  - Universitätsverlag Potsdam
CY  - Potsdam
ER  - 
TY  - JOUR
A1  - Weske, Mathias
A1  - van der Aalst, Wil M. P.
A1  - Verbeek, H. M. W.
T1  - Advances in business process management
Y1  - 2004
SN  - 0169-023X
ER  - 
TY  - JOUR
A1  - Andree, Kerstin
A1  - Ihde, Sven
A1  - Weske, Mathias
A1  - Pufahl, Luise
T1  - An exception handling framework for case management
JF  - Software and Systems Modeling
N2  - In order to achieve their business goals, organizations heavily rely on the operational excellence of their business processes. In traditional scenarios, business processes are usually well-structured, clearly specifying when and how certain tasks have to be executed. Flexible and knowledge-intensive processes are gathering momentum, where a knowledge worker drives the execution of a process case and determines the exact process path at runtime. In the case of an exception, the knowledge worker decides on an appropriate handling. While there is initial work on exception handling in well-structured business processes, exceptions in case management have not been sufficiently researched. This paper proposes an exception handling framework for stage-oriented case management languages, namely Guard Stage Milestone Model, Case Management Model and Notation, and Fragment-based Case Management. The effectiveness of the framework is evaluated with two real-world use cases showing that it covers all relevant exceptions and proposed handling strategies.
KW  - Exception handling
KW  - Knowledge-intensive processes
KW  - Flexible processes;
KW  - Case management
Y1  - 2022
U6  - https://doi.org/10.1007/s10270-022-00993-3
SN  - 1619-1366
SN  - 1619-1374
VL  - 21
IS  - 3
SP  - 939
EP  - 962
PB  - Springer
CY  - Heidelberg
ER  - 
TY  - JOUR
A1  - Meyer, Andreas
A1  - Pufahl, Luise
A1  - Batoulis, Kimon
A1  - Fahland, Dirk
A1  - Weske, Mathias
T1  - Automating data exchange in process choreographies
JF  - Information systems
N2  - Communication between organizations is formalized as process choreographies in daily business. While the correct ordering of exchanged messages can be modeled and enacted with current choreography techniques, no approach exists to describe and automate the exchange of data between processes in a choreography using messages. This paper describes an entirely model-driven approach for BPMN introducing a few concepts that suffice to model data retrieval, data transformation, message exchange, and correlation four aspects of data exchange. For automation, this work utilizes a recent concept to enact data dependencies in internal processes. We present a modeling guideline to derive local process models from a given choreography; their operational semantics allows to correctly enact the entire choreography from the derived models only including the exchange of data. Targeting on successful interactions, we discuss means to ensure correct process choreography modeling. Finally, we implemented our approach by extending the camunda BPM platform with our approach and show its feasibility by realizing all service interaction patterns using only model-based concepts. (C) 2015 Elsevier Ltd. All rights reserved.
KW  - Process modeling
KW  - Data modeling
KW  - Process choreographies
KW  - Data exchange
KW  - BPMN
KW  - SQL
Y1  - 2015
U6  - https://doi.org/10.1016/j.is.2015.03.008
SN  - 0306-4379
SN  - 1873-6076
VL  - 53
SP  - 296
EP  - 329
PB  - Elsevier
CY  - Oxford
ER  - 
TY  - JOUR
A1  - Pufahl, Luise
A1  - Weske, Mathias
T1  - Batch activity: enhancing business process modeling and enactment with batch processing
JF  - Computing
N2  - Organizations strive for efficiency in their business processes by process improvement and automation. Business process management (BPM) supports these efforts by capturing business processes in process models serving as blueprint for a number of process instances. In BPM, process instances are typically considered running independently of each other. However, batch processing-the collectively execution of several instances at specific process activities-is a common phenomenon in operational processes to reduce cost or time. Currently, batch processing is organized manually or hard-coded in software. For allowing stakeholders to explicitly represent their batch configurations in process models and their automatic execution, this paper provides a concept for batch activities and describes the corresponding execution semantics. The batch activity concept is evaluated in a two-step approach: a prototypical implementation in an existing BPM System proves its feasibility. Additionally, batch activities are applied to different use cases in a simulated environment. Its application implies cost-savings when a suitable batch configuration is selected. The batch activity concept contributes to practice by allowing the specification of batch work in process models and their automatic execution, and to research by extending the existing process modeling concepts.
KW  - Batch activity
KW  - Batch processing
KW  - Business process models
KW  - Process Enactment
KW  - Colored Petri Net
Y1  - 2019
U6  - https://doi.org/10.1007/s00607-019-00717-4
SN  - 0010-485X
SN  - 1436-5057
VL  - 101
IS  - 12
SP  - 1909
EP  - 1933
PB  - Springer
CY  - Wien
ER  - 
TY  - BOOK
A1  - Pufahl, Luise
A1  - Meyer, Andreas
A1  - Weske, Mathias
T1  - Batch regions : process instance synchronization based on data
N2  - Business process automation improves organizations’ efficiency to perform work. In existing business process management systems, process instances run independently from each other. However, synchronizing instances carrying similar characteristics, i.e., sharing the same data, can reduce process execution costs. For example, if an online retailer receives two orders from one customer, there is a chance that they can be packed and shipped together to save shipment costs. In this paper, we use concepts from the database domain and introduce data views to business processes to identify instances which can be synchronized. Based on data views, we introduce the concept of batch regions for a context-aware instance synchronization over a set of connected activities. We also evaluate the concepts introduced in this paper with a case study comparing costs for normal and batch processing.
N2  - Die Automatisierung von Geschäftsprozessen unterstützt Unternehmen, die Ausführung ihrer Prozesse effizienter zu gestalten. In existierenden Business Process Management Systemen, werden die Instanzen eines Prozesses völlig unabhängig voneinander ausgeführt. Jedoch kann das Synchronisieren von Instanzen mit ähnlichen Charakteristiken wie z.B. den gleichen Daten zu reduzierten Ausführungskosten führen. Zum Beispiel, wenn ein Onlinehändler zwei Bestellungen vom selben Kunden mit der gleichen Lieferanschrift erhält, können diese zusammen verpackt und versendet werden, um Versandkosten zu sparen. In diesem Papier verwenden wir Konzepte aus dem Datenbankbereich und führen Datensichten für Geschäftsprozesse ein, um Instanzen zu identifizieren, welche synchronisiert werden können. Auf Grundlage der Datensichten führen wir das Konzept der Batch-Regionen ein. Eine Batch-Region ermöglicht eine kontext-bewusste Instanzen-Synchronisierung über mehrere verbundene Aktivitäten. Das eingeführte Konzept wird mit einer Fallstudie evaluiert, bei der ein Kostenvergleich zwischen der normalen Prozessausführung und der Batchverarbeitung durchgeführt wird.
T3  - Technische Berichte des Hasso-Plattner-Instituts für Digital Engineering an der Universität Potsdam - 86 
KW  - BPM
KW  - Batchverarbeitung
KW  - Gruppierung von Prozessinstanzen
KW  - Datensicht
KW  - BPM
KW  - batch processing
KW  - process instance grouping
KW  - data view
Y1  - 2013
U6  - http://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:kobv:517-opus-69081
SN  - 978-3-86956-280-3
PB  - Universitätsverlag Potsdam
CY  - Potsdam
ER  - 
TY  - JOUR
A1  - Weidlich, Matthias
A1  - Dijkman, Remco
A1  - Weske, Mathias
T1  - Behaviour equivalence and compatibility of business process models with complex correspondences
JF  - The computer journal : a publication of the British Computer Society
N2  - Once multiple models of a business process are created for different purposes or to capture different variants, verification of behaviour equivalence or compatibility is needed. Equivalence verification ensures that two business process models specify the same behaviour. Since different process models are likely to differ with respect to their assumed level of abstraction and the actions that they take into account, equivalence notions have to cope with correspondences between sets of actions and actions that exist in one process but not in the other. In this paper, we present notions of equivalence and compatibility that can handle these problems. In essence, we present a notion of equivalence that works on correspondences between sets of actions rather than single actions. We then integrate our equivalence notion with work on behaviour inheritance that copes with actions that exist in one process but not in the other, leading to notions of behaviour compatibility. Compatibility notions verify that two models have the same behaviour with respect to the actions that they have in common. As such, our contribution is a collection of behaviour equivalence and compatibility notions that are applicable in more general settings than existing ones.
KW  - behaviour equivalence
KW  - behaviour compatibility
KW  - model verification
KW  - behavioural models
Y1  - 2012
U6  - https://doi.org/10.1093/comjnl/bxs014
SN  - 0010-4620
SN  - 1460-2067
VL  - 55
IS  - 11
SP  - 1398
EP  - 1418
PB  - Oxford Univ. Press
CY  - Oxford
ER  - 
TY  - BOOK
A1  - Kunze, Matthias
A1  - Weske, Mathias
T1  - Behavioural Models
BT  - From Modelling Finite Automata to Analysing Business Processes
N2  - This textbook introduces the basis for modelling and analysing discrete dynamic systems, such as computer programmes, soft- and hardware systems, and business processes. The underlying concepts are introduced and concrete modelling techniques are described, such as finite automata, state machines, and Petri nets. The concepts are related to concrete application scenarios, among which business processes play a prominent role. 

The book consists of three parts, the first of which addresses the foundations of behavioural modelling. After a general introduction to modelling, it introduces transition systems as a basic formalism for representing the behaviour of discrete dynamic systems. This section also discusses causality, a fundamental concept for modelling and reasoning about behaviour. In turn, Part II forms the heart of the book and is devoted to models of behaviour. It details both sequential and concurrent systems and introduces finite automata, state machines and several different types of Petri nets. One chapter is especially devoted to business process models, workflow patterns and BPMN, the industry standard for modelling business processes. Lastly, Part III investigates how the behaviour of systems can be analysed. To this end, it introduces readers to the concept of state spaces. Further chapters cover the comparison of behaviour and the formal analysis and verification of behavioural models.

The book was written for students of computer science and software engineering, as well as for programmers and system analysts interested in the behaviour of the systems they work on. It takes readers on a journey from the fundamentals of behavioural modelling to advanced techniques for modelling and analysing sequential and concurrent systems, and thus provides them a deep understanding of the concepts and techniques introduced and how they can be applied to concrete application scenarios.
Y1  - 2016
SN  - 978-3-319-44958-6
PB  - Springer
CY  - Cham
ER  - 
TY  - JOUR
A1  - Mendling, Jan
A1  - Weber, Ingo
A1  - van der Aalst, Wil
A1  - Brocke, Jan Vom
A1  - Cabanillas, Cristina
A1  - Daniel, Florian
A1  - Debois, Soren
A1  - Di Ciccio, Claudio
A1  - Dumas, Marlon
A1  - Dustdar, Schahram
A1  - Gal, Avigdor
A1  - Garcia-Banuelos, Luciano
A1  - Governatori, Guido
A1  - Hull, Richard
A1  - La Rosa, Marcello
A1  - Leopold, Henrik
A1  - Leymann, Frank
A1  - Recker, Jan
A1  - Reichert, Manfred
A1  - Reijers, Hajo A.
A1  - Rinderle-Ma, Stefanie
A1  - Solti, Andreas
A1  - Rosemann, Michael
A1  - Schulte, Stefan
A1  - Singh, Munindar P.
A1  - Slaats, Tijs
A1  - Staples, Mark
A1  - Weber, Barbara
A1  - Weidlich, Matthias
A1  - Weske, Mathias
A1  - Xu, Xiwei
A1  - Zhu, Liming
T1  - Blockchains for Business Process Management
BT  - Challenges and Opportunities
JF  - ACM Transactions on Management Information Systems
N2  - Blockchain technology offers a sizable promise to rethink the way interorganizational business processes are managed because of its potential to realize execution without a central party serving as a single point of trust (and failure). To stimulate research on this promise and the limits thereof, in this article, we outline the challenges and opportunities of blockchain for business process management (BPM). We first reflect how blockchains could be used in the context of the established BPM lifecycle and second how they might become relevant beyond. We conclude our discourse with a summary of seven research directions for investigating the application of blockchain technology in the context of BPM.
KW  - Blockchain
KW  - business process management
KW  - research challenges
Y1  - 2018
U6  - https://doi.org/10.1145/3183367
SN  - 2158-656X
SN  - 2158-6578
VL  - 9
IS  - 1
SP  - 1
EP  - 16
PB  - Association for Computing Machinery
CY  - New York
ER  - 
TY  - JOUR
A1  - Baier, Thomas
A1  - Mendling, Jan
A1  - Weske, Mathias
T1  - Bridging abstraction layers in process mining
JF  - Information systems
N2  - While the maturity of process mining algorithms increases and more process mining tools enter the market, process mining projects still face the problem of different levels of abstraction when comparing events with modeled business activities. Current approaches for event log abstraction try to abstract from the events in an automated way that does not capture the required domain knowledge to fit business activities. This can lead to misinterpretation of discovered process models. We developed an approach that aims to abstract an event log to the same abstraction level that is needed by the business. We use domain knowledge extracted from existing process documentation to semi-automatically match events and activities. Our abstraction approach is able to deal with n:m relations between events and activities and also supports concurrency. We evaluated our approach in two case studies with a German IT outsourcing company. (C) 2014 Elsevier Ltd. All rights reserved.
KW  - Process mining
KW  - Abstraction
KW  - Event mapping
Y1  - 2014
U6  - https://doi.org/10.1016/j.is.2014.04.004
SN  - 0306-4379
SN  - 1873-6076
VL  - 46
SP  - 123
EP  - 139
PB  - Elsevier
CY  - Oxford
ER  - 
TY  - JOUR
A1  - Luebbe, Alexander
A1  - Weske, Mathias
T1  - Bringing design thinking to business process modeling
Y1  - 2011
SN  - 978-3-642-13756-3
ER  - 
TY  - BOOK
A1  - Eid-Sabbagh, Rami-Habib
A1  - Hewelt, Marcin
A1  - Weske, Mathias
T1  - Business process architectures with multiplicities : transformation and correctness
N2  - Business processes are instrumental to manage work in organisations. To study the interdependencies between business processes, Business Process Architectures have been introduced. These express trigger and message ow relations between business processes. When we investigate real world Business Process Architectures, we find complex interdependencies, involving multiple process instances. These aspects have not been studied in detail so far, especially concerning correctness properties. In this paper, we propose a modular transformation of BPAs to open nets for the analysis of behavior involving multiple business processes with multiplicities. For this purpose we introduce intermediary nets to portray semantics of multiplicity specifications. We evaluate our approach on a use case from the public sector.
T3  - Technische Berichte des Hasso-Plattner-Instituts für Digital Engineering an der Universität Potsdam - 77 
Y1  - 2013
U6  - http://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:kobv:517-opus-66780
SN  - 978-3-86956-257-5
PB  - Universitätsverlag Potsdam
CY  - Potsdam
ER  - 
TY  - JOUR
A1  - Pernici, Barbara
A1  - Weske, Mathias
T1  - Business process management
Y1  - 2006
SN  - 0169-023X
ER  - 
TY  - BOOK
A1  - Weske, Mathias
T1  - Business Process Management : Concepts, Languages, Architectures
Y1  - 2007
SN  - 978-3-540-73521-2
U6  - https://doi.org/10.1007/978-3-540-73522-9
PB  - Springer-Verlag Berlin Heidelberg
CY  - Berlin, Heidelberg
ER  - 
TY  - BOOK
A1  - Smirnov, Sergey
A1  - Reijers, Hajo A.
A1  - Nugteren, Thijs
A1  - Weske, Mathias
T1  - Business process model abstraction : theory and practice
N2  - Business process management aims at capturing, understanding, and improving work in organizations. The central artifacts are process models, which serve different purposes. Detailed process models are used to analyze concrete working procedures, while high-level models show, for instance, handovers between departments. To provide different views on process models, business process model abstraction has emerged. While several approaches have been proposed, a number of abstraction use case that are both relevant for industry and scientifically challenging are yet to be addressed. In this paper we systematically develop, classify, and consolidate different use cases for business process model abstraction. The reported work is based on a study with BPM users in the health insurance sector and validated with a BPM consultancy company and a large BPM vendor. The identified fifteen abstraction use cases reflect the industry demand. The related work on business process model abstraction is evaluated against the use cases, which leads to a research agenda.
T3  - Technische Berichte des Hasso-Plattner-Instituts für Digital Engineering an der Universität Potsdam - 35 
Y1  - 2010
U6  - http://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:kobv:517-opus-41782
SN  - 978-3-86956-054-0
PB  - Universitätsverlag Potsdam
CY  - Potsdam
ER  - 
TY  - JOUR
A1  - Weidlich, Matthias
A1  - Polyvyanyy, Artem
A1  - Mendling, Jan
A1  - Weske, Mathias
T1  - Causal behavioural profiles - efficient computation, applications, and evaluation
JF  - Fundamenta informaticae
N2  - Analysis of behavioural consistency is an important aspect of software engineering. In process and service management, consistency verification of behavioural models has manifold applications. For instance, a business process model used as system specification and a corresponding workflow model used as implementation have to be consistent. Another example would be the analysis to what degree a process log of executed business operations is consistent with the corresponding normative process model. Typically, existing notions of behaviour equivalence, such as bisimulation and trace equivalence, are applied as consistency notions. Still, these notions are exponential in computation and yield a Boolean result. In many cases, however, a quantification of behavioural deviation is needed along with concepts to isolate the source of deviation.
 In this article, we propose causal behavioural profiles as the basis for a consistency notion. These profiles capture essential behavioural information, such as order, exclusiveness, and causality between pairs of activities of a process model. Consistency based on these profiles is weaker than trace equivalence, but can be computed efficiently for a broad class of models. In this article, we introduce techniques for the computation of causal behavioural profiles using structural decomposition techniques for sound free-choice workflow systems if unstructured net fragments are acyclic or can be traced back to S-or T-nets. We also elaborate on the findings of applying our technique to three industry model collections.
KW  - Causal Behavioural Profiles
KW  - Formal Methods
KW  - Behavioural Abstraction
KW  - Structural Decomposition
KW  - Exclusiveness
KW  - Concurrency
KW  - Order Relations
KW  - Causality
KW  - Optionality
Y1  - 2011
U6  - https://doi.org/10.3233/FI-2011-614
SN  - 0169-2968
VL  - 113
IS  - 3-4
SP  - 399
EP  - 435
PB  - IOS Press
CY  - Amsterdam
ER  - 
TY  - GEN
A1  - Combi, Carlo
A1  - Oliboni, Barbara
A1  - Weske, Mathias
A1  - Zerbato, Francesca
ED  - Trujillo, JC Davis
T1  - Conceptual modeling of processes and data
BT  - Connecting different perspectives
T2  - Conceptual Modeling, ER 2018
N2  - Business processes constantly generate, manipulate, and consume data that are managed by organizational databases. Despite being central to process modeling and execution, the link between processes and data is often handled by developers when the process is implemented, thus leaving the connection unexplored during the conceptual design. In this paper, we introduce, formalize, and evaluate a novel conceptual view that bridges the gap between process and data models, and show some kinds of interesting insights that can be derived from this novel proposal.
Y1  - 2018
SN  - 978-3-030-00847-5
SN  - 978-3-030-00846-8
U6  - https://doi.org/10.1007/978-3-030-00847-5_18
SN  - 0302-9743
SN  - 1611-3349
VL  - 11157
SP  - 236
EP  - 250
PB  - Springer
CY  - Cham
ER  - 
TY  - JOUR
A1  - Polyvyanyy, Artem
A1  - Weidlich, Matthias
A1  - Weske, Mathias
T1  - Connectivity of workflow nets the foundations of stepwise verification
JF  - Acta informatica
N2  - Behavioral models capture operational principles of real-world or designed systems. Formally, each behavioral model defines the state space of a system, i.e., its states and the principles of state transitions. Such a model is the basis for analysis of the system's properties. In practice, state spaces of systems are immense, which results in huge computational complexity for their analysis. Behavioral models are typically described as executable graphs, whose execution semantics encodes a state space. The structure theory of behavioral models studies the relations between the structure of a model and the properties of its state space. In this article, we use the connectivity property of graphs to achieve an efficient and extensive discovery of the compositional structure of behavioral models; behavioral models get stepwise decomposed into components with clear structural characteristics and inter-component relations. At each decomposition step, the discovered compositional structure of a model is used for reasoning on properties of the whole state space of the system. The approach is exemplified by means of a concrete behavioral model and verification criterion. That is, we analyze workflow nets, a well-established tool for modeling behavior of distributed systems, with respect to the soundness property, a basic correctness property of workflow nets. Stepwise verification allows the detection of violations of the soundness property by inspecting small portions of a model, thereby considerably reducing the amount of work to be done to perform soundness checks. Besides formal results, we also report on findings from applying our approach to an industry model collection.
Y1  - 2011
U6  - https://doi.org/10.1007/s00236-011-0137-8
SN  - 0001-5903
VL  - 48
IS  - 4
SP  - 213
EP  - 242
PB  - Springer
CY  - New York
ER  -