Affiliations: Department of Mathematics and Computer Science,
Eindhoven University of Technology, P.O. Box 513, 5600 MB Eindhoven, The
Netherlands. E-mail:
{k.m.v.hee,o.i.oanea,a.serebrenik,n.sidorova,m.voorhoeve}@tue.nl | Program Systems Institute of Russian Academy of
Science, Pereslavl-Zalessky, 152020, Russia. E-mail:
[email protected]
Abstract: In this paper we consider adaptive workflow nets, a class of nested
nets that allows more comfort and expressive power for modeling adaptability
and exception handling in workflow nets. We define two important behavioural
properties of adaptive workflow nets: soundness and circumspectness. Soundness
means that a proper final marking (state) can be reached from any marking which
is reachable from the initial marking, and no garbage will be left.
Circumspectness means that the upper layer is always ready to handle any
exception that can happen in a lower layer. We define a finite state
abstraction for adaptive workflow nets and show that soundness and
circumspectness can be verified on this abstraction.
