Workshop SBC'2000

Program

Tuesday, May 2nd:

12:00

Arrival

12:15 - 13:00

Lunch

13:00 - 13:30

Introduction

13:30 - 14:30

Parameterisation and Modularity in Coloured Petri Nets

Thomas Mailund
Abstract: A modular approach to modelling makes larger systems easier to handle, and a large degree of reuse significantly decreases the development time and reduces maintenance cost. But it is often the case that large CPN models contain a number of similar constructions, where only a few details differ. Modularisation alone does not allow for much reuse in such circumstances. However, by parameterising the parts that differs between the modules we can construct a single module that describes the whole family of modules. We will examine different kinds of parameterisation of CPN modules, their use, and (if time permits) describe how they can be formally defined.
 

14:30 - 15:00

Coffee Break

15:00 - 16:00

Communication and Modular Coloured Petri Nets

Bo Lindstrøm
Abstract: The talk will focus on how to integrate communication and modular Coloured Petri Nets (CP-nets). An essential property of modules is that modules must be able to communicate. Thus, by introducing communication between modules it becomes possible to combine modules into larger modules. Different ways of communicating between modules exists. We propose four different ways: place-to-place, place-to-transition, transition-to-place, and transition-to-transition. Place-to-place communication is similar to place fusion. Place-to-transition and transition-to-place communication are similar to ordinary arcs between places and transitions. Transition-to-transition communication corresponds to synchronising transitions. Finally, we will also briefly discuss some of the advantages of using communication and modular CP-nets when developing distributed systems.
 

16:00 - 16:30

Coffee

16:30 - 17:30

Reference Nets

Olaf Kummer
Abstract: Based on Valk's ideas of using nets as token objects, it is investigated whether references to nets can be considered as tokens in a way that is theoretically well-founded, easy to use, and efficiently executable. This leads to the development of reference nets.
Some additions to coloured Petri nets are required to exploit the full potential of this concept. Dynamically created net instances allow us to go beyond the expressiveness of ordinary nets. In order to coordinate the execution of multiple net instances, synchronous channel are added. Automatic garbage collection of net instances replaces an error-prone explicit deletion. The tight integration of a high-level object-oriented inscription language allows the use of adequate modelling tools for different part of the system. Mathematically, the theory is founded on graph rewriting systems according to the single-pushout approach. Natural restrictions are applied, removing those effects of graph rewriting that would be alien to Petri net theory. Algorithms for the execution of reference nets have been invented and implemented in the tool Renew. The architecture of the simulator is generic and can be adapted to various net formalisms.
 

17:30 - 18:00

Discussion

Wednesday, May 3rd:

9:30 - 10:30

Design and Implementation of Communication in Design/CPN

Francois Vernet and Stefan Nimsgern
Abstract: This talk will describe design and implementation of different ways of communicating between running simulations of CPN models and remote applications. The work is a further development of the approach described in 'A framework for interacting Design/CPN - and Java processes' by Kummer, Moldt, and Wienberg. Different approaches to the design of a connection between Design/CPN and remote applications are described. This includes communication between Design/CPN simulators which leads to distributed simulations. Controlling a Design/CPN simulation from a Java applet running in a Web browser will also be discussed.
 

10:30 - 11:00

Coffee Break

11:00 - 12:00

Performance Analysis using Coloured Petri Nets

Lisa Wells
Abstract: Coloured Petri Nets (CP-nets) have proved to be very useful for modelling and analysing the behaviour of very diverse types of real-world systems. Until now, CP-nets have been used primarily for analysing the logical correctness of a system, however, CP-nets can also be used to analyse the performance of a system. We are currently focusing on simulation-based performance analysis. This talk will discuss our work concerning providing better support for running batches of simulations, generating reliable statistical output, and performing sensitivity analysis.
 

12:00 - 13:30

Lunch

13:30 - 14:30

Efficient Generation of Condensed State Spaces

