TY  - JOUR
A1  - Polyvyanyy, Artem
A1  - Weidlich, Matthias
A1  - Weske, Mathias
T1  - Connectivity of workflow nets the foundations of stepwise verification
T2  - 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
UR  - https://publishup.uni-potsdam.de/frontdoor/index/index/docId/36748
SN  - 0001-5903
VL  - 48
IS  - 4
SP  - 213
EP  - 242
PB  - Springer
CY  - New York
ER  -