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.

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) = sum_k=1²ⁿ S_k²ⁿ k!

where Regions(2n) is the number of equivalence classes over 2n clocks each constrained to lie in the interval (0,1), and S_k²ⁿ 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 :-)

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.

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!

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.

Characteristic Formulae (continued)

In a previous post, I briefly discussed the notion of characteristic formula for a state in a labelled transition system using Hennessy-Milner logic (HML) as the underlying property specification language. In light of its beautiful connection with bisimilarity, HML and its variations are prime candidates for logics in which to express characteristic properties for bisimulation-like relations. However, there are other options.

A classic result on characteristic formulae was obtained in the paper

Browne, M. C.; Clarke, E. M.; Grümberg, O. Characterizing finite Kripke structures in propositional temporal logic. Theoret. Comput. Sci. 59 (1988), no. 1-2, pp. 115-131.

The above paper shows that for any finite Kripke structure, i.e., a labelled transition graph with an initial state, it is possible to construct a Computation Tree Logic formula uniquely characterizing that finite Kripke structure. Browne, Clarke and Grümberg call the notion of equivalence matching "logical equivalence wrt CTL" E-equivalence. Two states are said to be E-equivalent if they have the same labelling of atomic propositions, and transitions to other states preserve the E-equivalence. (Surprise, surprise! This is just bisimilarity for Kripke structures.) It turns out that, modulo E-equivalence, finite Kripke structures are characterized by CTL formulae containing the "next-time" operator. (A formula of the form X φ, read "next φ", states that φ has to hold at the next state of the computation path.)

Another characteristic formula result is presented in that paper for an equivalence between states called S-equivalence (equivalence with respect to stuttering) . Two state sequences are said to correspond if each can be partitioned into finite blocks of identically labelled states such that each state of the ith block in one sequence is E-equivalent to each state in the ith block of the other sequence. Two states are said to be S-equivalent if, for each state sequence starting at one, there is a corresponding state sequence that starts at the other.

Theorem: S-equivalence classes of states in a finite Kripke structure are completely characterized by next-time-free CTL formulae.

The absence of the next-time operator is expected in light of the inability of S-equivalence to "count" the number of steps in a stuttering sequence. S-equivalence is closely related to van Glabbeek's and Weijland's branching bisimilarity. Logical characterizations of branching bisimilarity have been offered by De Nicola and Vaandrager in the paper:

R. De Nicola and F.W. Vaandrager. Three logics for branching bisimulation. Journal of the ACM, 42(2):458-487, 1995.

Kucera and Schnoebelen have presented a refinement of the above classic theorem by Browne, Clarke and Grümberg in the paper

A. Kucera and Ph. Schnoebelen. A general approach to comparing infinite-state systems with their finite-state specifications. Theor. Comput. Sci. 358(2-3): 315-333 (2006).

In a follow-up post, I'll try to wind up this brief three-part discussion of characteristic formulae by mentioning a couple of results on characteristic formulae for timed automata.

Bulletin of the EATCS, October 2006

The October 2006 issue of the Bulletin of the EATCS is now available on line. This 90th volume of the Bulletin marks an important date in the life of this publication in that it is the first volume that is available freely on the web from the moment of its publication. This is a one year open access experiment that I hope will be continued in the future. If you have not done so already, I warmly encourage you to become a member of the EATCS, also to support the open distribution of the Bulletin.

I firmly believe that having the Bulletin open access will further increase its quality and impact, turning it into an even more useful and widely read publication than it already is. Thanks to Vladimiro Sassone for his great editorial work on the Bulletin.

This issue of the Bulletin has at least two papers of direct interest to concurrency theorists (see the concurrency column and the programming languages column). I also enjoyed reading Leonid Libkin's contribution to the logic in computer science column.

Support the Bulletin, an open access publication in theoretical computer science, by, amongst other things, becoming a member of the EATCS and publishing articles in the Bulletin. Feel free to contact me if you'd like to write a piece for the concurrency column.

Characteristic Formulae

A piece of classic concurrency theory that is perhaps not so well known as it deserves to be concerns the characterization of the equivalence class of a process p (modulo a suitable notion of behavioural equivalence) by means of a single formula F(p) in a logic. This means that, no matter what process q we consider, q is equivalent to p iff it satisfies the formula F(p). The formula F(p), when it exists, is usually referred to as the characteristic formula of p (modulo the chosen notion of equivalence). Of course, the formula F(p) is unique up to logical equivalence, and that's why we allow ourselves the liberty to talk about the characteristic formula for p.

Why is this notion interesting at all? A classic result in the theory of concurrency is the characterization theorem of bisimulation equivalence in terms of Hennessy-Milner logic (HML) due to Matthew Hennessy and Robin Milner. (See this paper.) This theorem states that two bisimilar processes satisfy the same formulae in Hennessy-Milner logic, and if the processes satisfy a technical "image finiteness condition", then they are also bisimilar when they satisfy the same formulae in the logic. This means that, for bisimilarity and HML, logical equivalence coincides with behavioural equivalence, and that whenever two processes are not equivalent, then we can always find a formula in HML that witnesses a reason why they are not. This distinguishing formula is useful for debugging purposes, and can be algorithmically constructed for finite processes. (Algorithms for computing such distinguishing formulae for strong and weak bisimilarity are implemented in tools like the Edinburgh Concurrency Workbench.)

The characterization theorem of Hennessy and Milner is, however, less useful if we are interested in using it directly to establish when two processes are behaviourally equivalent using the logic. Indeed, that theorem seems to indicate that to show that two processes are equivalent we need to check that they satisfy the same formulae expressible in the logic, and there are countably many such formulae, even modulo logical equivalence. Isn't it possible to find a single formula that characterizes the equivalence of a process p?

To the best of my knowledge, this natural question was first addressed by Susanne Graf and Joseph Sifakis in their paper

Susanne Graf and Joseph Sifakis. A modal characterization of observational congruence on finite terms of CCS. Inform. and Control, 60 (1986), no. 1-3, pp. 125--145.

In that paper, they offered a translation from recursion-free terms of Milner's CCS into formulas of a modal language representing their equivalence class with respect to observational congruence.

Can one characterize the equivalence class of an arbitrary finite process---for instance one described in the regular fragment of CCS---up to bisimilarity using HML? The answer is negative because each formula in that logic can only describe a finite fragment of the initial behaviour of a process. (The "sight" of a formula is limited by the maximum nesting of modal operators occurring in it.)

Consider, for instance, the automaton over set of labels {a,b} with only one state p and a self-loop edge labelled a. The characteristic formula for p modulo bisimulation should state the following properties, which together completely characterize the behavior of p.

1. Process p affords an a-labelled transition leading to itself (that is, to a process that is bisimilar to p).
   
2. No matter how p makes an a-labelled transition, it always ends up in a state that is bisimilar to p.
3. Process p affords only a-labelled transitions.

If we let F(p) stand for the characteristic formula for p, then we can express the above properties in HML by means of the following recursively defined formula:

