Tuesday, May 30, 2006

Good News from BICI

One of the institutions that is very close to my heart is the Bertinoro International Center for Informatics (aka BICI). I was therefore very pleased to hear today from Alessandro Panconesi that on June 10 there will be a press conference in Bertinoro to announce a three-year sponsorship program in favour of BICI. The sponsors are three banks or, more precisely, the foundations associated with them.

With the money BICI will institute a fellowship program to allow scholars in difficult financial conditions and PhD students to take part in Bertinoro events.

As Alessandro wrote to me, the level of funding is very far from that enjoyed by institutions like Dagsthul but it is nevertheless substantial. This is remarkable given how difficult it is to find funding for initiatives of this kind and
science in general in Italy.

Thanks to Alessandro for his sterling effort to put Bertinoro on the map as a suitable location for hosting high quality events in Computer Science. A look at the list of coming and past events that have been held in Bertinoro shows that BICI is working very well. Many happy returns to BICI and its friends. I won't be able to attend the press conference on June 10, but I'll be there in spirit.

Monday, May 29, 2006

ICE-TCS Theory Week in Reykjavík

We are entering a busy week of ICE-TCS events here in Reykjavík. After the very pleasant and inspiring visit by Jan Friso Groote, our Dutchman in residence is now Wan Fokkink, the co-author with whom Anna and I have written the largest number of papers. (Lucky us!)

Wan will be one of the three keynote speakers at the Second ICE-TCS Theory Day. The other keynote speakers will be Jan Kratochvil (Charles University, Pragua, CZ) and, last but not least, Moshe Vardi. This small symposium will take place on Wednesday, 31 May.

On Thursday, 1 June, there is an exciting and well publicized public talk of Moshe Vardi at 17:00. The poster for this lecture (in Icelandic!) is on the left.

I'll report on these events as soon as the dust has settled. Anna, Magnús Halldórsson and I will be repayed of our efforts in organizing them if Icelandic computer scientists will show up to these talks, and young researchers and students will be enticed to work in TCS by the stimulating research presented by our guests.

Wednesday, May 24, 2006

A Classic Open Problem

I just attended Jan Friso Groote's second talk during his inspirational visit to Reykjavík University. In this talk, entitled On using and proving modal formulas for analyzing processes, Jan Friso used some mCRL2 models of strategic games he developed during his stay to motivate the use of the modal mu-calculus (with data) to express properties of processes. He also showed how to do model checking for the modal mu-calculus via Gaussian elimination, and mentioned the tantalizing open problem of whether model checking for the modal mu-calculus is in P.

If you are looking for a (hard) open problem to work on, then this is one that you might want to pit your wits against. For the moment, the best result I am aware of on the characterization of the structural complexity of the model checking problem for the mu-calculus is by Marcin Jurdzinski. In this paper, Marcin showed that the problem is in the intersection of UP and coUP.
UP is the class of decision problems solvable by an NP machine such that
  • If the answer is 'yes,' exactly one computation path accepts.
  • If the answer is 'no,' all computation paths reject.

List of Accepted Papers for CONCUR 2006

Congratulations to the authors whose papers were selected for CONCUR 2006. The conference programme promises to be very interesting, and bears witness to the vitality of concurrency theory as a research area.

List of accepted papers:

1 Transition Systems of Elementary Net Systems
with Localities
Maciej Koutny, Marta Peitkiewicz-Koutny

3 Model Checking Quantified Computation Tree Logic
Arend Rensink

14 Encoding CDuce in the Cphi-calculus
Guiseppe Castagna, Mariangiola Dezani-Ciancaglini,
Daniele Varacca

17 A New Type System for Deadlock-Free Processes
Naoki Kobayashi

20 Strategy Improvement for Stochastic Rabin and
Streett Games
Krishnendu Chatterjee, Thomas Henzinger

22 On Finite Alphabets and Infinite Bases III: Simulation
Taolue Chen, Wan Fokkink

26 A Complete Axiomatization of Branching Bisimulation
for Probabilistic Systems, with an Application in
Protocol Verification
Suzana Andova, Jos baeten, Tim Willemse

30 Event Structure Semantics for Nominal Calculi
Roberto Bruni, Herman Megratti, Ugo Montanari

37 Sortings for Reactive Systems
Lars Birkedal, Soren Debois, Thomas Hildebrandt

43 Probabilistic I/O Automata: Theories of Two Equivalences
Eugene Stark, Rance Cleaveland, Scott Smolka

44 A Capability Calculus for Concurrency and Determinism
Tachio Terauchi, Alex Aiken

45 Dynamic Access Control in a Concurrent Object Calculus
Avik Chaudhuri

46 A Complete Axiomatic Semantics for the CSP
Stable-Failures Model
Yoshinao Isobe, Marcus Roggenbach

