Dat 5/SSE3: Semantics models and verification (Autumn 2004)

Lecturers: Jiri Srba and Hans Huttel

Students:     Tomas Jonasson
                    Michael Knudsen
                    Morten Kühnrich
                    Ragnhildur Oskarsdottir
                    Sigmar Stefansson
                    Jens Kristian Søgaard
                    Ye Tian

Location

             The course is held in E1-214.

Aims of the course

The aims of this course are:

  1. To provide a deeper understanding of advanced topics within the area
  2. To support the project work
  3. To teach students how to present and assess academic research papers

The topics of the course related directly to those of the student projects and are

All students are supposed to attend all sessions.

Contents

The course consists of a mixture of informal lectures given by the lecturers and presentations of selected research articles.

Lectures

The lecturers will give a few informal lectures.

Presentations

Each student will present two papers.:
The first presentation has as its primary aim to help ensure that the students have a thorough understanding and are able to demonstrate this. Consequently, the presentations will be relatively long (about 45 minutes) followed by a discussion focusing primarily on the contents of the presentation.
The second presentation has as its primary aim to ensure that the students can present a research paper in such a way that it gives a good overview of the main contributions of the paper.

All students and lecturers are supposed to comment on the presentations. 

For each presentation, another student will be asked in advance to be the main commentator. He/she must prepare a number of questions in advance, based on the article, and must give detailed comments concerning the actual presentation.

Practicals

There are no practicals associated with the sessions that involve presentations. The first three lectures may involve short practicals.


Course material


List of research papers

This list is not yet complete. Most papers will be available electronically.

Process calculi:

Petri Nets:


Plan  (details will appear as the course proceeds)


Session
Date and time Topic
Lecturer
Presentation
Literature
1
7.9 10.00-12.00
Introduction to Petri Nets.
Jiri
None

2
14.9 10.00-12.00
The pi-calculus
Hans
None
Parrow p. 3-25
3
21.9 10.15-12.00
The pi-calculus
Hans
None
Parrow p. 25-28, 39-42, 43-54
4
28.9  10.15-12.00
Reading, assessing and presenting scientific work (Slides from lecture)
Jiri


5
5.10 10.15-12.00
Reachability tree
Jiri
Tommi (Krishna, disc.)
James L.Peterson: Petri Net Theory and the modelling of systems, p. 87.88,91-106
6
13.10 10.15-12.00
Open bisimulation
Hans
Jens (Ragnhildur, disc.)
Davide Sangiorgi: A Theory of Bisimulation... (click for PDF version)
7
18.10 10.00-12.00
1-safe Petri nets
Jiri
Tian and Krishna (Tommi, disc.)
Allan Cheng, Javier Esparza, Jens Palsberg: Complexity Results for 1-safe Nets, p. 1-16
8
25.10
Types for mobile ambients Hans Morten (disc. Michael) Luca Cardelli, Andrew Gordon: Types for mobile ambients
9
2.11
On non-decidability of reachability for timed-arc Petri nets Jiri Simmi (disc. Tian) Valero Ruiz, Guartero Gomez and Frutos de Escrig. On non-decidability of reachability for timed-arc Petri nets
10
9.11
Better Quasi-Ordered Transition Systems Jiri Ragnhildur (disc. Jens) Parosh Aziz Abdulla and Aletta Nylen. Better Quasi-Ordered Transition Systems.
11
16.11
Proof Techniques for Cryptographic Processes Hans Mikael (disc. Morten) Michele Boreale, Rocco De Nicola and Rosario Pugliese. Proof Techniques for Cryptographic Processes (Postscript version)
12
23.11
Short presentations
  • Are Timed Automata Updatable?
Krishna (Ragga, disc.) P. Bouyer, C. Dufourd, E. Fleury, A. Petit Are Timed Automata Updatable? Morten Luca Cardelli, Andrew D. Gordon. Anytime, Anywhere - Modal Logics for Modal Ambients (PDF version)
13 30.11 Short presentations
  • General Decidability Theorems for Infinite-State Systems
  • Framed bisimulation
Simmi (Morten, discussion) P.A. Abdulla, K. Cernas, B. Jonsson. General Decidability Theorems for Infinite-State Systems Michael Martin Abadi and Andy Gordon. A Bisimulation Method for Cryptographic Protocols(PDF)
14 7.12 Short presentations.
  • Properties of Distributed Timed-Arc Petri Nets
Ragga (Jens, discussion) M. Nielsen, V. Sassone and J. Srba. Properties of Distributed Timed-Arc Petri Nets Jens Martin Abadi.Protection in Programming Language Translation(PDF)
15
14.12
Short presentations.
  • Modelling and Analysis of Production Systems Using a Petri Net Based Approach
  • Specification and Analysis of the MPEG-2 Video Encoder with Timed-Arc Petri Nets
  • Tian speaker (Simmi, discussion)
  • Tommi speaker (Michael, discussion)
Modelling and Analysis of Production Systems Using a Petri Net Based Approach by W.M.P. van der Aalst and Specification and Analysis of the MPEG-2 Video Encoder with Timed-Arc Petri Nets by V. Valero, F.L. Pelayo, F. Guartero and D. Cazorla

Additional resources