F(p) = diamond(a) F(p) AND [a]F(p) AND [b] False,

where I write diamond(a) for the a-labelled may modality in HML to prevent the blogging software from interpreting the standard notation as a HTML tag :-)

The right-hand side of the above formula determines a monotonic endofunction over the collection of sets of processes. The famous Knaster-Tarski fixed-point theorem yields a complete lattice of fixed-points for that function. It turns out that the largest fixed-point is the collection of all processes that are bisimilar to p. So, we can give characteristic formulae modulo bisimulation for states of finite labelled transition systems using HML enriched with a facility for the recursive definition of formulae, where recursively defined formulae are interpreted using largest fixed-points.

I believe that this characteristic formula construction was first noticed in the relatively unknown MSc thesis

Anna Ingolfsdottir, Jens Christian Godskesen and Michael Zeeberg. Fra Hennessy-Milner Logik til CCS-Processer. Department of Computer Science, Aalborg University, 1987

The thesis, supervised by Kim G. Larsen, was unfortunately encrypted in Danish, and this is one of the reasons why it is not as well known as it deserves to be. Some of ideas and technical developments from that work then appeared in the paper

Bernhard Steffen, Anna Ingolfsdottir: Characteristic Formulae for Processes with Divergence Inf. Comput. 110(1): 149-163 (1994),

which is by now the standard reference for the development of characteristic formulae for bisimulation-like behavioural relations over finite processes.

New Rector at Reykjavík University

The new rector of Reykjavík University was suddenly announced at 15:30 today by the chairman of the Board of Directors, Bjarni Ármannsson. The new rector is another woman, Svava Grönfeldt, who was the deputy of the CEO of Actavis. (See also her brief CV at the University of Iceland, courtesy of MohammadReza Mousavi.) She is also the author of Service Leadership: The Quest for Competitive Advantage with Judith B. (Banks) Strother. (Check the price!)

I will refrain from passing judgement on this choice until I see her in action. One word about the selection process, though. One of our contacts at Columbia University wrote to us saying:

First, most established American universities would announce a Search Committee to search for a new president. The Search Committee would typically comprise members of the board of directors, faculty, and even a staff member and student. Second, once a Search Committee was in place, a formal announcement would be made, with a deadline for applications and nominations. The principal publication that most universities--American or European--use to make these announcements is The Chronicle of Higher Education and sometimes even The New York Times education employment section. The Search Committee would meet to review applications and nominations and typically will select between 7 and 10 potential candidates for initial interviews. Following that, finalists, perhaps 3 individuals, would be interviewed in-depth and even asked to write a statement of their vision for the university. The selection of a final candidate is usually a consensus process.

Whatever process they chose, it was nothing like this, and the decision was not a consensus one. I hope it was a good one, especially because Reykjavík University is at a watershed, and a clear message has to be sent out as to whether the university wants to be what the Americans call a "research university" or some kind of teaching and service institution. However, I can already say that I did not like hearing the chairman of the Board of Directors talk about the university as an "educational company". I might be old fashioned, but a university is not a firm, and has very different purposes from a company.

Fingers crossed.

Predicting the Future

Last Friday, I read this article on La Repubblica, an Italian newspaper. The article discusses the special issue of the New Scientist that marks its 50th birthday. For this special issue, the New Scientist asked about 70 "brilliant minds" (their words) to take a peek at their crystal balls, and predict what science will have brought us by the year 2056.

A few well-known scientists talk about mathematics and computing. In fact, even one of the mathematics contributions focus on computer science! Tim Gowers' prediction discusses the P versus NP problem. He writes:

There are about half a dozen problems that almost all mathematicians agree are supremely important. One that I particularly like is the "P = NP" problem. ....

This problem gets to the heart of mathematics, because mathematical research itself has the property I have described: it seems to be easier to check that a proof is correct than to discover it in the first place. Therefore, if we found a solution to the P = NP problem it would profoundly affect our understanding of mathematics, and would rank alongside the famous undecidability results of Kurt Gödel and Alan Turing.

Thanks for the further publicity Timothy!

As for Gregory Chaitin, he went on record as saying that:

In my own field, I hope the current desiccated, formal approach has died out and people are more adventurous and creative.

I cannot believe that this statement will win him many friends :-) I, for one, am overawed to live in a research world which is full of very creative people. Sure, the heights of "creativity" are the realm of a chosen few, but one should never underestimate the importance of contributing small bricks of knowledge to the scientific enterprise. If everybody just looked for the next quantum leap in a field all of the time, the result will probably be stagnation.

I'll try to get hold of a copy of that number of the New Scientist.

On a local note, I had my own personal peek at my crystal ball last October, when I forecast that the rector of Reykjavík University will be chosen as one of the candidates to run for parliament at the next Icelandic elections. It did not take special powers of predictions to come to that conclusion. I am eagerly waiting to see who the next rector will be. Above all, I hope that the new rector will be "research friendly".

Spinoza

Last September I finished reading the book Betraying Spinoza: The Renegade Jew Who Gave us Modernity by Rebecca Goldstein. Reading that book brought back memories of my high school days, when I was taking philosophy classes and my teacher---a grey-haired, fine man by the name of Angelo Giordano I remember fondly---used to tell us about Baruch Spinoza's Ethics. I also recalled that, when I was a visiting researcher at INRIA-Sophia Antipolis in 1991, Gérard Boudol once told me that the "Dutch are more Cartesian than us French". (I hope I am quoting him correctly after all these years :-))

Reading Goldstein's warm account of Spinoza's philosophy and of his social and intellectual environment made me think that Spinoza's thought really has had a deep influence on the Dutch way of thinking (whatever that may be), and might indeed be one of the sources of the rationality that inbues Dutch society.

As Spinoza hints at in his writings, for every fact that is true, there is a reason why it is true. Since there are no arbitrary aspects of reality, logic itself must explain the world. In fact, logic itself is the world, which is just the collection of logical implications that make Nature.

Spinoza wrote:

"Thus in life it is before all things useful to perfect the understanding, or reason, as far as we can, and in this alone man's highest happiness, or blessedness, consists...."

I do not know whether I feel like endorsing Spinoza's vision completely, but I certainly feel that the intellectual process of beholding his vision of the world is an enriching one.

The closing words of Goldstein's book are a fitting climax to a well-written volume that I recommend heartily:

"The world has been transformed (though not enough) by a long and complicated chain of causes and effects that reaches back to Spinoza's choice to think out the world for himself."

I cannot help but feeling that the exercise of "thinking our way toward radical objectivity" would be a useful exercise for many of our leaders today.

You can also listen to a podcast interview with Rebecca Goldstein on the Nextbook website. Enjoy.

You might also wish to check out Rebecca Goldstein's other books. In particular, the novel The Mind-Body Problem is a favourite of mine. Readers of this blog will also enjoy the well-written, but at times somewhat flawed, Incompleteness: The Proof and Paradox of Kurt Gödel.