52 Inference of Event-Recording Automata Using
Timed Decision Trees
Olga Grinchtein, Bengt Jonsson, Paul Petterson

57 Reachability in Recursive Markov Decision Processes
Tomas Brazdil, Vaclav Brozek, Vojtech Forejt, Antonin Kucera

58 Second-Order Simple Grammars
Colin Stirling

60 Weak Bisimulation up to Elaboration
Damien Pous

61 Controller Synthesis for MTL Specifications
Patricia Boyer, Laura Bozzelli, Fabrice Chevalier

65 Finding Shortest Witnesses to the Nonemptiness
of Automata on Infinite Words
Orna Kupferman, Sarai Sheinvald

69 Operational Determinism and Fast Algorithms
Henri Hansen, Antti Valmari

75 Liveness, Fairness and Impossible Futures
Rob van Glabbeek, Marc Voorhoeve

79 Concurrent Rewriting for Graphs with Equivalences
Paolo Baldan, Fabio Gadduducci, Ugo Montanari

81 Proving Liveness by Backward Reachability
Parosh Aziz Abdulla, Bengt Jonsson, Ahmed Rezine,
Mayank Saksena

84 A Livelock Freedom Analysis for Infinite State
Asynchronous Reactive Systems
Stefan Leue, Alin Stefanescu, Wei Wei

86 On Interleaving in Timed Automata
Ramzi Ben Salah, Marius Bozga, Oded Maler

92 Generic Forward and Backward Simulation
Ichiro Hasuo

108 Minimization, Learning, and Conformance Testing
of Boolean Programs
Viraj Kumar, P. Madhusudan, Mahesh Viswanathan

110 A Language for Task Orchestration and its
Semantic Properties
William Cook, David Kitchin, Jayadev Misra

123 Checking a Mutex Algorithm in a Process Algebra
with Fairness
Flavio Corradini, Maria Rita Di Berardini, Walter Vogler

Tuesday, May 23, 2006

Visualization of Huge State Spaces

As I mentioned in one of my previous postings, Jan Friso Groote is currently visiting Anna and me in Reykjavík. As part of his stay, Jan Friso delivered a seminar on Wednesday, 10 May. The seminar, entitled "Visualization of Large State Spaces", marked, albeit belatedly, the first birthday of ICE-TCS---our little research centre in theoretical computer science.

The talk was the best attended one in computer science I have seen here in Reykjavík. It was accessible to a wide audience, and made a very strong, and aesthetically pleasing, case for the use of visualization techniques in the analysis of models of computing systems.

I had already heard previous versions of (parts of) this talk in Aalborg and Bertinoro, but the visualization tool is improving all the time, and so is the amount of information that an expert like Jan Friso can derive from the pictures it depicts. During the talk, we were treated to some very good examples of what one could call "visual data mining" in concurrency.

The work Jan Friso presented in the talk is described in detail in the paper

J.F. Groote and F.J.J. van Ham. Interactive visualization of large state spaces. International Journal on Software Tools for Technology Transfer 8:77-91, 2006.

I strongly recommend this paper to all of you.

Jan Friso will deliver his second seminar tomorrow, and I hope to post a few lines on it here in due course.

Monday, May 22, 2006

EATCS Distinguished Award 2006

The EATCS Distinguished Award 2006 will be presented during ICALP 2006 in Venice to Mike Paterson in recognition of his outstanding scientific contributions to theoretical computer science.

A good sample of Paterson's scientific output is mentioned on the DBLP, where you can get an idea of the range of his contributions spanning the last 36 years or so.

In this age of hyper specialization, it is good to see that our community can still boast several "Renaissance men" like Mike Paterson. Paraphrasing the last sentence in Stephen D. Smith's MathSci review of Enrico Bombieri's single paper in group theory, I can only say that an ordinary mortal such as yours truly is overawed by the depth and breadth of Paterson's contributions.

[Addendum: I just found out that Tom Leighton won the SIGACT Distinguished Service Award. Tom Leighton will be familiar to many of you as the prime mover behind Akamai. Look here for a glimpse at his research output.]

Saturday, May 20, 2006

Is This Hubris or What?

"My work is a fundamental extension of the work of Gödel and Turing on undecidability in pure mathematics." (Gregory J. Chaitin, "Conversations with a Mathematician---Math, Art, Science and the Limits of Reason", pp. 109-110, Springer-Verlag, 2003)

It is not up to me to say whether this is true or not---it is fair to say, however, that Chaitin's work is considered to be fundamental by many and will probably stay with us---, but is it up to the author himself? Would any of my readers claim in public that her/his work is fundamental?

My modest opinion is that the only judge of whether (the result of) some human endeavour is fundamental in any sense is Time.

Thursday, May 18, 2006

Classifying Quadratic Forms

This is probably not news for many of you, but I recently read the very well-written piece All Square by Ivars Peterson. In that piece, the author describes some results in number theory by Manjul Bhargava (Princeton) and Jonathan P. Hanke (Duke) on universal quadratic forms whose statements even I could understand.

