Modelling and Verification 2006

The news items are listed roughly in reverse chronological order.

- Friday, 17 March 2006: Those of you who are interested in understanding why the
algorithm presented on page 27 of the slides for lecture 17
works are encouraged to read Appendix A.3 in the textbook. The algorithm
on that page is nothing but the algorithm described on page 239 of the
textbook phrased in terms of boolean logic. The following
legenda might be of help:
- Bis(
**x**,**u**) stands for the boolean formula that describes the set of pairs of bisimilar states (namely strong bisimilarity). This set is computed iteratively. Initially, all pairs of states are bisimilar because we have no reason to distinguish them. So, initially Bis(**x**,**u**) := 1. - Old(
**x**,**u**) := Bis(**x**,**u**) records the set of states that were considered bisimilar at the previous iteration. - The new approximation to strong bisimilarity is computed using Old(
**x**,**u**) and the definition of bisimilarity. - If the new formula for Bis(
**x**,**u**) is equivalent to Old(**x**,**u**), then we can stop. Otherwise we iterate steps 2 and 3 above once more.

- Bis(
- Friday, 17 March 2006: A revised version of the textbook is now available as a postscript file. This version implements the list of errata pointed out by the students following the course in Aalborg right now.
- Friday, 17 March 2006: Today I'll be holding a revision class before the exam. This will be an "all questions answered" session. It'll be very short if you do not have questions ready!
- Tuesday, 14 March 2006: I have posted a new schedule for the exam on the exam page. Please check it before the exam day!
- Tuesday, 14 March 2006: The solutions for the sixth and last exercise sheet are now available.
- Monday, 13 March 2006: I have swapped Jónas Tryggvi Jóhannsson and Dađi Ármannsson in the schedule for the oral exam.
- Friday, 10 March 2006: The preliminary schedule for the exam on Wednesday, 22 March,
is
as follows:
- 13:00-13:20 Bjarki Elías Kristjánsson
- 13:20-13:40 Jónas Tryggvi Jóhannsson
- 13:40-14:00 Guđmundur Hreiđarsson
- 14:00-14:20 Gunnar Kristjánsson
- 14:20-14:40 Hafţór Guđnason
- 14:40-15:00 Hilmar Finnsson
- 15:00-15:20 Dađi Ármannsson
- 15:20-15:40 Kristján Valur Jónsson
- 15:40-16:00 María Arinbjarnar
- 16:00-16:20 Örn Arnar Jónsson
- 16:20-16:40 Sólmundur Jónsson

- Thursday, 9 March 2006: Gerd Behrmann has just informed me that IBEN, the tool I mentioned repeatedly during the lectures, is available for download from http://iben.sourceforge.net/. Download it and play with it!
- Tuesday, 7 March 2006: The exercise sheet for tomorrow's session is now available.
- Monday, 6 March 2006: A revised version of the textbook is now available as a postscript file. This version implements the list of errata pointed out by you and the students following the course in Aalborg right now.
- Saturday, 4 March 2006: Preliminary information on the exam is now available. You can already begin to prepare all but one of the five exam questions. The last lecture in the course will be mostly devoted to a discussion of the exam questions.
- Wednesday, 1 March 2006: The schedule for the rest of the course is now available!
- Wednesday, 1 March 2006: The whole of the afternoon session today will be devoted to second miniproject.
- Tuesday, 28 February 2006: The solutions for the fifth exercise sheet are now available.
- Tuesday, 21 February 2006: The second miniproject is now available! You will be working on it during the lecture time on Friday, 24 February, and the whole afternoon on Wednesday, 1 March. Make sure you have Uppaal installed and that you have read the suggested tutorial paper before Friday.
- Tuesday, 21 February 2006: The slides for tomorrow's lecture are now available as a file in PDF format. A new exercise sheet and the solutions for the fourth exercise sheet are also available.
- Friday, 17 February 2006: The slides for today's lecture are now available as a file in PDF format.
- Tuesday, 14 February 2006: Information on the exam! The oral exam for the course will be held on Wednesday, 22 March, from 13:00 in room 303. Details of the exam process will be posted on these pages in due course.
- Tuesday, 14 February 2006: The slides for tomorrow's lecture are now available as a file in PDF format. A new exercise sheet is also available.
- Thursday, 9 February 2006: Tomorrow's lecture time will be devoted to your work on the Alternating Bit Protocol. The exercise session on Wednesday, 15 February, will also be used for that assignment. Bear in mind that you are expected to work on the assignment also outside the lecture/tutorial time.
- Tuesday, 7 February 2006: When installing the CWB on Windows XP use SML 110.0.7, IIRC. That certainly works.
- Thursday, 2 February 2006: The slides for tomorrow's lecture are now available as a file in PDF format.
- Thursday, 2 February 2006: The first miniproject is now available!
- Wednesday, 1 February 2006: Work on the first miniproject is will begin on Wednesday, 8 February 2006. I will supervise your work on the miniproject during the lecture time and the subsequent exercise session.
- Wednesday, 1 February 2006: The solutions to the exercises for the second tutorial are now available.
- Wednesday, 1 February 2006: The list of exercises for our third tutorial/exercise session is now available.
- Wednesday, 1 February 2006: The slides for today's lecture are now available as a file in PDF format.
- Monday, 30 January 2006: A new version of the errata for the book has been posted.
- Thursday, 26 January 2006: The slides for tomorrow's lecture are now available as a file in PDF format.
- Thursday, 26 January 2006: The solutions to the exercises for the first tutorial are now available.
- Wednesday, 25 January 2006: The slides for today's lecture are now available as a file in PDF format.
- Tuesday, 24 January 2006: The list of exercises for our second tutorial/exercise session is now available. Make sure you have it available tomorrow.
- Thursday, 19 January 2006: The slides for tomorrow's lecture are now available as a file in PDF format.
- Thursday, 19 January 2006: Work on the first miniproject is tentatively scheduled to begin on Friday, 3 February 2006. I will supervise your work on the miniproject during the lecture time and the subsequent exercise session.
- Wednesday, 18 January 2006: The slides for today's lecture are now available as a file in PDF format.
- Tuesday, 17 January 2006: The list of exercises for our first tutorial/exercise session is now available. Make sure you have it available tomorrow.
- Friday, 13 January 2006: The first errata for the book have been reported. See the errata file (PDF).
- Friday, 13 January 2006: The slides for today's lecture are now available as a file in PDF format.
- Wednesday, 11 January 2006: The tutorials/exercise sessions for this course will take place on Wednesdays from 14:45 till about 16:00. These sessions will take place in room 303.
- Wednesday, 11 January 2006: The slides for today's lecture are now available as a file in PDF format. You might also wish to look at some old, scanned handwritten slides of mine.
- Friday, 6 January 2006: The exercise sessions for this course will be held
on Tuesdays from 13:00 till 14:35. The room for the exercise sessions will be
announced soon. Some of the exercise sessions will be used for the work on your
mini projects.

Note: I expect you to do the exercises with my assistance! - Friday, 6 January 2006: Copies of the current draft of the textbook for the course are now available for purchase from the library. A bound copy costs 1800 ISK. I strongly recommend that you buy one.
- Monday, 2 January 2006: A draft web page for the course is available here.