The Number of Labelled Trees over n Nodes

Yesterday, my colleague Anders Claesson, from the combinatorics group at Reykjavík University, gave a very good talk at the Icelandic Mathematical Society entitled "The Art of Bijective Proofs and the Science of Generating Functions". During the talk, Anders used as a running example a theorem of Cayley's to the effect that the number of labelled trees over n nodes is n^n-2.

Anders presented a bijective proof of this counting result due to André Joyal. (Concurrency theory buffs will recall that Joyal, together with Mogens Nielsen and Glynn Winskel, was one of the authors of the famous paper Bisimulations from Open Maps. Anders tells me that Joyal is also the father of the theory of combinatorial species.)

The proof is truly beautiful, and establishes a bijection between doubly rooted trees over {1,...,n}, and functional digraphs over that set. (A digraph is functional if the out-degree of each of its nodes is 1.) I encourage all of you to have a look at it.

Anders then showed how to obtain a proof of Cayley's theorem using the very general machinery of generating functions. (See this freely available book.) I must admit that I find the latter proof a little "magical", but this is due to my ignorance of the machinery of formal power series, generating functions and Lagrange inversion :-)

Addendum 18/11/2006: I have noticed that the classic textbook A Course in Combinatorics (2nd Edition) by J. H. van Lint and R. M. Wilson presents three different proofs of Cayley's theorem. (I think that the book offers five proofs of that result overall.)

As reading on generating functions, Anders recommends the draft book Analytic Combinatorics by Philippe Flajolet and Robert Sedgewick even more than Herbert Wilf's book.

Advice from David Patterson

A while back, I stumbled the following advice for new CS professors by David Patterson. (In case you don't know him, David Patterson led the design and implementation of RISC I, likely the first VLSI Reduced Instruction Set Computer, and was a leader, along with Randy Katz, of the Redundant Arrays of Inexpensive Disks project (or RAID), which led to reliable storage systems from many companies. He has been chair of the CS division at Berkeley, the ACM SIG in computer architecture, and the Computing Research Association, was the former president of the ACM.)

Patterson's advice is crystallized into the following Patterson Rules for increasing productivity at work, and reducing the frustration that ensues from coming in earlier, staying later, and getting less work done.

Use startup funds/personal funds to have office at home as nice as office nice desk/chair, fast modem (>=ISDN), printer, big screen, ...

Determine time of day most creative/effective: early morning, after 6PM, ...?

Work at home alone during those time slots

Do creative work uninterrupted at most creative time

Be sure to be at school from lunch (social) and afternoon (lectures, student/colleague dropin, seminars ...)

Other pieces of advice from him include the following nuggets.

Learn to say: NO! (but in a very polite way)

always think about it overnight, ask trusted friend before you say yes
(saying no lets you say yes later)

Make daily, weekly, semester to do lists

Find ways to keep a secretary/assistant busy: travel, fill out grade forms, schedule, ...

Read email <= once a day (when less productive)

Circadian rhythms: 20 minute nap at about 3PM adds > 1 hour of productivity in evening

Travel is #1 time synch; budget it appropriately

I feel that I fare embarrassingly badly on all of these accounts, but I do make daily, weekly, semester to do lists---which have a tendency to grow, rather than shrink, as time progresses---, and I am at school essentially every day. (Can you hear the sound of the barrel being scraped?) Some of those items do not apply to me at all. (Startup funds/personal funds? Secretary? Budgeting travel?) And, as for reading email <= once a day, well probably I should give it a try, but, as a friend of mine used to say, "The spirit is strong, but the flesh is weak."

Do the Patterson rules apply to your work practices?

Workshop on Emerging Trends in Concurrency Theory

The colloquium Emerging Trends in Concurrency Theory will be held at LIX, École Polytechnique de Paris, during 13-15 of November 2006. The colloquium is organized by Catuscia Palamidessi and Frank D. Valencia, and will be held under the auspices of Working Group 1.8 on Concurrency Theory of IFIP TC1. The guest of honor will be Turing Award winner Robin Milner, who was awarded one of the prestigious Blaise Pascal International research chairs to visit LIX for the 2006-2007 academic year.

The event will have well over 10o participants, and has a programme of talks to whet anybody's appetite. I am really sorry to have to miss this event, which clashes with the exams for our courses in Reykjavík---a rather mundane reason for having to miss what will be a great event.

Fortunately, Wan (Fokkink), the co-chair of WG1.8, will be there, you will be able to discuss with him matters related to the proposal to hold a WG workshop at CONCUR 2007.

It would be great if one or more of the participants could report on the workshop using the blog. All you need to do is to email me your report(s), and I'll take care of posting them on this blog.

I, for one, would be happy to read about yet another great event I am missing.

Book off to the Publisher

Lester Burnham: Remember those Posters that said, today is the first day of the rest of your life? Well that's true with everyday except one, the day you die.

I have just posted the final manuscript of the book "Reactive Systems: Modelling, Specification and Verification", co-authored with Anna Ingolfsdottir, Kim G. Larsen and Jiri Srba, off to Cambridge University Press.

We'll maintain a web site for the book, that will be published in the spring 2007. (At the moment it is empty, sorry!) On the web site, an instructor will find suggested schedules for his/her courses, exercises that can be used to supplement those in the textbook, links to other useful teaching resources that we will make available on the web, further suggestions for student projects and electronic slides that can be used for the lectures. We'll also make available CWB and Uppaal models for all of the proposed projects. Students will have access to the solutions for the mandatory and strongly recommended exercises in the book.

For the moment, you can read the preface, and have a look at the table of contents here. Then, tell your library to buy copies in due course, make a note to buy your own copy when the book is out, and consider it for course use :-)

I must say that it really feels like "the first day of the rest of my life", hence the quote from American Beauty. Now it is time to catch up with several outstanding other projects, hoping that my co-workers will still want to work with me at this stage.

Brief News from the Math World

The December issue of the Notices of the AMS is out. It is not one of the most interesting I have seen, but it has a report on the International Congress of Mathematicians 2006 by Allyn Jackson, and a report on the 2006 Fulkerson Prize.

Terence Tao continues to collect prizes and awards. He has also landed the SASTRA Ramanujan Prize.

Anders Claesson, from the combinatorics group at Reykjavík University, has pointed out the following two math blogs to me: Mathematics under the Microscope and A Neighbourhood of Infinity. Maybe some of you might enjoy looking at them.

Bill Gasarch has a guest post on the Complexity Weblog on the topic of private information retrieval. He mentions the following papers:

An Ω(n^1/3) lower bound for bilinear group based Private Information Retrieval by Alexander Razborov and Sergey Yekhanin, FOCS 2006.

New Locally Decodable Codes and Private Information Retrieval Schemes, by Sergey Yekhanin

Apparently, the former paper models 2-Database-Private Information Retrieval via Latin Squares and then uses representation theory of finite groups to push through the lower bound. The latter uses Mersenne primes.

