I've been working on the 3rd assignment of Formal Methods today.

The assignments basically involve describing various systems in a formal language, and then generating a state-space of it. There are a number of tricks to reduce this state-space, while some properties will still hold. This way it's easy to prove certain behaviour.

In the assignment I did today (not quite finished yet), the goal is to prove that the alternating-bit protocol is a good protocol. That is, that a bit put in from one side will come out from the other one (even though the channels might be unreliable). After reduction of the original state-space (left), only 3 states remain: 0 (nothing going on), 1 (a 1 is sent and received) and 2 (a 0 is sent and received). The thing we proved this way is that there is no 'state 3' in which for example a 1 is sent and a 0 received (this would be an error).


Tomorrow I'll go to Chess and continue there because I want to print a few of the state-spaces. This to help me understand exactly how the state-space reduction algorithms work.

He's on the bus, it takes about 26 hours before he's in Hungary...

I'll take the train in about 15 minutes to Amsterdam Amstel. Daniël is leaving again and we'll have some coffee.

Just came back from Ettie, working on some physics... I must admit I forgot a lot. Newton's Laws have never been my best subject really.

Like I wrote about a week ago, the Dutch parliament can be viewed online.

Accidentally I found out that the British Parliament also has such a webcam, see here. Quote from today's debate: "terrorism is wicked and must be stopped".

Yesterday I studied some more theory on Formal Methods, and today I started the practical work. I finished the first assignment, which is about analysing a very simple protocol. The picture here is a instantiation of a system where two 1-bit buffers are put in sequence.

There has been a new release of the program I use for this website, PhpNuke. I've just installed it, and things seem to work fine.

Not a lot of changes, but the new version has a few features that are useful for me as administrator. Most important though is the fact that it's more secure (for the experts: it now allows register_globals() to be off).


A nice thing is the fact that there are a few new Themes, have a look at them here.


If you do find any bugs, please let me know.

Exactly one hour ago (at 6:55) autumn started.

It was a nice evening with musaka and a movie: "Kissing a Fool". Quite amusing. If you have a decent internet connection you could look at the movie's trailer here (in QuickTime), or at a longer preview here.

Today is a car-free day in Europe, and Haarlem is also participating.

A little further down the Spaarne both the sides of the river are blocked for traffic and there's another big street that will be used for a market and children-games instead of for cars.

There are 39 cities in the Netherlands with a car-free Sunday, in Bulgaria 82 (see their website).



The car-free day is an invention of the French minister Dominique Voynet; it started in France in 1998.