Top of this page
Skip navigation, go straight to the content

Seminar Formal Methods (2IF95) 2007

The seminar aims at showing and teaching how to do research. The seminar of the academic year 2007/2008 is headed by professor Jos Baeten while I provide assistence for this course. For questions you can always email us, stop by my room or prof. Baeten’s room if available.


27-08-2007: The seminar has started. Next week there will be no seminar! We will continue the seminar on September 11, 2007.

30-08-2007: The schedule has been updated. We will follow a bi-weekly schedule during the whole semester.

11-09-2007: Schedule update: scheduled the second parts of the presentations of 11-09-2007.

11-10-2007: Schedule update for the rest of block B. Updated the bibliography file.

08-11-2007: The schedule has been updated for block C! Also the research proposal and an updated bibliography file are available now.

04-12-2007: Final schedule update.


Block A

28-08-2007: Seminar introduction talk by prof. Baeten.

11-09-2007: First two presentations: [Mil84] and [BK84icalp].

25-09-2007: Third presentation [Mo90] and part 2 of the presentation of [Mil84].

Block B

09-10-2007: Part 2 of the presentation of [BK84icalp].

23-10-2007: The presentation of [BBP94] and [BCG07].

06-11-2007: The presentation of [MM94concur] and [BBK87tcs].

Block C

Before: Study the material and collect ideas for a possible solution.

20-11-2007: Discussion about the research, finding a solution.

04-12-2007: Second research discussion (in HG 7.19).

14-12-2007: Deadline for sending in paper segments.

18-12-2007: Final seminar meeting!

Research Proposal

In the research we consider the process algebras BPA and PA. PA has not been discussed during the seminar, but it is BPA extended with interleaving (merge and left merge operators), so parallelism without communication. Bergstra et at. prove that BPA* is less expressive than PA* [BBP94] and also that BPA*0 is less expressive than PA*0, where 0 is the deadlocked process (denoted in [BBP94] with δ). The goal of the research is to find out that if we add the empty process 1 to both BPA*0 and PA*0, then we can show that BPA*0,1 is less expressive than PA*0,1 using a proof similar to the proofs given in [BBP94] and [BFP01]. An alternative proof could proceed via the result in [BCG07] that the processes denoted by closed BPA*0,1-terms are precisely those definable by well-behaved recursive BPA0,1-specifications. Note that due to the presence of 1, the binary star p*q used in the papers gives rise to the definition of the unary star p* using p*1.