Technische Universitat Munchen
In the world of service oriented architectures, one deals with networks of cooperating components. A component offers services; to deliver a service it possibly needs services of other components, thus forming a service tree. This tree is built dynamically and not known before-hand. It is hard to verify the behavior of a service tree by using standard verification techniques, because these techniques typically assume a static flattened model. In this paper the authors model a component by an open petri net.