February 2008 Issue of the BEATCS

Volume 94 of the Bulletin of the EATCS is now available on line, freely and to everybody as it should be.

Of course, you should read the two pieces that make up the concurrency column :-) In addition, apart from the contributions to the other columns in the Bulletin, I encourage you to have a look at A "big-ideas" approach to teaching Computation Theory , a contribution to the educational column by Arnold L. Rosenberg. I have not had time to mull over his proposal yet, but it is certainly worth thinking about it and contributing our two-cent worth to what is an interesting opinion on how to teach one of our flagship courses.

Let me encourage you to support the EATCS by becoming a member of that association. For a mere 25 € 30 € per year (25€ if you are also a SIGACT member), you will make sure that the EATCS can continue supporting TCS research as a whole.

What is the Shortest PhD Thesis in TCS?

Gmail's webclips feature alerted me to the availability of Edmund Landau's PhD thesis in English translation. The thesis is 13 pages, which is substantially shorter than any PhD thesis in CS I am aware of.

I suspect that PhD theses in mathematics are, by and large, shorter than those in TCS. What is the shortest PhD thesis in either subject you are aware of? (In the case of mathematics, let's restrict ourselves to modern times, but if anyone knows of a thesis that is shorter than Landau's I'd be interested in knowing the details.)

Here is my own contribution. Off the top of my head, I recall that Jay Loren Gischer's PhD thesis from Stanford (year: 1984; topic: the theory of pomsets; supervisor: Vaughan Pratt, see also here) was between 45- and 50-page long.

Abel Prize 2008

The Norwegian Academy of Science and Letters has decided to award the Abel Prize for 2008 to John Griggs Thompson, University of Florida and Jacques Tits, Collège de France. Thompson and Tits receives the Abel Prize “for their profound achievements in algebra and in particular for shaping modern group theory”.

The committee's citation can be read here. Thompson and Walter Feit are the authors of the famous Odd Order Paper, filling a whole issue of the Pacific Journal of Mathematics. Georges Gonthier is leading an effort that aims to produce a computer-checked proof of this famous result in group theory.

The Usefulness of Bisimilarity Checking in Practice

I am collecting information as well as opinions on the practical usefulness of bisimulation checking. I feel that there are disparate views out there and they may be worth recounting. I plan to solicit opinions from experts in the verification community, but I am also interested in the thoughts on this topic of the readers of this blog. Feel free to email me your opinions or to post a comment. I would also appreciate receiving bibliographic references where the usefulness of bisimulation checking and bisimulation minimization are discussed.

Thanks in advance!

Accepted Papers for LICS 2008

The list of accepted papers for LICS 2008 is now available here. Some of the accepted papers that, judging by their titles, ought to be of interest for a concurrency theorist are the following ones.

- Christel Baier, Nathalie Bertrand, Patricia Bouyer, Thomas Brihaye and Marcus Groesser. Almost-Sure Model Checking of Infinite Paths in One-Clock Timed Automata

- Taolue Chen and Wan Fokkink. On the Axiomatizability of Impossible Futures: Preorder versus Equivalence

- Ivan Lanese, Jorge A. Perez, Davide Sangiorgi and Alan Schmitt. On the Expressiveness and Decidability of Higher-Order Process Calculi

- Emmanuel Beffara. An Algebraic Process Calculus

- Tomas Brazdil, Jan Kretinsky, Antonin Kucera and Vojtech Forejt. The Satisfiability Problem for Probabilistic CTL

- Sam Staton. General Structural Operational Semantics through Categorical Logic

I'll try to find some time to write a few lines on at least some of them when they are available on line.

Axiomatizing Restriction and Relabelling

Time flies somehow. At some point in late February I posted the following paper:

Luca Aceto, Anna Ingolfsdottir, Bas Luttik and Paul van Tilburg. Finite Equational Bases for Fragments of CCS with Restriction and Relabelling. Technical Report CSR-08-08, TU/Eindhoven, February 2008.

I meant to write a blog entry on the paper then, but that intention has not materialized until now.

So what is the above study about? We investigate the equational theory of several fragments of Milner's CCS modulo (strong) bisimilarity with special attention to restriction and relabelling. The largest fragment we consider includes action prefixing, choice, parallel composition without communication, restriction and relabelling. We present a finite equational base (i.e., a finite ground-complete and omega-complete axiomatisation) for it, including the left merge from ACP as auxiliary operation to facilitate the axiomatisation of parallel composition.

Perhaps surprisingly, no complete axiomatisations of bisimilarity over languages including restriction and relabelling have been given to date. In a classic paper, Milner studied an algebra of flowgraphs with operations of (parallel) composition, restriction and relabelling, and provided a complete axiomatisation for it. In that reference, however, the notion of equivalence between expressions is purely “structural”, since two expressions are equated when they denote the same flowgraph up to isomorphism.

I hope that some of you will find the paper worth looking at. I enjoyed working on it a lot, thanks to my co-authors.

Four IFIP Scholarships for ICALP 2008

IFIP TC1 has kindly provided sponsorship for four 500-euro scholarships. The four scholarships will be used to support participation in ICALP 2008 by young researchers from countries where access to funds is limited by covering registration and some of the local expenses. Preference will be given to PhD students presenting papers at the conference.

To apply for one of the IFIP scholarships, please send an email to the address icalp08 AT ru DOT is. The application should be sent by Wednesday, 30 April 2008, at 12:00 GMT, and should contain a motivation for the sponsorship request together with an indication of whether the applicant is a co-author of one of the papers selected for the conference.

Proving Non-finite Axiomatizability Results Via Reductions

I recently completed the writing of two papers before the final rush towards ICALP 2008. The first of these papers, in chronological order, is

Luca Aceto, Wan Fokkink, Anna Ingolfsdottir and MohammadReza Mousavi. Lifting Non-Finite Axiomatizability Results to Extensions of Process Algebras. Technical Report CSR-08-05, TU/Eindhoven, February 2008.

The general setting for the work reported in this paper is that of process algebras, which are prototype languages for the description of reactive systems. Since these languages may be used for describing specifications of process behaviour as well as their implementations, an important ingredient in their theory is a notion of equivalence or approximation between process descriptions. The equivalence between two terms in a process algebra indicates that, although possibly syntactically different, these terms describe essentially the same behaviour. Behavioural equivalences are therefore typically used in the theory of process algebras as the formal yardstick by means of which one can establish the correctness of an implementation with respect to a given specification.

In the light of the algebraic nature of process algebras, a natural question is whether the chosen notion of behavioural equivalence or approximation can be axiomatized by means of a finite collection of equations. The first negative results concerning finite axiomatizability of process algebras go back to the Ph.D. thesis of Faron Moller. Since then, several other non-finite axiomatizability results have been obtained for a wide collection of very basic process algebras; see here for a survey of such results dated mid-2005.

In general, results concerning (non-)finite axiomatizability are very vulnerable to small changes in, and extensions of, the formalism under study. Furthermore, proofs of non-finite axiomatizability results in the concurrency-theory literature are extremely delicate, rather long and error-prone. Hence, it would be useful to find some general techniques that can be used to prove non-finite axiomatizability results. Such a general theory would allow one to relate non-finite axiomatizability theorems for different formalisms, and spare researchers (some of) the delicate technical analysis needed to adapt the proofs of such results. The search for such general results is what inspired our research leading to this paper.

In the aforementioned paper, we present a theorem offering a general technique that can be used to prove non-finite axiomatizability results, and present some of its applications within concurrency theory. In this theorem, we give sufficient criteria to obtain new non-finite axiomatizability results from known ones.

The technique we propose is based on a variation on the classic idea of reduction mappings, which underlies the proofs of many classic undecidability results in computability theory and of lower bounds in complexity theory. In this setting, reductions are translations between languages that preserve sound (in)equations and (in)equational proofs over the source language, and reflect families of (in)equations responsible for the non-finite axiomatizability of the target language. In other words, the existence of a reduction shows that

• "nasty" families of (in)equations over the target language are also present in the source language, and
  
• if they were provable by means of a finite collection of valid (in)equations in the source language, they would also be "finitely provable" in the target language.
  

We show the applicability of our reduction-based technique by obtaining seven, to our knowledge novel, non-finite axiomatizability results for timed and stochastic process algebras. We also investigate some limitations of our approach. In particular, we show that prebisimilarity is not finitely based over CCS with the divergent process Omega, but that this result cannot be proved by a reduction to the non-finite axiomatizability of CCS modulo bisimilarity.

There are a few promising areas of further research in this area, and we are currently exploring some of them (ICALP organization and other tasks permitting).

I'll write a few lines on the second paper soon, but those of you who are interested in looking at it may find it here.

CS/Math Blogging and Social Skills

A very recent post by David Eppstein discusses the risks untenured academics may run into when blogging. David mentions the following typical quote: “pretenured professors should be aware of the risks of blogging and develop strategies to avoid or mitigate the pitfalls of blogging without a tenure net.”

I have the feeling, however, that at times what is needed is not the development of strategies for "safe blogging", but rather an appreciation of the fact that academics live in a society of peers, and that social skills and tact are needed for most of us to thrive in the scientific community. When supervising budding academics, we focus a lot on their scientific development, and rightly so. I am starting to believe, however, that at the same time we should pay more attention to the development of their "social skills". Being able to maintain a good working relationship with one's colleagues is a definite plus at work. Being perceived as an arrogant oddball typically isn't. Spurting gratuitous vitriolic remarks may be even funny in the very short term, but I believe that it soon becomes tiring.

We are part of a community, and a certain amount of respect for the work of our peers is healthy, if not altogether necessary, for the proper working of our society. I do not think that it is a proper thing to do to refer to one's colleagues as "losers" or to conferences as "worthless". We are all in this business to try and offer our modest contributions to (theoretical) computer science. Some of us are definitely more successful than others, but we (and most of our scientific conferences and journals) all have a role, no matter how tiny, to play. When a conference or workshop is not playing a useful role for the community it addresses, either it stops running or it redefines its scope.

Sheer arrogance serves neither the community as a whole nor the individuals who exhibit it. It will lead us nowhere. We should teach our students to exercise their freedom in judging their future colleagues with care, and make them aware of the dangers of considering themselves geniuses who are not bound by the minimal social conventions that apply to most common mortals. In fact, reading the blogs of, or talking to, scientists whose work I admire, I have always been struck by their courtesy and professionalism. We should all learn from their good example.

As an aside, Timothy Gowers, in his lovely little book "Mathematics: A Very Short Introduction", writes:

It is my impression, and I am not alone in thinking this, that, among those [the mathematicians] who do survive the various culls, there is usually a smaller proportion of oddballs than in the initial student population.

While the negative portrayal of mathematicians may be damaging, ...., the damage done by the word 'genius' is more insidious and possibly greater.....

The last quality [exceptional strategic ability] is, ultimately, more important than freakish mental speed: the most profound contributions to mathematics are often made by tortoises rather than hares.

I strongly recommend the book. It is really well written.