A quadratic form is a polynomial with integer coefficients in which each term has a variable with exponent 2 or is a multiple of a product of two variables. Such a form is universal if it can generate all of the positive integers. Can one check whether a quadratic form is universal? The two mathematicians mentioned above have shown that it can, by proving that a quadratic formula is universal iff it can generate 29 different positive integers in the range 1 to 290! They also enumerated all of the 6436 universal quadratic forms in four variables.

Computer scientists like us will be happy to know that Jonathan P. Hanke uses computers in his work. (Look at this page.)

Wednesday, May 17, 2006

On the Axiomatizability of Priority

One of the positive things that happened during my sabbatical from posting on this diary was that I helped contribute to the writing of the paper On the Axiomatizability of Priority that I co-authored with Taolue Chen, Wan Fokkink and Anna Ingólfsdóttir. (As a consequence of this joint paper, my Taolue Chen number is now 1.) An extended abstract of that paper will appear in the proceedings of ICALP 2006.

The aforementioned paper studies the equational theory of bisimulation equivalence over the process algebra BCCSP extended with the classic priority operator theta of Baeten, Bergstra and Klop. Those who know my partiality for negative results won't be overly suprised to read that the main results in that paper are non-finite axiomatizability results that add the priority operator to the "bestiary" of operations from process theory that spoil the finite axiomatizability result for bisimilarity over BCCSP.

Are these results "interesting"? Well, they certainly won't change anybody's life, but I like them, despite the amount of effort that it takes to achieve them. I hope that a couple of readers will find them worth reading too.

Not all of my recent output is devoted to negative results though. I was lucky enough to contribute to the development of another paper during the last few months, but that will be the subject of another post.

[In case you wonder whether those papers would have been written without my collaborators, the answer is a resounding "No!"]

Wednesday, May 10, 2006

Concurrency Column for June 2006

I have just posted the Concurrency Column for the June 2006 issue of the Bulletin of the EATCS.

The column is a piece by Patricia Bouyer and Fabrice Chevalier entitled "On the Control of Timed and Hybrid Systems". The authors have been amongst the prime movers behind the recent developments in this fascinating research area, and their survey paper offers a well-written bird's eye view of the problems in this field and of the results that have been achieved so far.

Enjoy it!

Monday, May 08, 2006

"Give us something to take home!"

One of the pieces I keep reading over and over again is Gian-Carlo Rota's "Ten Lessons I Wish I Had Been Taught."

I am always reminded of his advice that a speaker should always try to give her/his audience something to take home when I am attending a talk that seems to lack a clear message. (And there are still quite a few of those, alas.) This is all the more true when we are trying to address an audience that is not made up of experts in the topic we wish to present.

I tried to pay heed to Rota's advice when preparing my invited talk for the Workshop on Logic, Models and Computer Science, held in Camerino from April 20 till April 22. The organizers of that workshop were kind enough to give me the opportunity to try and present some of the work my co-authors and I have done on negative results in the equational logic of processes to an audience consisting of distinguished logicians and computer scientists. This was an audience I would normally not reach with my work, and it remains to be seen whether I was even remotely successful in my attempt to reach them then. However, during the talk, I felt that being single-minded in my message was indeed helping me keep on the right track. In case anybody is interested, the slides I used for the talk are available as a PDF file.

The advice we give others is the advice that we ourselves need. I'll keep repeating Rota's mantra to myself whenever I have a talk to prepare. The results may not be good, but I'll try.

[Something I noticed in the workshop in Camerino was that people were not really ready to ask questions to the speakers. There is possibly a different tradition in Logic from the one in Computer Science, where it is the done thing to make sure that there is at least one question---no matter how routine it may be---following each talk.]

Sunday, May 07, 2006

A New Home for the Process Algebra Diary

From today, my modest Process Algebra Diary has a new home. Even a luddite like me has to bow to the usefulness of the latest technology at times :-)

I was prompted to try and use this blogging software by Luca Trevisan's blog In Theory. (Grazie Luca!) The main reason for using a proper blogging software in lieu of plain html files for the Process Algebra blog is that my two readers will now be able to post comments on my postings. Moreover, in my role as initial chairman of the IFIP WG1.8 on Concurrency Theory, I plan to use this blog as an open forum for discussions related to concurrency theory and its future.

I can see that my last posting on the Process Algebra Diary was written about three months ago. A lot has happened since then, and I'll try to review these last three months in a series of postings over the next few days --- assuming I manage, for once, to keep a promise, that is.

For the moment, I am glad to announce that Jan Friso Groote will be visiting Anna and me (and the little virtual research centre in TCS we contributed to set up) in Reykjavík over the next three weeks. I trust that his visit will do a lot for our efforts to put concurrency theory on the map here in Iceland.