Louise Lorentsen
Abstract: Many concurrent systems posses a certain degree of symmetry, e.g., they are composed of identical components whose identities are interchangeable seen from a verification point of view. The Design/CPN tool supports state spaces with permutation symmetries based on user-supplied symmetry specifications. This means that the user of the tool is required to provide the permutation symmetries, and the tool then uses these as a basis for the reduction. The idea of state spaces with permutation symmetries is to construct equivalence classes of markings which are symmetric in the sense that they can be obtained from each other by one of the permutation symmetries. Instead of representing all markings it suffices to store a representative for each equivalence class containing a reachable marking. In this way a condensed state space is obtained which is typically orders of magnitude smaller than the full state space. The practical applicability of condensed state spaces is highly dependent on how effective we can determine whether two markings are symmetric or not. In this talk we will present and discuss strategies and techniques for efficient generation of condensed state spaces.
 

14:30 - 15:00

Coffee Break

15:00 - 16:00

Modeling Framework for (Intelligent) Agents

Heiko Rölke
Abstract: Modelling languages like UML have gained a great success in the last years. UML is now standardized and seems to achieve its intention to be the one and only notation for object oriented software engineering. There are some new efforts to develop similiar languages (and, built up on languages and notations, tools and frameworks) for agents. Until now, these efforts do not have any outcome. Every scientist in the field of agent oriented software development (and related areas) invents agents from scratch.
My work is on how Petri nets can be brought into this field. Especially provably correct behaviour or provable properties are of interest, because agent communication languages have often been supported with modal or temporal logics. Moreover, Petri nets have the advantage to be understandable without giving up a clear semantics (as it is often done with diagrammatical figures in UML). A Petri net agent framework has therefore the advantage to be executable and intuitively understandable at the same time. Nevertheless many problems like the modeling of intelligence remain unresolved up to now.
 

16:00 - 16:30

Coffee Break

16:30 - 17:30

Compositionality for Agent-oriented Petri Nets

Michael Köhler
Abstract: The main topic of my current work concerns the formal aspects of composionality. Compositionality covers many related areas in computer science, namely:
(a) Composition of reference nets, a special dialect of Petri nets;
(b) Composition of protocols, controlling the actions of agents;
(c) Composition of safeness and liveness proofs hand-in-hand with the composition of Petri nets, in contrast to global proof style.
Current attention is paid to the static composition of finite protocol components for agent communications in our Petri net architecture for multi agent systems. For the near future this formalism is to be extended for run-time composition of protocols, so we are able to investigate and formalize the modification and creation of agent behavior.
 

17:30 - 18:00

Discussion

Thursday, May 4th:

9:30 - 10:30

Linear Logic for Object Petri Nets

Berndt Farwer
Abstract: Linear Logic has a close resemblance to Petri nets in that it has connectives that can handle resources in the same manner as ordinary Petri nets do. In a simplistic attempt to characterize Linear Logic, it can be described as allowing arguments over multisets, while classical logic arguments range over sets.
We try to mingle the two formalisms, defining Linear Logic Petri nets as a new formalism, allowing the study of different object Petri net formalisms in a uniform framework. Emphasis is given to the possibility of employing Linear Logic for specifying dynamic modifications of object net structures.
 

10:30 - 11:00

Coffee Break

11:00 - 12:00

Petri nets and mobility

Ivana Trickovic
Abstract:  Mobility encompasses both physical and logical computing entities that move, where movements can happen within local area networks or wide area networks, such as the Internet. In addition, the Internet appears as an environment where distributed programs may be deployed and run. This motivates creating programming as well as modelling languages that would  provide a framework for programming and modelling mobile computations and mobile computing.
One approach, which is my area of research, would be to study mobility in the framework of Petri net theory, and specially in the  framework of high-level Petri nets formalisms that incorporate the paradigm of nets in nets, such as Object Petri nets. This could  be a ground for defining modelling language for modelling mobile computation and mobile computing.
The concepts that are of interests are: locality, protection mechanisms, concurrency, and communication mechanisms.
 

12:00 - 12:30

Discussion

12:30

Lunch