caa a22 4500 445869704 CHVBK 20180317145508.0 cr unu---uuuuu 170323e20110701xx s 000 0 eng 10.1007/s00236-011-0137-8 doi (NATIONALLICENCE)springer-10.1007/s00236-011-0137-8 Connectivity of workflow nets: the foundations of stepwise verification [Elektronische Daten] [Artem Polyvyanyy, Matthias Weidlich, Mathias Weske] 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. Springer-Verlag, 2011 Polyvyanyy Artem Business Process Technology Group, Hasso Plattner Institute at the University of Potsdam, Prof.-Dr.-Helmert-Str. 2-3, 14482, Potsdam, Germany aut Weidlich Matthias Business Process Technology Group, Hasso Plattner Institute at the University of Potsdam, Prof.-Dr.-Helmert-Str. 2-3, 14482, Potsdam, Germany aut Weske Mathias Business Process Technology Group, Hasso Plattner Institute at the University of Potsdam, Prof.-Dr.-Helmert-Str. 2-3, 14482, Potsdam, Germany aut Acta Informatica Springer-Verlag 48/4(2011-07-01), 213-242 0001-5903 48:4<213 2011 48 236 https://doi.org/10.1007/s00236-011-0137-8 text/html Onlinezugriff via DOI 1 research-article jats NATIONALLICENCE 856 40 https://doi.org/10.1007/s00236-011-0137-8 text/html Onlinezugriff via DOI NATIONALLICENCE 700 1- Polyvyanyy Artem Business Process Technology Group, Hasso Plattner Institute at the University of Potsdam, Prof.-Dr.-Helmert-Str. 2-3, 14482, Potsdam, Germany aut NATIONALLICENCE 700 1- Weidlich Matthias Business Process Technology Group, Hasso Plattner Institute at the University of Potsdam, Prof.-Dr.-Helmert-Str. 2-3, 14482, Potsdam, Germany aut NATIONALLICENCE 700 1- Weske Mathias Business Process Technology Group, Hasso Plattner Institute at the University of Potsdam, Prof.-Dr.-Helmert-Str. 2-3, 14482, Potsdam, Germany aut NATIONALLICENCE 773 0- Acta Informatica Springer-Verlag 48/4(2011-07-01), 213-242 0001-5903 48:4<213 2011 48 236 Metadata rights reserved Springer special CC-BY-NC licence nationallicence BK010053 XK010053 XK010000 NATIONALLICENCE NATIONALLICENCE NL-springer