Petri Nets 2012 & ACSD 2012
Hamburg, Germany, June 25–29, 2012
Petri nets are employed as a multifunctional integrative framework for biomodel engineering. We describe the general concept of a modular modelling approach that consideres the functional coupling of components of genome, transcriptome, and proteome with complex cellular phenotypes. For this purpose, the effects of genes and their mutated alleles on downstream components are modeled by composable, metadata-containing Petri net models organized in a database with version control, accessible through a web interface. Gene modules are coupled to protein modules through mRNA modules by specific interfaces designed for the automatic, database-assisted composition. Automatically assembled executable models may then consider cell type-specific gene expression patterns and take the resulting protein concentrations into account. With a sufficient number of protein modules in the database, the composed Petri nets can predict complex effects of gene mutations or uncover complex genotype/phenotype relationships. In this context, forward and reverse engineered modules are fully compatible.
I challenge the traditional choice of topics and the usual style of presentation for introductory courses on Petri nets. For such a course I suggest a number of aspects that usually are not considered fundamental. This includes faithful models, a slight revision of formalisms and terminology, specific techniques to increase the expressive power of Petri net models, aspects derived from distributed runs, and particular mathematics to specify and verify properties of Petri net models.
by Karsten Wolf
Academic tools are increasingly important outcomes of academic research. They can be used for proving applicability of theoretical results, for linking theory and practice, and they can serve as well assessable deliverables of research projects. The Petri net group in Rostock has a long tradition in developing Petri net related academic tools. Today, about 20 tools are contributed, developed by teams working in different cities and countries. Our tools have been integrated into several general verification frameworks.
In the talk, we would like to give an overview on tool development in Rostock and discuss our general tool philosophy, including interoperability and integration. We will also share our experience concerning general issues in academic tool development as opposed to industrial software engineering. Our examples will include recent tools such as the Anica tool that checks an information flow security property on Petri nets.
The results of the research group forMAlNET (funded by the German Research Council 2006-2012) on reconfigurable Petri nets are presented in this talk. We introduce a family of modeling techniques consisting of Petri nets together with a set of rules. For reconfigurable Petri nets not only the follower marking can be computed but also the structure can be changed by rule application to obtain a new net that is more appropriate with respect to some requirements of the environment. Moreover, these activities can be interleaved. For rule-based modification of Petri nets we use the framework of net transformations that is inspired by graph transformation systems. The basic idea behind net transformation is the stepwise modification of Petri nets by given rules. The rules present a rewriting of nets where the left-hand side is replaced by the right-hand side.
Motivation for this family of formal modeling techniques is the observation that in increasingly many application areas the underlying system has to be dynamic in a structural sense. Complex coordination and structural adaptation at run-time (e.g. mobile ad-hoc networks, communication spaces, ubiquitous computing) are main features that need to be modeled adequately. The distinction between the net behavior and the dynamic change of its net structure is the characteristic feature that makes reconfigurable Petri nets so suitable for systems with dynamic structures.
In this talk we first motivate the use of reconfigurable Petri nets and present their basic ideas. The concepts are discussed and are then given mathematically. We employ the notion of high-level replacement systems extensively to obtain rules and transformations of place/transition nets. These notions are then exem- plified in a case study modeling scenarios of the Living Place Hamburg. Living Place Hamburg can be considered as a system of ubiquitous computing and am- bient intelligence. Scenarios of the Living Place are modeled using reconfigurable place/transition nets providing a formal model of the internal system behavior of this system, so that this model helps us to improve our understanding of the modeled system. Subsequently we extend the theory to algebraic high-level nets, this employs again high-level replacement systems with nested application conditions as well as a individual token approach. These new concepts are illus- trated and discussed in the case study Skype at length. The analysis of Skype as a concrete and typical existing Communication Platform is an example for a mod- eling methodology for Communication Platforms using an integrated modeling approach based on algebraic higher order nets.
The talk is concluded with a discussion of further results.