I have not looked at the papers, but that sounds like yet another application of very hard maths in volume A TCS.

Process Algebra on Lambda the Ultimate

MohammadReza Mousavi pointed out to me this post on Lambda the Ultimate (the programming languages weblog), which will please process calculi buffs. (Thanks Mohammad!) That post points out some, more or less recent, work on process calculi for transactions.

The references provided in that post are to the point. As Mohammad pointed out to me, relevant process algebraic work along those lines may also be found in the paper

H.M.A. van Beek. An algebraic approach to transactional processes. CS-Report 02/18, Department of Mathematics and Computing Science, Technische Universiteit Eindhoven, December 2002. Harm's Ph.D. thesis contains that report as a chapter (Chapter 8).

As far as I know, the earliest studies of "atomic transactions" within the field of process calculi were presented by Gérard Boudol and Ilaria Castellani in two papers that appeared in the late 1980s:

• Gérard Boudol, Atomic actions, in EATCS Bulletin Vol. 38 (1989), 136-144.
  [Abstract, PostScript, .ps.gz]
• Gérard Boudol and Ilaria Castellani, Concurrency and atomicity, in Theoretical Computer Science Vol. 59 (1988), 25-84.
  [Abstract]

It would be good if younger researchers rediscovered those two papers. I read them at the early stages of my "career", and I warmly recommend them.

I encourage my readers to post further reading suggestions on the topic of process calculi for atomic transactions. As Charles Stewart writes on Lambda the Ultimate, this topic will repay a closer look.

Rock and TCS

Janos Simon and Luca Trevisan are reporting from FOCS 2006 (Berkeley, CA)---a conference from which our community is, alas, conspicuously absent---on the Complexity Blog and on In Theory, respectively. Their live reports make for very interesting reading. I encourage you to read Janos's report on the FOCS Business Meeting to get an idea of the state of funding for TCS in the US.

One of the events at FOCS was a concert by Lady X and The Positive Eigenvalues, a band that includes Christos Papadimitriou on keyboards. As Luca Trevisan notes in his blog, apart from Christos Papadimitriou, Mike Jordan, and guest star Anna Karlin, that band includes "a number of other Berkeleites (for some reason, all Italians)."

This is not the first ever example of a rock concert held at a major theory conference. I recall that Dexter Kozen and his band performed at the Monterey aquarium during LICS 1989. Amongst others, they offered (T)CS renditions of songs by the Ramones (I wanna be promoted) and the Dead Kennedys (Categories über alles). At the time I collected a leaflet with the text of the songs Dexter's band played, but I lost it. Here is a scanned version of the leaflet, courtesy of Don Sannella. Enjoy it!

Report on NWPT06

Anna and I organized the 18th Nordic Workshop on Programming Theory from Wednesday, 18 October, till Friday, 20 October, at Reykjavík University. The workshop was held under the auspices of the Icelandic Centre of Excellence in Theoretical Computer Science (ICE-TCS) and of the IFIP TC1 Working Group 1.8 on Concurrency Theory, and was partly sponsored by Reykjavík University.

The NWPT series of annual workshops is a forum bringing together programming theorists from the Nordic and Baltic countries (but also elsewhere). The previous workshops were held in Uppsala (1989, 1999 and 2004), Aalborg (1990), Gothenburg (1991 and 1995), Bergen (1992 and 2000), Turku (1993, 1998, and 2003), Aarhus (1994), Oslo (1996), Tallinn (1997 and 2002), Lyngby (2001), and Copenhagen (2005). Thus, this was the first ever NWPT workshop held in Iceland.

The event was attended by 45 scientists from the Nordic countries, but participants came from as far as south as Italy :-) In addition, several local MSc and advanced BSc students enjoyed some of the presentations, which were of consistently high quality. (Here are a couple of quick observations on the geographical distribution of the participants.

1. There were no contributed talks from Sweden, and David Sands was therefore the only representative of Swedish computer science at the workshop.
   
2. There was a good number of participants from Germany.)
   

The scientific programme consisted of four invited presentations and 26 contributed ones. The four invited talkes were:

• Gerd Behrmann, Aalborg University. How to become a successful tool builder - the dirty tricks
• Matthew Hennessy, University of Sussex. Some Remarks on Testing Probabilistic Processes.
• Hanne Riis Nielson, DTU. Analysis of Process Interactions
• David Sands, Chalmers University of Technology and University of Göteborg. Specifying and Verifying Dynamic Information Flow Properties

Hanne Riis Nielson gave the workshop the best of starts by offering an excellent overview of her work on using static analysis techniques to validate models of computational scenarios vis-a-vis the actual "reality" that is being modelled. As a motivating question she asked: "How can we be sure that process calculi descriptions of, say, biological processes/pathways are faithful to reality?" At the end of her clear and well-paced lecture, the audience was left feeling that static analysis can indeed help in addressing the all important motivating question underlying her presentation.

Gerd Behrmann's talk offered a thought provoking and stimulating analysis of the role of tool development in algorithmic verification. Gerd gave the audience many good reasons for building tools, but also pointed out that empirical studies in this field are often of questionable quality, with results that are not reproducible and unfounded conclusions. He pledged for this situation to be improved if tool building is to become a respected scientific activity.

Not surprinsingly, Gerd's talk gave rise to a lively discussion (both during and after the presentation). Flemming Nielson made some very interesting remarks after the talk, explaining how a tool developer can obtain credit for his/her work at his institution (DTU), e.g., by means of innovation schemes and the writing of books about the lessons learned during tool building. He also defended, in case there was any need to do so, the hard work of theorists, and uttered the following eminently quotable sentence:

"The purpose of theory is insight, not theorems!"

Matthew Hennessy delivered a talk on testing probabilistic processes that presented work he did while visiting NICTA in Australia. This was a one hour version of a shorter talk he had delivered earlier at the symposium in honour of Gordon Plotkin's sixtieth birthday. Matthew gave a typically well polished lecture, which managed to present a lot of technical work without ever giving his audience the feeling of being overwhelmed by the mathematics. I am looking forward to reading the paper on which the talk was based.

The last invited talk for the workshop was delivered by David Sands. Static verification of secure information flow has been a popular theme in recent programming language research, but the information flow policies considered are based on a static view of security levels. In his talk, Dave provided a road map of the main directions of current research, and introduced a simple mechanism, called flow locks, for specifying dynamic information flow policies, and a type-and-effect system for statically verifying flow lock policies. The talk was based on joint work with Niklas Broberg.

The 26 contributed talks were mostly of excellent quality, presenting work at different stages of development; some of it was definitely in progress, some other was "in infancy", and some was instead very mature. This is what a workshop should be like!

Some photos from the workshop, courtesy of MohammadReza Mousavi, are available.

The 2007 edition of the workshop will be held in Oslo, Norway. I trust that it'll be just as successful as we felt this one was. Good luck to Olaf Owe, who will take over the mantle of organizer from Anna and me.

