Sunday, December 24, 2006

Christmas Reading

Science magazine has chosen Perelman's proof of the Poincare Conjecture as breakthrough of the year for 2006. See this article by Dana Mackenzie. You can also read about the nine runners-up as well as the scientific fraud of the year.

The January 2007 issue of Scientific American features an article by Bill Gates entitled A Robot in Every Home.

Happy reading and merry Christmas.

Friday, December 22, 2006

Sussex in 1987

Julian Rathke is moving from Brighton to Southampton, where he joins Vladimiro Sassone (another former member of the School of Informatics at the University of Sussex). It does not take magical powers to foresee that Southampton will soon have a very strong theory group.

Julian tells me that it is a strange time at Sussex. Half of the department is moving buildings, so the department office and all of the secretaries are gone, the good old debugging room (the unofficial coffee room of the department at a time when the university regulations essentially did not allow for such rooms, hence the name) is also no more. Just an empty shell of a room now. Very sad.

Reading Julian's description prompted me to look back to a windy September-October 1987, when I arrived in Brighton to work for a year as a research assistant under Matthew Hennessy. The department of computer science was very small then. Yet, there was already a tightly knit group of theory people that created a very good atmosphere for intellectual growth. At that time, Marek Bedcnarzyk was putting the final touches to his PhD thesis, and Allen Stoughton was finalizing his monograph on fully abstract models of programming languages. Mark Millington, one of Matthew's former Edinburgh students, was there teaching Software Engineering. (It is a pity that Mark's PhD thesis is not very well known. It was a good piece of work.) I shared an office with Rance Cleaveland, a freshly minted PhD from Cornell, where he had formalized theories of processes using NuPRL. (Rance was working on the development of the Concurrency Workbench, but did a lot more than that---not least, he taught me a lot over beers at our local pub :-)) Across the fire doors leading to the Mathematics department, Andy Pitts was spending some time at Sussex, supported by a grant from the Royal Society.

Already the year after, the theory group grew substantially in size, with the arrival of PhD students from Britain and from abroad, postdocs, and later new members of staff. The rest, as they say, is history. It is a pity that not so much is left of that theory group at Sussex. (The linchpin, Matthew Hennessy, is still there, but many people have come and gone in the meantime.)


This is one of the pros and cons of academic life. One travels from place to place, possibly grows attached to each of the departments/centres one works for, and the colleagues one meets there, but eventually we all leave for somewhere else.

Good luck to Julian for his new job at Southampton, and congratulations to Vladi for having enticed an excellent collaborator like Julian to join his new department.

Monday, December 18, 2006

Being Head of Department: A New Experience

As of 1 January 2007, and for at least about eight months, I'll be the acting head of the CS department at Reykjavík University.

Not surprisingly, I am trying to gather some useful advice on how to survive this new experience, and hopefully live to tell the tale as far as research, teaching and service to the academic community are concerned. So far, I have found some useful information on the CRA web site, but I'd love to hear any advice you might have on how to manage one's time while being head of department, and what aspects of the job one should be particularly aware of. Drop me a line, or use the comments section. I'll be grateful for any piece of information you might provide.

I apologize to those of you who kindly invited me to serve on PCs for conferences during the first half of 2007. I was honoured by your consideration, but decided to politely decline all of those invitations rather than do a bad job. (I must freely admit that the prospect of chairing the department is worrying me somewhat :-() I hope that I made the right choice.

Saturday, December 16, 2006

Research in Italy

Yesterday I travelled back to Reykjavík after a very short visit to Italy. During the trip back to the North Atlantic, I was reading La Repubblica, an Italian newspaper. One of the news items that caught my eye dealt with the protests by the rectors of Italian universities, who are very unhappy about the cuts to their institutions' budgets that are part of the latest financial law passed by the Italian government.

I am afraid that I do not know enough about the developments to express an informed opinion about the whole thing. However, I have always sternly refused to buy the argument that, unlike other countries, Italy does not have the cash to support universities and research. How can a member state of the G8 elite be short of money to support its future? Let's not mask lack of interest in science and technology as supposed poverty. By way of example, BRICS and the other research centres of the Danish National Research Foundation were richly funded for five-year periods (14 years for BRICS) with the interests resulting from the privatization of an insurance company! The outcome for Danish science is for everybody to see.

Why shouldn't the same type of investment in basic research be possible in a country like Italy? The reasons must be the same that prevent Italy from investing in its schools and universities. Three figures in the article I was reading yesterday paint an amazingly bleak picture. Italy boasts only about 3 researchers every 1000 workers. This is less than each of the other countries mentioned in the list. We (Italians) spend only about 1.2% of the GNP in research. Only Greece, Spain and Portugal invest less. Last but not least, Italy spends only 8000$ a year per university student. This is the same as Hungary, and half of what Sweden spends. Why are we Italians so masochistic?

Still, if I look at Italian research in TCS, I can only classify it as being very strong, despite the lack of money for research and the sub-optimal support. Yes, I know that I am biased. Even though I have never worked in an Italian university myself, I try to maintain good ties with my colleagues based in Italy. It is, however, an incontrovertible fact that there are many very active and very strong Italian TCS researchers. The strongest Italian CS departments are high class, and Italy exports talent. Off the top of my head, I could come up with the following list of Italian TCS researchers working abroad (with apologies to those whose names have not crossed my mind right now):

  1. Luca de Alfaro
  2. Roberto Amadio
  3. Antonio Bucciarelli
  4. Cristiano Calcagno
  5. Luca Cardelli
  6. Ilaria Castellani
  7. Giuseppe Castagna
  8. Roberto Di Cosmo
  9. Luigi Liquori (who is from Pescara like me)
  10. Giuseppe Longo
  11. Sergio Maffeis
  12. Pasquale Malacaria
  13. Silvio Micali
  14. Catuscia Palamidessi
  15. Luigi Santocanale
  16. Vladimiro Sassone
  17. Luca Trevisan
  18. Daniele Varacca
  19. Luca Viganò
  20. Francesco Zappa Nardelli
(Notice how many of these researchers work in France, and how many of them are located in Paris!) I believe that the above people would be considered as forming a very strong theory group anywhere in the world, and there are many more strong TCS researchers in Italy itself. I can only encourage the Italian political establishment and Italian universities to give Italian researchers a suitable environment for producing the best research they can. To my mind, this would be a win-win situation for Italy as a whole. Unfortunately for Italian science, it looks like Italy's politicians disagree with me.

Addendum 19/12/2006: Yesterday I read an article by Princeton philosopher Peter Singer, on the subject of philantropy, poverty and ethics. (Thanks to Luca Trevisan for his post on this very interesting article, which is a must read during the crazy Christmas period.)

The following excerpt from that article struck me as being very relevant to this disjointed post of mine:

The Nobel Prize-winning economist and social scientist Herbert Simon estimated that “social capital” is responsible for at least 90 percent of what people earn in wealthy societies like those of the United States or northwestern Europe. By social capital Simon meant not only natural resources but, more important, the technology and organizational skills in the community, and the presence of good government. These are the foundation on which the rich can begin their work.

If instead of wealth, we consider "intellectual output", how much would Italian researchers produce in the presence of better technology and organizational skills in the community, and in the presence of good government? What if they could devote more of their time to not fighting against the system?

Thursday, December 14, 2006

Zeilberger's 76th Opinion

Dr. Z strikes again. Read his 76th opinion, entitled Why P Does Not Equal NP and Why Humans Will Never Prove It by Themselves, and form your own counter-opinion. As usual, reading Zeilberger's opinion won't leave you cold.

Zeilberger writes:

All the problems in, say, Garey and Johnson, are essentially one problem, since they are all trivially equivalent.

Well, I am not sure that I agree that those problems are "trivially" equivalent. "Triviality" is in the eye of the beholder, and maybe one has to be a top notch mathematician like Zeilberger in order to find all of the reductions between NP-complete problems trivial. I admit that I do not find most of them to be trivial at all.

I also find the characterization of the work of complexity theorists as "just proving yet-another reduction theorem" somewhat restrictive.

I am expecting to see some comments on this opinion on the complexity theoretic blogs.

Addendum posted on 15 December 2006: Read Luca Trevisan's thoughtful comments.

Let me also mention another statement of Zeilberger's from opinion 76:

There is no hope, as smart and "creative" as you and your cronies are, that you will be able to prove it by yourselves. Your only hope is to enlist that "simple" mechanical device, that ironically, you computer-scientists, do not use very much, not even for spell-checking!

Now that I have algebraic combinatorialists working near me, I can vouch that they use computers a fair amount in their work---possibly more than many theoretical computer scientists. However, in concurrency theory, people construct and use software tools to make models of computing devices and to analyze their behaviour algorithmically. Readers who have never used such tools might wish to play with Uppaal or HyTech to mention but two such tools.

Wednesday, December 13, 2006

Accepted Papers for FOSSACS 2007

The list of accepted papers for FOSSACS 2007 is now available. (Thanks to Jun Pang for the pointer.) The conference looks interesting, and I hope to report on some of the papers when, if ever, I have time to read them.

Tuesday, December 12, 2006

Accepted Papers at ETAPS 2007

The list of accepted papers for TACAS 2007 is out, and so is the one for ESOP 2007. TACAS accepted as many as 54 papers, and the list of contributors looks very impressive. Several papers have an all-star list of authors, e.g.,

Multi-Objective Model Checking of Markov Decision Processes by Kousha Etessami, Marta Kwiatkowska, Moshe Y. Vardi, and Mihalis Yannakakis.

ESOP features a list of accepted papers that is definitely of interest to concurrency theorists.

Most accepted papers at TACAS and ESOP have at least three authors, further confirming the trend to higher and higher degrees of collaboration in most fields of TCS.

Happy browsing! I am still awaiting the list of accepted papers for FOSSACS 2007. In any event, the tenth anniversary edition of ETAPS looks already like a conference one should attend. I myself, however, will be attending a marriage of mathematicians that will be held in Chicago at around that time.

Monday, December 11, 2006

RIP (Research In Peace)

The Institut Mittag-Leffler has just celebrated its ninetieth birthday. It is a Nordic research institute for mathematics, under the auspices of the Royal Swedish Academy of Sciences, created by Gösta and Signe Mittag-Leffler who donated their house, library and fortune to the Academy. The Institute runs year-long research programs in specialized areas of mathematics, and I am told that it is a great place to visit.

One of their programmes is called RIP (Research in Peace). This is a programme allowing mathematicians from Scandinavian universities, who are not directly connected to the current scientific programme, to visit the Institute for shorter periods. My colleague, and frequent indirect contributor to this blog, Anders Claesson is presently visiting Mittag-Leffler using the RIP programme.

Maybe some of you will be interested in organizing a programme on some topic in TCS at that institution.

Friday, December 08, 2006

Characteristic Formulae for Timed Automata

The last installment of this series of three posts on characteristic formulae deals with characteristic formulae for behavioural equivalences over timed automata.

The first construction of a characteristic formula for timed bisimilarity over timed automata I am aware of was presented in the paper

François Laroussinie, Kim G. Larsen, and Carsten Weise. From Timed Automata to Logic - and Back. Jirí Wiedermann, Petr Hájek (Eds.): Mathematical Foundations of Computer Science 1995, 20th International Symposium, MFCS'95, Prague, Czech Republic, August 28 - September 1, 1995, Proceedings. Lecture Notes in Computer Science 969 Springer 1995, ISBN 3-540-60246-1.

In that paper, the authors propose a timed version of Hennessy-Milner logic Lnu, and show thateach timed automaton can be uniquely characterized by a single formula in that logic up to timed bisimilarity.

The construction in that paper relied on the region graph of the timed automaton, and thus produces "large" formulae. (See yesterday's post on the number of regions in a timed automaton.) In the setting of timed automata without invariants, the construction by Laroussinie, Larsen and Weise was improved upon in the paper

Luca Aceto, Anna Ingólfsdóttir, Mikkel Lykke Pedersen, and Jan Poulsen. Characteristic Formulae for Timed Automata. ITA 34(6): 565-584 (2000).

That paper offers characteristic formula constructions in the real-time logic Lnu for several behavioural relations between (states of) timed automata. The behavioural relations studied in op. cit. are timed (bi)similarity, timed ready simulation, faster-than bisimilarity and timed trace inclusion. The characteristic formulae delivered by the constructions offered in the aforementioned paper have size which is linear in that of the timed automaton they logically describe.

Finally, the paper

Luca Aceto, Patricia Bouyer, Augusto Burgueño, Kim G. Larsen. The power of reachability testing for timed automata. Theor. Comput. Sci. 300(1-3): 411-475 (2003)

uses a property language characterizing the power of reachability testing over timed automata in the context of "test automata" to provide a definition of characteristic properties with respect to a timed version of the ready simulation preorder, for nodes of τ-free, deterministic timed automata.

I am not aware of a timed counterpart of the results by Browne, Clarke and Grümberg on the characterization of bisimulation-like equivalences over Kripke structures using characteristic formulae in fragments of CTL. Is Timed CTL expressive enough to describe characteristic formulae for timed bisimilarity? This has been an item on my "to do" list for quite some time, but I have never had the guts to start working on the problem yet.

Thursday, December 07, 2006

Number of Regions in a Timed Automaton

While working on the book Reactive Systems: Modelling, Specification and Verification, my co-authors and I were looking for a formula counting the number of regions in a timed automaton exactly in order to motivate the introduction of the notion of zone. Thanks to Rajeev Alur and Tom Henzinger, I now know the answer, which I report here in case anybody else is interested.

There is a characterization of the number of regions where all clocks lie between 0 and 1 in terms of Stirling numbers of the second kind in this paper (page 13 bottom).

Peter Kopke's PhD thesis available from Tom's web page at http://mtc.epfl.ch/~tah/Students/kopke.pdf also contains that characterization. The section that starts on page 164 (of the file) offers the following formula:

Regions(2n) = sumk=12n Sk2n k!

where Regions(2n) is the number of equivalence classes over 2n clocks each constrained to lie in the interval (0,1), and Sk2n is the number of ways of partitioning a set with 2n elements into k subsets. So Regions(2n) is exactly the number of ways of partitioning a set with 2n elements into k ordered subsets.

As the algebraic combinatorialists here at Reykjavík University know well, I am always very impressed by these counting formulae :-)

Tuesday, December 05, 2006

IFIP WG1.8 Workshop at CONCUR

The IFIP WG1.8 on Concurrency Theory will organize a strategic workshop at CONCUR 2007. (The workshop proposal is below.) I'll post more details on the workshop as they become available. In particular, a web page for the event will be ready by 15 January, 2007. For the moment, I am happy to inform you that Hubert Garavel has accepted to deliver one of the addresses at the event.

---------------------------------------


TITLE: IFIP WG 1.8 Workshop on Applying Concurrency Research in Industry (7 or 8 September 2007)

DURATION: Half a day

ORGANIZERS: Luca Aceto, Jos Baeten, Wan Fokkink, Anna Ingolfsdottir, and Uwe Nestmann (on behalf of WG1.8)

SUMMARY: This strategic workshop, held under the auspices of IFIP Working Group 1.8 on Concurrency Theory, aims at highlighting the challenges that arise in applying concurrency theory research in an industrial setting, broadly construed. Its purpose is to be a forum for the discussion of the state-of-the-art in the transfer of results from concurrency theory to industry, and for distilling the lessons to be learned from the successes and failures so far. Moreover, we shall discuss, e.g., how to increase the impact that concurrency research can have in industry, the role of software tools in this technology transfer effort, and what are possible novel industrial application areas of concurrency theory research. The ultimate goal of the meeting, and subsequent discussions, will be to establish road map(s) for the concurrency theory community, or parts thereof, in applying its research in industrial settings.

The topic of the workshop is strongly related to all of the areas of CONCUR interest. Semantics, logics, and verification techniques for concurrent systems are necessary for the development of languages and methods for use in industrial applications. Conversely, the industrial applications of methods from concurrency theory research stimulate further advances in the basic theory covered by the CONCUR conference series. Successful applications of concurrency theory in industry further highlight the fundamental scientific and technological relevance of work done within the CONCUR community.

SELECTION OF PAPERS: The workshop will consist of three-four invited presentations, followed by discussions. We might summarize the presentations and discussions in an article for the concurrency column of the Bulletin of the EATCS. The theme of the workshop could form the basis for a special issue of a journal (for instance JLAP), but such a special issue would not be necessarily based upon presentations at the workshop. There would be a separate call for contributions for that volume.

Monday, December 04, 2006

Italian Success in Logic

I have just read an email message on the mailing list of the Italian Association for Logic and its Applications (AILA). The news is that Matteo Viale has been awarded the 2006 Sacks Prize of the ASL.

Matteo Viale finished his doctorate last September at the University of Turin and the University of Paris VII (co-supervised by Alessandro Andretta and Boban Velickovic) . In his thesis, he has solved one of the major open problems in logic and set theory by showing that the proper forcing axiom (PFA) implies the singular cardinal hypothesis (SCH). The result is reported in this paper.

Congrats to Matteo!

News from EATCS

The Call for Papers of ICALP 2007 has been published. I hope you will contribute to that success of that conference by submitting the best results of your research work to it. The PC for track B looks definitely concurrency friendly.

The Call for Nominations for the 2007 Gödel Prize has been posted on the EATCS web site. The deadline for nominations is January 31, 2007.

The Call for Nominations for the 2007 EATCS Award has been published (page 13 of Bulletin issue 90). The nominations should be sent to Wolfgang Thomas by December 15, 2006. Hurry up if you do intend to nominate one of our colleagues in concurrency theory!

Friday, December 01, 2006

A Google Talk by Luis von Ahn

If you have a few spare moments, look at this very interesting talk by Luis von Ahn:
http://video.google.com/videoplay?docid=-8246463980976635143&q=google+TechTalks.
(Thanks to Anders Claesson for this pointer.)

Luis von Ahn is the winner of one of the MacArthur genius awards for 2006. I just tried his ESP game ( http://www.espgame.org/) for the first time. It is actually rather smart, in a way, and apparently some people play it a lot (even over 10 hours a day, according to von Ahn). In so doing, they help label images on the web, using all those human brain cycles devoted to game playing for a good cause.