Archive for June, 2012|Monthly archive page

LAM’12 Programme

In News on June 21, 2012 at 7:45 am

Logics, Agents, and Mobility

Chairs: Berndt Müller (Farwer) and Michael Köhler-Bußmeier

Monday, 25 June

09:00-Invited Talk (Room B-201 Informatics Campus)
Wolfgang Marwan Petri Nets – an Integrative Framework for Advanced Biomodel Engineering
10:15-Joint Session with PNSE (Room F-132 Informatics Campus)
Kees Van Hee, Natalia Sidorova and Jan Martijn Van Der Werf When Can We Trust a Third Party? – A Soundness Perspective
Agata Janowska, Wojciech Penczek, Agata Półrola and Andrzej Zbrzezny Using Integer Time Steps for Checking Branching Time Properties of Time Petri Nets
11:45-Session 2 (Room C-104 Informatics Campus)
José Martín Castro-Manzano Modelling Intentional Reasoning with Defeasible and Temporal Logic
13:45-Session 3 (Room C-104 Informatics Campus)
Artur Męski, Wojciech Penczek, Maciej Szreter BDD-based Bounded Model Checking for LTLK over Two Variants of Interpreted Systems
14:45-Joint Talk with PNSE (Room F-132 Informatics Campus)
Michael Westergaard, Dirk Fahland and Christian Stahl Grade/CPN: Semi-automatic Support for Teaching Petri Nets by Checking Many Petri Nets Against One Specification
15:20-Session 4 (RoomC-104 Informatics Campus)
Frank Heitmann, Michael Köhler-Bußmeier A Mobility Logic for Object Net Systems
16:45-Invited Talk (Room B-201 Informatics Campus)
Julia Padberg Reconfigurable Petri Nets: Modeling and Analysis


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.