Double Blind Refereeing

A colleague of ours was discussing the following dilemma with Anna today.

A computer scientist is preparing a submission to a conference in Language Technology that has double blind refereeing. He is just about the only person in the world doing tagging for Icelandic. Should he cite his own work in the submission?

This colleague realized that, by citing his own work, he would make his identity known to the reviewers, and was worried that this might influence them. We told him that a reviewer would be able to infer the name of the author from the paper anyway because he is really the only possible author of that paper. (In general, in TCS the set of possible authors of a paper is not very large, and, using tell-tale stylistic or notational usages, a reviewer of an authorless paper is often able to determine the author(s) of a paper with a rather large degree of accuracy.)

Consider also the following catch-22 situation. A reviewer of the paper by our colleague could reject it because the anonymous author X is neither citing the closely related work of author X nor comparing his work with that of author X! It would be just great to have one's paper rejected for not citing one's own work, wouldn't it?

I have never believed in double blind refereeing. This story has reinforced my lack of belief in this system.

Mini Course on Model Checking Real-time Systems in Reykjavík

As part of the ICE-TCS activities held during the coming week, which will be mostly devoted to the 18th Nordic Workshop on Programming Theory, we shall host a mini course Model Checking for Real-time Systems held by Kim G. Larsen. The course will be held on Monday, 16 October, at Reykjavík University. (In case you are interested in looking at some text in Icelandic, you can see the announcement that will appear tomorrow in one of the local newspapers.)

The course will be followed by an exercise session on Tuesday, 17 October, held by Alexandre David (Aalborg University). Feel free to drop by, if you happen to be in Reykjavík for the Iceland Airwaves music festival.

Teaching Reductions

This semester I am teaching Introduction to the Theory of Computation at Reykjavík University, a course taken by third year BSc students and MSc students alike. I like teaching this course (based on Michael Sipser's book bearing the same title) very much, and I try to convey to the students the intellectual excitement I feel about the theory of automata, computability and complexity.

After last Wednesday's lecture, however, I was totally drained of energy. Why? During Tuesday's lecture I introduced the concept of reduction, and used it to prove the undecidability of the emptiness, equality and regularity problem for Turing machines. The day after I started the lecture with a warm-up, peer instruction session asking the students to argue that it is undecidable whether a Turing machine accepts the language {Alan, Turing}. The reaction was summarized by the blank stare I got from most of my audience Even when we worked through the solution together, I still had the feeling that many of them were not comfortable with the notion of reduction. I had to work very hard to try and clarify it as best as I could, and it is not clear to me yet whether I succeeded.

Looking back to my previous experiences teaching this course, or variations on it, in Aalborg, this is not surprising. The notion of reduction is the bread-and-butter of computability and complexity, and one of the cornerstones of algorithmic thinking. Having mastered it, the rest of the material in my introductory courses becomes, I would venture to say, relatively easy. It is one of those powerful concepts that opens up new vistas, and, despite being very natural and ubiquitous in the theory of computing, requires some intellectual maturity to be understood fully.

A typical pitfall I have experienced over the years is that many students think that the pre-processing algorithm converting, say, the question "Does a Turing machine M accept the string w?" into an equivalent one of the form "Does the Turing machine M' accept the empty language?" actually runs M on input w when, while producing the code for M', it writes the line of code

Run M on input w.

Here I usually use the analogy with a compiler to try and dispel their doubts. (Basically, I tell them to view the pre-processing algorithm implementing the reduction as a compiler between inputs to two different problems. The pre-processing algorithm outputs a piece of code, but never runs it.) It is not up to me to say whether this works, but it seems to me that most of the students "crack the code", and start thinking naturally in terms of reductions between algorithmic problems.

Is it just my personal experience, or are reductions hard to grasp for many of our students? I'd be happy to hear how you go about teaching reductions in your classes on the theory of computation, and what analogies/metaphors you use to help your students understand such a fundamental notion.

Turing in the Notices of the AMS

The November issue of the Notices of the AMS is entirely devoted to Alan Turing. (I first learned about this issue via Luca Trevisan's blog in theory.) I have only had time to skip through Solomon Feferman's piece on Turing's thesis (his PhD thesis, not the Church-Turing thesis), but the whole issue looks very interesting.

I have already recommended it to the students who are taking my theory of computation course in Reykjavík.

Enjoy it!

Paul Halmos, 1914-2006

I just saw a sad news item on the AMS web site. Paul Halmos passed away on Monday, 2 October. He was a master of mathematical exposition, both in writing and speaking, and taught many writers in the mathematical sciences how to write.

A few years ago, I had the pleasure of borrowing his "mathobiography" I Want to Be a Mathematician from Steffen Lauritzen in Aalborg, and enjoyed it immensely. I plan to buy a copy for my bookshelves at some point.

Bas Luttik has keeps telling me to read Halmos's expository work on algebraic logic. I keep postponing doing so, but maybe now it is time to start. At least after some pencil sharpening has taken place :-)

Let me end with a quotation from Halmos's mathobiography I like:

"I love to do research, I want to do research, I have to do research, and I hate to sit down and begin to do research---I always try to put it off just as long as I can.
....Isn't there something I can (must?) do first? Shouldn't I sharpen my pencils perhaps?"

- --Paul Halmos, I Want to be a Mathematician

These days I sharpen my pencils a lot, alas.

N is a Number

Yesterday, ICE-TCS hosted its first movie event with the projection of the documentary film N is a Number: A Portrait of Paul Erdös by George Csicsery. I bought the DVD of this award winning documentary using my Springer author discount, and, rather than watching it at home, I decided to share it with my colleagues at Reykjavík University. I also hoped that some of our students would show up to watch the documentary. (Every opportunity is good to entice students to study TCS! Unfortunately, however, no student took the bait and joined us :-()

The documentary is good and I recommend it, even though it does not hold many surprises for people who have read the popular books on Paul Erdös. However, watching Paul Erdös strut his skills on the dias before diving into the mathematics was an enjoyable experience for somebody like me who never had the chance of seeing him "live".

I wonder whether he is still managing to keep the SF's score low wherever he may be now.

Addendum: The Erdös numbers of the members of ICE-TCS are here.

MohammadReza Mousavi in Reykjavík

Albeit belatedly, due to some last minute bureacratic hassles arising from the lack of experience of the staff at a young university like Reykjavík University, MohammadReza Mousavi has joined our little concurrency theory group at Reykjavík University. Anna and I are understandably thrilled at having him here. Mohammad will have a joint position between Reykavík University and TU Eindhoven.

The 'group' has doubled in size since August this year, with the arrival of Silvio Capobianco (a mathematician from Rome) and Mohammad. Their arrival has also strengthened ICE-TCS considerably, and their presence is giving Anna and me a good intellectual environment to work in. Now it's up to us to make the most of this opportunity, and I hope that we'll be able to capitalize on their scientific strength. If we don't, then it's going to be solely our fault.

The problems we encountered in getting a visa for Mohammad at the last minute seem to have some positive consequences. Together with the Icelandic research council, we are pressing the politicians here to establish a fast-track for researchers seeking visas and work permits to come and work in Iceland. Having a "researcher visa" procedure might make it more attractive for scientists to come and work here in the North Atlantic, at times when access to other countries is becoming more and more difficult. I'll keep you posted on the developments.

New Perspectives on Fairness

I have just posted the concurrency column for the October 2006 installement of the Bulletin of the EATCS. The October column is a lovely piece entitled New Perspectives on Fairness by Daniele Varacca and Hagen Voelzer.

Fairness is an important concept that appears repeatedly in various forms in different areas of computer science, and plays a crucial role in the semantics and verification of reactive systems. Entire books are devoted to the notion of fairness---see, for instance, the monograph by Nissim Francez published in 1986---, and researchers in our community have painstakingly developed a taxonomy of various fairness properties that appear in the literature, such as unconditional fairness, weak fairness, strong fairness, and so on. This research is definitely important in light of the plethora of notions of fairness that have been proposed and studied in the literature.

But when is a temporal property expressing a fairness requirement? The authors of this column have recently developed a very satisfying answer to this fundamental question by offering three equivalent characterizations of ``fairness properties'' in the setting of linear-time temporal logic: a language-theoretic, a topological, and a game-theoretic characterization. This survey discusses these recent results in a very accessible fashion, and provides also a beautiful link between the study of fairness and classic probability theory.

I trust that you will enjoy reading this piece by Daniele and Hagen as much as I did. It is not often that one sees notions and results from several areas of mathematics and computer science combine so well to offer a formalization of a concept that confirms our intuition about it.

MacArthur Genius Awards for 2006

Lance Fortnow has a post on the latest batch of "genius awards" by the Mac Arthur foundation. Awards in disciplines of potential interest to the readers of this blog are to

• Luis von Ahn.
  
• Terence Tao.
• Claire Tomlin. The announcement makes very interesting reading for a concurrency theorist, and for anyone interested in formal verification:
  

  Much of Tomlin's research concentrates on aeronautical applications of hybrid systems research, particularly aircraft flight control and air traffic conflict resolution. As the number of variables increases and their interactions become more complex, it becomes ever more difficult to guarantee that systems will always be within safe limits. Tomlin has developed practical algorithms for determining when unsafe conditions may arise, and for establishing feedback control laws for a hybrid system guaranteed to remain within a safe subset of all reachable states.
  

In keeping with my previous jazz-related post, I am glad to see that John Zorn, one of my favourite musicians and prime mover behind Tzadik Records, is one of the recipients of the award. Check out his Masada series if you have not done so already.

Congratulations to the winners of the awards!

Jazz meets Process Algebra

Bas Luttik's band, the Residence Jazz Sextet, now has a web site, and a CD. I heard a demo version of the CD, and it sounds good. On the band's web site, you can also listen to mp3 demos of the tracks on the CD. Enjoy it!

An Essay by Palamidessi and Valencia

Catuscia Palamidessi and Frank Valencia have written an essay on Languages for Concurrency, which will appear in the Programming Languages column of the Bulletin of the EATCS (edited by Ian Mackie (Kings College, London, UK) and David Sands (Göteborg, Sweden)). I enjoyed reading it myself---even though I hopefully knew the material it covers already---, and warmly recommend it.

This essay is a commendable example of `outreach activity´ from two very active members of the concurrency theory community. Let's give it to our students and colleagues from other areas of computer science to read, and let's try to sow the seeds of our research area in our departments. Something good is bound to come out of these kind of efforts. For the moment, thanks to Catuscia and Frank for offering a contribution in this direction.

New Award to Moshe Vardi

Moshe Vardi has been named as a co-recipient of the first LICS-test-of-time award for his paper An Automata-Theoretic Approach to Automatic Program Verification, co-authored with Pierre Wolper. Congratulations to Moshe and Pierre for yet another award!

See http://www2.informatik.hu-berlin.de/lics/#awards for a description of the award. I think that the idea to look back 20 years for the award is a good one, and look forward to seeing more awards in areas of logic related to concurrency theory and formal verification.

Experimental Blog for the IFIP WG on Concurrency Theory

Together with Wan Fokkink and Anna Ingolfsdottir, I recently set up a separate blog on concurrency theory. The aim of that blog is to serve as a dicussion forum for topics of interest to the members of IFIP WG1.8. I hope that the readers of this blog, if there are any, will contribute to the discussion threads that will be posted on the new blog.

PC Chair for FOSSACS 2008

FYI, the PC chair for FOSSACS 2008 will be Roberto Amadio. Sharpen your pencils and prepare good papers for that conference!

Gordon Plotkin is 60

On 7-8 September, LFCS, School of Informatics, University of Edinburgh, will host a symposium to celebrate Gordon Plotkin's 60th birthday. The detailed programme for that event lists a series of stellar speakers, and the list of participants is truly impressive.

This is really good to see. Gordon is one of the veritable giants in TCS, and he has had outstanding students and collaborators over the years. His contributions to the study of the semantics of programming languages (be it denotational, logical or operational) and to its mathematical underpinnings are well known, so I'll just limit myself to wishing Gordon a happy symposium.

What Are the Most Important Open Problems in Concurrency?

Let us assume that one can assess the healthiness of a research field, say concurrency theory, by looking at the most important open problems in that field. These open problems can be used to try and convince researchers in another area and students that the field of concurrency theory is "alive and kicking", and maybe entice a few of them to work within the field.

Based upon this thought experiment, wouldn't it be a good thing to have a repository of open problems that identify the present state of development in concurrency theory, and suggest directions for further research?

At some point in the past, I started putting together a list of open problems, but I have not really maintained it for a while. Will you help me revive this enterprise by sending me, or posting as a comment to this blog entry, a description of your favourite open problems in concurrency theory, together with links to partial solutions and pointers to the literature? This input of yours might even form the basis for a useful installment of the Concurrency Column in the Bulletin of the EATCS, and generate a lot of research in our field following what Luca Trevisan has called in this very informative blog entry the "Hungarian approach to mathematics": pose very difficult problems, and let deep results, connections between different areas of math, and applications, come out as byproducts of the search for a solution.

By the way, Luca Trevisan has a few very interesting posts related to Szemeredi's theorem and other results in additive combinatorics. (See this one, and the five blog entries on Szemeredi's theorem.) Those posts give an inkling of the level of mathematical sophistication that has been reached in TCS research from the volume A camp. Check them out!

A New Yorker Article on the Poincaré Conjecture

Yesterday I finished reading a rather long, but interesting article published in the New Yorker. The article, written by Sylvia Nasar (of Beautiful Mind fame) and David Gruber, describes some of the developments surrounding the proof of the Poincaré conjecture, has excerpts of an interview with Perelman, and offers us a glimpse of what happens behind the scenes of the mathematical arena. The former Fields medal winner and top-notch mathematician Shing-Tung Yau appears as the "villain" in the story.

I do not know if the content of the article is truly trustworthy, but it makes for some interesting, and at times arresting, reading. This excerpt, for one, tells the remarkable story of the recent publication of what could be a key paper in the story of the solution of the Poincaré conjecture:

On April 13th of this year, the thirty-one mathematicians on the editorial board of the Asian Journal of Mathematics received a brief e-mail from Yau and the journal’s co-editor informing them that they had three days to comment on a paper by Xi-Ping Zhu and Huai-Dong Cao titled “The Hamilton-Perelman Theory of Ricci Flow: The Poincaré and Geometrization Conjectures,” which Yau planned to publish in the journal. The e-mail did not include a copy of the paper, reports from referees, or an abstract. At least one board member asked to see the paper but was told that it was not available. On April 16th, Cao received a message from Yau telling him that the paper had been accepted by the A.J.M., and an abstract was posted on the journal’s Web site.

Quite a remarkable refereeing process for a paper proving one of the Millennium Problems of the Clay mathematical institute!

Italian TCS Presence at the ICM 2006

Today was a good day for Italian TCS at the International Congress of Mathematicians 2006. The inaugural talk in the section on Mathematical Aspects of Computer Science was delivered by Luca Trevisan (UC Berkeley). Luca's talk was based on the paper Pseudorandomness and Combinatorial Constructions.

Congratulations to Luca for being invited to deliver a talk at ICM 2006.

Question: How many Italian computer scientists have been invited speakers at the section on Mathematical Aspects of CS at the ICM so far?

I do not know the answer myself. Does any of my readers do?

Live Transmission from ICM 2006

The web pages for ICM 2006 point to this link for live trasmission of the sessions and recordings of previous sessions. Warning: I have not tried to view anything myself yet, so I hope this works :-)

One of yesterday's highlights for my family and close environment was Richard Stanley's invited plenary talk. Stanley is the "godfather of algebraic combinatorics", or so says Doron Zeilberger on his links page, and the former supervisor of Bridget Tenner (Kári's girlfriend) , and of Einar Steingrimsson, the head of the algebraic combinatorics research group at Reykjavik University.

For those of you who would like to read it, Stanley's paper for ICM 2006 is Increasing and decreasing subsequences and their variants (34 pages).

Fields and Nevanlinna Prizes

This is old news by now, but, in case you have not seen it already, at the opening ceremony of the 2006 International Congress of Mathematicians (ICM), four Fields Medals were awarded. The medalists are Andrei Okounkov, Grigory Perelman, Terence Tao, and Wendelin Werner. Perelman has apparently declined the award. At a press conference, John Ball (president of the IMU) said that Perelman will be recorded as having been awarded a Fields Medal but as having declined to accept it. Jon Kleinberg received the Nevanlinna Prize, and Kiyoshi Itô, who is 91, received the first-ever Gauss Prize. Congratulations to Jon, who also got a Mac Arthur fellowship in 2005. An AMS press release has more details about the six winners.

Luca Trevisan has "live commentary" from ICM 2006. Make sure you follow his lively blog reports! (For instance, look at his report on the laudationes for the prize winners.)

Today is a great day for TCS at ICM 2006. Avi Widgerson delivered his plenary talk "P, NP and mathematics: a computational complexity perspective", and brought one of the fundamental notions in Computer Science to the attention of a hord of mathematicians. I strongly advice all of you to read the beautiful paper he wrote for the occasion, and on which the talk is based. I look forward to reading Luca Trevisan's report on the talk.

Thanks Luca!

Addenda: BBC coverage, Guardian story, New York Times article.

I could not resist checking my distance from the 2006 Fields medal winners. According to the data on the AMS web site, my collaboration distance from all of the winners of the Fields medal is 6, apart from the one from W. Werner, which is 5. My Kleinberg distance is 4. Finally, my K. Ito number is infinite.

Scientifically speaking, my distance from each of these guys is infinite.

A Good Newpaper Article on Maths

Readers of this diary might enjoy looking at the article "Elusive Proof, Elusive Prover: A New Mathematical Mystery". This is an excellent example of coverage of mathematics in the press, and deals with the developments surrounding Perelman's proof of Poincaré’s conjecture.

This article is also very timely. The ICM 2006 kicks off tomorrow, and Richard Hamilton (Columbia University, New York, USA) will deliver a talk on the Poincaré conjecture at 17:15. As an Italian abroad, I am also proud to announce that Alfio Quarteroni (École Polytechnique Fédérale de Lausanne, Lausanne, Switzerland and Politecnico di Milano, Milan, Italy) will also deliver a plenary address tomorrow.

The section on Mathematical Aspects of Computer Science starts on August 26.

Colin Stirling in the Gödel Award Committee

I have heard from Mogens Nielsen that Colin Stirling has agreed to serve as one of the EATCS representatives in the Gödel award committee. This is great news for the concurrency theory community, and we should all be proud of Colin's nomination. (Colin is taking the place of P.L. Curien, whose term on the award committee ended this year, when he chaired the award committee.)

The Gödel Prize for outstanding papers in the area of theoretical computer science is sponsored jointly by the European Association for Theoretical Computer Science (EATCS) and the Special Interest Group on Algorithms and Computing Theory of the Association of Computing Machinery (ACM SIGACT). This award is presented annually, with the presentation taking place alternately at the International Colloquium on Automata, Languages, and Programming (ICALP) and ACM Symposium on the Theory of Computing (STOC).

As I have already written in earlier posts devoted to this prize, a look at the list of winners clearly indicates a bias towards SIGACT-friendly research. During his presentation at ICALP 2006, Curien explained that this is a somewhat natural outcome of the fact that the prize is awarded by a committee formed by three SIGACT representatives and three EATCS members. Now, unlike SIGACT, the EATCS is an organization representing the whole of TCS, and its representatives in the Gödel award committee cover the areas of logic and semantics, automata and formal languages and algorithms and complexity theory. When it comes down to voting, papers in algorithms and complexity are more likely to get four votes than those in, say, logic and semantics.

Is this a desirable state of affairs? I am not so sure myself, but I believe that the EATCS should continue being involved in the Gödel prize. Let me wish Colin good luck with his work in the committee. I hope that we'll make his job easier by nominating excellent papers in logic and semantics for the award. After all, isn't it a bit weird that so few Gödel prizes are being given for work done in logic?

Handwritten Slides, Course Notes and Hard Copies of Old Papers

Anna and I had to make some drastic decisions when packing our things in Aalborg. Some of these decisions involved the material stored in the boxes stored in the university cellar that housed the contents of our offices there. We had between 15 and 20 boxes full of books, handwritten slides for talks and courses, hard copies of technical reports and papers, photocopies of (parts of) books and reprints of our papers.

Not having time to sort things, we eventually threw everything away, apart from a few books that we really cared about.

Was that a good decision to take? Well, for a start, we had been packing our things in the house for about a week, and we were sick and tired of it. Disposing of the reprints of our papers was not a painful decision at all since most of the papers are available electronically. However, when we told Kim G. Larsen that we had got rid of our handwritten slides, notes and course folders he immediately said: "That was a stupid thing to do! I still use some of my old handwritten slides for courses and summer schools."

Looking back, it is true that we lost a part of our working life by disposing of those boxes. Some of those notes reported on work that was "in progress", and I feel that I'll never be able to reproduce them. (The person who wrote those notes is not here anymore, and will never come back.) Does this matter? The sad truth is that it probably does not. That work would have never been finished anyway, and, even if it did, it would not have been "important enough".

Would you have made the same choice as we in our situation? Think about it before your next move.

Fulkerson Prize 2006

The Fulkerson Prize is given by the Mathematical Programming Society every three years to up to three papers in discrete mathematics. The winners of the 2006 prizes are the papers:

• Primes in P, Manindra Agrawal, Neeraj Kayal and Nitin Saxena
• A polynomial-time approximation algorithm for the permanent of a matrix with nonnegative entries, Mark Jerrum, Alistair Sinclair and Eric Vigoda.
• Graph Minors. XX. Wagner's conjecture, Neil Robertson and Paul Seymour.

Note that Agrawal and his students have landed yet another prize for their paper after the Gödel Prize 2006 that was given to them at ICALP 2006. The third paper establishes, after work presented in twenty papers and spanning about 500 pages, the Robertson-Seymour Theorem, which has been hailed as a monumental result in graph theory and one of the deepest results in the whole of mathematics. The authors have a knack for settling long-standing conjectures in graph theory.

The winners of the Fields Medal and the Nevanlinna prize will be announced at ICM 2006 by the end of this month. I am very curious to see who will land the prizes, and whether Perelman will be awarded a Fields Medal for his work on the Poincare conjecture.

Mike Paterson's Secrets for Success

During the award ceremonies at ICALP 2006 in Venice, Mike Paterson, the recipient of the EATCS distinguished award for 2006, delivered a very witty talk in which he told the attendees his "secrets for success." Here is the short story for those amongst you who could not be in Venice to listen to Mike in person. (I apologize for any misrepresentation of Mike's message, and for being unable to match the wit and warmth in his presentation using this medium---or any other for what matters.)

Mike summarized the ingredients of his "success" as follows:

1. Start early!
2. Get lucky!
3. Hang out with smart people!
4. Enjoy what you do!
   

The first of these pieces of advice is probably the hardest to follow for many of us. What Mike meant was that at the beginning of a research field there are, I quote, "a lot of cherries ready for picking." These are problems whose solution is deemed to be important for the early development of the field and is not technically very hard. As a field matures, the open questions tend to get harder and harder, and the techniques that are brought to bear to their solutions are more and more sophisticated. Moreover, at the beginning of a research field, one can even try and steer the interests of the research community towards the problems one can actually solve.

The second point is that it does help to be in the "right place at the right time." A chat with the right person may open a lot of doors, and so can working with the right people and on a topic that is deemed to be hot at a given time. Mike gave some personal reminescences related to how he ended up working at MIT, and sharing an office, actually two offices, with Michael Fischer. Having said that, "Luck favours the prepared mind" (Pasteur), and so one should make one's own luck.

Having good collaborators is one of the most important factors in a research career. A look at our research landscape quickly reveals that more and more papers are multi-authored and are the result of a collaboration. I would recommend "hanging out with smart people" to any young researcher, no matter how smart he/she might be. There is so much to be learned in working with others!

Regarding the last point, Lance Fortnow wrote in this post that you must "Be sure to have fun doing your research because if you are not having fun you won't be successful and you can likely make more money doing something else that isn't fun." Judging from his presentations at ICALP, Mike Paterson is still having a lot of fun doing his research! Look at his recent work on the "overhang" problem with Uri Zwick to understand why. Uri Zwick is one of the "smart people" Mike likes to hang out with.

Mike's latest project is the Centre for Discrete Mathematics and its Applications. Check it out.

Thanks to Mike for setting such a good example for all of us to try and follow.

ICALP 2008

Last Tuesday, the EATCS general assembly held at ICALP 2006 in Venice has accepted the bid presented by Magnús M. Halldórssón on behalf of ICE-TCS to hold ICALP 2008 in Reykjavík. Anna, Magnús and I look forward to seeing you in Iceland in July 2008.

I'll try to report on a couple of interesting events at ICALP 2006 over the next few days. For the moment, I'll just say that Manindra Agrawal received the Gödel Prize 2006, and that Mike Paterson received the EATCS distinguished award. Mike's entertaining talk let us in on his "secrets for success." His presentation will need a separate post, even though I am pretty sure that you are already wondering what his secrets are :-)

ICALP Report

So Italy brought the Fifa World Cup 2006 home after 24 years. I am biased on this issue, so I won't comment on Italy's win. For an independent opinion, you might wish to check out this article from the Guardian. (Allow me to say, however, that, not surprisingly, I am glad Italy won the championship :-))

I am now at ICALP 2006, and will be attending the General Assembly in about 45 minutes. For the moment, I can give you a couple of possibly interesting news regarding the EATCS. First of all, the new president of the EATCS is going to be Giorgio Ausiello. Mogens Nielsen (the former president) and Paul Spirakis will act as vice-presidents. There are going to be some interesting developments in the role that the EATCS will play for the development of Theoretical Computer Science as a whole. A small, but I believe very important, first step is the free access experiment for the Bulletin of the EATCS, which will begin asap. This will make the Bulletin a more widely read, and I believe better quality, publication.

I'll keep you posted on other developments related to publications and EATCS prizes in due course. News regarding the location of ICALP 2008 will follow soon.

Off to ICALP in Venice

I am off to ICALP 2006 in Venice tomorrow, and hope to get to Venice in time to watch all of the World Cup final---even though watching the match will make me suffer as I always do when Italy are playing.

On Monday I'll attend the EATCS Council meeting, where I expect interesting discussions on whether the Bulletin should be freely available to all on the web, and the issue of EATCS prizes. My opinion, and one that I'll argue for at the meeting, is that the Bulletin should be freely available on the web in its entirety, just like the Notices of the AMS---whose electronic publication is supported by the members' dues. This will help us reach a wider audience, and further increase the visibility of TCS.

On Tuesday afternoon, during the EATCS general assembly, Magnus Halldorsson, Anna Ingolfsdottir and I will present a bid on behalf of ICE-TCS to host ICALP 2008 in Reykjavik, Iceland. If you are in Venice, make sure you attend the assembly and vote for us :-)

I'll try to report on these meetings and on the conference at a later time.

How We Should Not Behave

I encourage all of you to take a deep breath and read the comments to this post by Lance Fortnow. Reading also the comments to this one won't hurt. Then draw your own conclusions.

I'll refrain from further comments, but thanks to Boaz Barak and Luca Trevisan for their thoughtful contributions.