LAM’12 Papers and Talks

In Uncategorized on June 5, 2012 at 8:43 am

LAM’12 will be held on 25 June 2012 at the University of Hamburg. The following contributed papers will be presented.

  • Artur Meski, Wojciech Penczek and Maciej Szreter: BDD-based Bounded Model Checking for LTLK over Two Variants of Interpreted Systems
  • José Martín Castro-Manzano: Modelling Intentional Reasoning with Defeasible and Temporal Logic
  • Frank Heitmann and Michael Köhler-Bußmeier: A Mobility Logic for Object Net Systems

An invited talk will be given by Julia Padberg:

Reconfigurable Petri Nets: Modeling and Analysis

The results of the research group for MAlNET (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 ob- tain 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 transfor- mation 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 dy- namic in a structural sense. Complex coordination and structural adaptation at run-time (e.g. mobile ad-hoc networks, communication spaces, ubiquitous com- puting) 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 sys- tems 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.


Leave a Reply

Fill in your details below or click an icon to log in: Logo

You are commenting using your account. Log Out /  Change )

Google+ photo

You are commenting using your Google+ account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )


Connecting to %s

%d bloggers like this: