CALCO Report, Part 3

This is the third, and final, installment of the coverage of CALCO 2007 on this blog. Thanks again to Mohammad for providing reports on the first three days of the event.

The first talk on Thursday was an invited address by Barbara König. Barbara's talk gave an excellent introduction to the general ideas and results on an active area of research in concurrency theory, namely the problem of deriving labelled transition system semantics and bisimulation congruences from reduction semantics and rewrite rules. This is a line of research that has been motivated by the theory of bisimulation congruences for process calculi, most notably the pi-calculus, and where categorical techniques play a fundamental role. See, for instance, the work by Leifer and Milner, and that by Sassone and Sobocinski.

Thursday also featured some talks on modal and epistemic logics, two talks on Chu spaces, and several categorical talks, which were alas well beyond my understanding of category theory.

The invited talk on Friday was delivered by Luis Caires, one of the prime movers behind the development of spatial logics. Luis' talk introduced a logical approach to the semantics of types for concurrency and to their soundness proofs based on spatial logics. I found the ideas presented in Luis' talk very intriguing, and I am going to read his paper in the proceedings when I have some time on my hands.

The conference concluded with a session on process algebra, where both Mohammad and I gave talks. (It is not for me to comment on how successful we were :-)) In case anybody is interested, the slides for my talk are here.

I enjoyed my trip to lovely Bergen, and thank the organizers for a very well-organized event. I hope to be able to visit Bergen again in the future. You can see some photos from Bergen here. Eventually, photos from CALCO will be available here.

Let me conclude with a couple of quotes from talks given at the conference and a poem I saw engraved in Vaagsallmenningen in Bergen.

"If you spell out this definition set theoretically, it looks quite horrible, but is not so difficult." (Clemens Kupke)

"The real voyage of discovery consists not in seeking new landscapes, but in having new eyes." (Marcel Proust, cited by Radu Mardare)

"Hele sit liv,
Anicet,
skal et menneske
laere at leve.
Hele sit liv,
Anicet,
skal han og
laere at doe."

(This roughly means "All his life, Anicet, a man must learn how to live. All his life, Anicet, he must also learn how to die.")

CALCO Report Part 2

Here is the second report from CALCO authored by Mohammad. Enjoy!

Live Report from CALCO - Part 2 Without further ado, here is my second report from CALCO. I will only give a short report of the two interesting keynote talks presented yesterday and today.

• Tuesday: Tuesday was the first day of CALCO 2007 main conference. There were some 40-50 participants (depending on when the snapshot is taken). Till Mossakowki opened the conference by mentioning that, despite initial doubts, CALCO 2007 was indeed a success and it attracted some 57 submissions from 3 continents and 14 countries.

  Stephen Bloom gave the keynote speech of Tuesday on algebraic and regular words and trees formalized as continuous $\Sigma$-algebras. He mentioned a recent result of his together with Zoltan Esik (I&C, 197(1-2):55--89, 2005) in which they present a complete axiomatization for regular words modulo isomorphism. He quoted the following interesting statement from his teacher who taught him about ordinals.

  "Ordinals are the numbers you use to count apples."

• Wednesday: Glynn Winskel delivered his keynote address on symmetry and concurrency. He motivated the choice of the topic by a few examples from Petri Nets and HD Automata and Strand Spaces to the effect that the lack of a notion of symmetry blocks universal treatment of some constructions (such as unfolding). He started off by introducing event structures (surprise, surprise!) and presented their application as types (in stable domain theory) and processes (in the semantics of process algebras and Petri Nets). Subsequently (total, rigid, and open) maps on event structures were presented as ways of relating them and in particular open maps are underscored as a notion of bisimulation among event structures. Semantics of nondeterministic dataflow programs was presented as a challenge to which event structure with some sort of maps to input and output even structures, called stable spans, provide a solution. Glynn mentioned that this is the same as the idea of pro-functors, but admittedly I could not appreciate the value of this fact! After some discussion on insufficiency of stable maps, he defined an abstract notion of symmetry using (a pair of) open maps on event structures. He ran a bit out of time and could not get into concrete applications of this notion of symmetry but the moral of the story, if I understand it correctly, is that by taking symmetry into account you get more general and universal constructions (maps) that are not too fine to distinguish between symmetric objects.

To conclude my reports on CALCO, I feel obliged to thank the local organizer for the excellent organization. Luca arrived here on Wednesday afternoon and I guess we will all have the chance to read about the rest from him.

Live Report from CALCO 2007 - Part 1

This is a guest post provided by MohammadReza Mousavi. Thanks to Mohammad!

Luca kindly invited me to write a guest post in his blog on CALCO 2007: the 2nd Conference on Algebra and Coalgebra in Computer Science. It is hosted by the University of Bergen in the picturesque city of Bergen (a UNESCO world heritage sight).

I am currently sitting in CALCO-jnr, a workshop of CALCO dedicated to young researchers (mainly Ph.D. students). The CALCO-jnr workshop is being attended by some 35 participants and I find the talks quite interesting and for such a workshop, which is usually meant for work-in-progress type of presentations, of reasonably high quality.

I must admit that the more categorical talks go well beyond my knowledge of this field and thus, I just write a few sentences about the few talks that I could (partially) follow.

• Ichiro Hasuo (a bright young researcher from Kyoto University, currently on leave to do a Ph.D. with Bart Jacobs) presented a very interesting talk on the application of Microcosm principle in Concurrency Theory. The Microcosm principle states that there is an analogy between the structure of the outer world and that of its elements (and in particular, that of the inside world of a human being; see this for an application in mathematics). Ichiro (together with Bart Jacobs and Ana Sokolova) take this idea into Computer Science and use it to prove properties such as congruence of behavioral equivalences (specified by the final model of the co-algebra under consideration) and commutativity and associativity of the operators under consideration. If I understand it correctly, they define a natural transformation that maps the composition operator at the level of co-algebras (e.g., LTSs) to the semantics of the composition of the objects in the carrier of the co-algebra (e.g., sets of pairs of processes indexed with labels). A concrete and tangible application is the way the semantics of parallel composition is defined by the synchronization scheme. Their approach resembles the bi-algebraic approach to operational semantics (e.g., this). A more detailed account of their results is available from here.
• Alexandra Silva presented some thoughts on representing bi-infinite streams, i.e., sequence of the form "... a_{-1} a_{0} a_{1} ..." using other worked-out co-algebraic frameworks for infinite binary trees and infinite streams. I remember a very interesting and accessible talk of Jan Rutten in FMCO 2003 presenting the very interesting co-algebraic treatment of streams which resembles the algebraic analysis techniques we learned in high school. Jan will give a talk on a related topic tomorrow, so you may get to read more about it soon.
• Liam O'Reilly talked about CSP-CASL-Prover which is based on a framework combining CSP as the process language and CASL for algebraic specification (of data types) and thus combines process specification and data specification. Their framework is built upon other tools, namely CSP Prover, which allow for reasoning about CSP processes with CASL data types in Isabelle. Coming from Eindhoven, I wonder whether this type of work can be seen as a rival to mCRL2 toolset and if so, which one will be favored in the long run.

In the afternoon, there were two parallel sessions: the continuation of CALCO-jnr and CALCO-tools. I decided to attend the tool presentations and here is a summary of what I learned there.

• Francisco Duran talked about the Maude tool environment. He introduced several tools built around Maude, including Interactive Theorem Prover, Termination Tool, and the Real-Time Maude Tool. Interestingly, a number of these tools have a web interface. There is a recent book on Maude, which can be bought from here.
• In the second talk, Dorel Lucanu introduced CIRC which is a tool for proving behavioral equivalences among (possibly infinite) processes specified in Maude.

So much for my first day of CALCO in Bergen; we will be off to a medieval castle for the reception this evening. Stay tuned for the second report!

Greetings from Bergen.

Being An Active Scientist at Age Eighty

Last Wednesday morning I took an hour to go and listen to a talk by Sigurdur Helgason at the University of Iceland. Sigurdur Helgason is one of Iceland's foremost scientists and a mathematician of great distinction, or so I am told. Suffice it to say that the American Mathematical Society have agreed to publish his collected works by some time next year---a honour that is bestowed only to true giants in mathematics.

I had the pleasure to meet Sigurdur Helgason in June 2004, when Anna and I visited Boston and MIT for Kári Ragnarsson's PhD graduation. He struck me as a very lively, curious and laid-back guy, who still enjoyed life, teaching his courses and thinking about maths despite being well over 70.

Sigurdur Helgason's talk kicked off a conference in honour of his 80th birthday. I had no chance of appreciating the technical content of the talk, but it was remarkable to see a 80-year-old man deliver such a well-planned presentation, reporting on some results he seemed to have achieved over the last four years or so. That was a truly awesome thing to witness.

What I found unbecoming was that there were no questions from the audience after the talk. Maybe the tradition in his area of maths is different from the one in TCS, but I would have expected at least the session chair to ask a token question to that great man.

Fortunately, being 80 and famous, he did not seem to be bothered!

Third ICE-TCS Theory Day

Last Friday, ICE-TCS hosted its third theory day. The programme for the event may be found here.

This year's theory day featured an inaugural professorial address delivered by Magnús M. Halldórsson, who joined my department at Reykjavík University on August 1. The addition of Magnús to our academic staff will substantially strengthen our research profile.

At the theory day, Magnús gave a talk in which he presented approximation algorithms for optimization problems when the objective function is unknown. The aim of the work he discussed during his presentation is to obtain algorithms that are guaranteed to perform reasonably well for all objective functions in the given class. He focussed on cost functions that are monotonic and concave (or, more generally, sub-additive), and presented approximation algorithms whose approximation ratio is 4 for concave functions and 6 for sub-additive ones.

Thomas Erlebach from the University of Leicester continued the "approximation theme" with a talk on network discovery problems. The work Thomas presented in his talk aims at discovering information about an unknown network (modelled as a connected undirected graph) or on verifying the correctness of network information. Thomas discussed two query models. In the former, a query at a node returns all the shortest path trees rooted at that node. In the latter, the result of a query at a node is the collection of shortest-path distances from that node. For the former type of queries, Thomas presented, for instance, a randomized O(sqroot{n log n})-competitive algorithm. For the latter query model, there is a deterministic Omega(sqroot{n}) lower bound and a randomized O(log n) lower bound. Much more can be found in the paper

Zuzana Beerliova, Felix Eberhard, Thomas Erlebach, Alexander Hall, Michael Hoffmann, Matus Mihalak, L. Shankar Ram:
Network Discovery and Verification
IEEE Journal on Selected Areas in Communications, Vol. 24, No. 12, December 2006, pp. 2168-2181. Special issue on Sampling the Internet: Techniques and Applications.

The afternoon session was devoted to a one-hour talk by Tommi Sottinen, our new recruit in financial mathematics, and to two 25-minute talks by Silvio Capobianco and MohammadReza Mousavi. Tommi gave an accessible introduction to the mathematics underlying financial mathematics and the Black-Scholes model. Silvio reported on recent joint work with Patrizia Mentrasti and Tommaso Toffoli, and showed us how to convert certain types of cellular automata to lattice gases. Mohammad wound up a nice scientific day by giving an accessible introduction to some recent work of his aiming at a unified framework for functional and performance analysis of processes. He proposed an approach enabling a provably sound transformation from some existing stochastic process algebras, e.g., PEPA and MTIPP, to a generic form in the mCRL2 language.

This workshop marks the beginning of a very busy year for ICE-TCS, a year leading up to ICALP 2008 in Reykjavík. I hope to see you in Reykjavík for that conference!

Atle Selberg (1917-2007)

The AMS news page reports that the Norwegian mathematician Atle Selberg passed away on August 6. As the AMS news item states, Selberg is perhaps best known for his work on the zeros of the Riemann zeta function, for which he was awarded a Fields Medal in 1950, and for his "elementary" proof of the prime number theorem. His honors include the 1986 Wolf Prize in Mathematics.

Selberg was also involved in one of the most famous controversies regarding allocation of credit for a result. His controversy with Paul Erdös regarding the genesis of the "elementary" proof of the prime number theorem features in every account of Erdös' life and work. See, e.g., this book and this obituary.

Addendum: I just saw that Luca Trevisan also has a (better) post on Selberg's death. Luca points to an obituary on the IAS web pages.

LICS Test-of-Time Award 2007

The LICS Test-of-Time Award recognizes a small number of influential papers which appeared in the LICS proceedings from 20 years prior that have best met the “test of time”.

I have just read that the Awards Committee for 2007, consisting of Yuri Gurevich (Chair), Rajeev Alur, and Glynn Winskel, selected the papers

• Samson Abramsky, Domain Theory in Logical Form, and
  
• Robert Harper, Furio Honsell and Gordon Plotkin, A Framework for Defining Logics,
  

as winners of the 2007 LICS Test-of-Time Award (for papers from LICS 1987). Congratulations to the authors for this recognition of their work! For once, I could have successfully bet on those two papers winning the award for 2007 :-)

Programming the Universe

I recently finished reading the book Programming the Universe by Seth Lloyd, Professor of Mechanical Engineering at MIT. The book is a very pleasant, thought-provoking read, and its message is honey to the ears of us computer scientists. To see why, it suffices only to read the first few lines in Chapter 1 of the book.

This book is the story of the universe and the bit. The universe is the biggest thing there is and the bit is the smallest possible chunk of information. The universe is made of bits. Every molecule, atom, and elementary particle registers bits of information. Every interaction between those pieces of the universe processes that information by altering those bits. That is, the universe computes, and because the universe is governed by the laws of quantum mechanics, it computes in an intrinsically quantum-mechanical fashion; its bits are quantum bits. The history of the universe is, in effect, a huge and ongoing quantum computation. The universe is a quantum computer.

Basically, Seth Lloyd's message is that information is just as important as classic physical quantities like energy in understanding the universe, and that viewing the universe as a quantum computer can actually help us understand it better. He even proposes a theory of quantum gravity based on this view---a theory that, unlike others, may even be testable experimentally.

You might like to have a look at a scientist's cut from the material Lloyd penned down for the book here. There you will also find some interesting quotes from referee reports Lloyd received for some of his papers, and the following estimate on the number of operations performed by the universe since the big bang.

The universe can have performed 10¹²⁰ ops on 10⁹⁰ bits (10¹²⁰ bits including gravitational degrees of freedom).

I wonder if Scott Aaronson has reviewed this book on his blog. It would be interesting to hear his opinion.

Vardi on Process Equivalences

Last Saturday, Moshe Vardi posted the paper Branching vs. Linear Time: Semantical Perspective (invited ATVA'07 paper with Sumit Nain). This is a nicely written and balanced paper distilling Moshe's thoughts on the choice of semantics for concurrent processes. I have no doubt that it will generate some healthy discussion in the concurrency theory community. I strongly encourage my two readers to have a look at it.

Oversimplifying the message in the paper by Moshe and Sumit, in their opinion the plethora of process semantics is due to "semantic underspecification". To overcome this underspecification, they propose to develop process semantics based on the following principles.

1. Principle of Contextual Equivalence: Two processes are equivalent if they behave the
   same in all contexts, which are processes with “holes”.
2. Principle of Comprehensive Modeling: A process description should model all relevant
   aspects of process behaviour.
3. Principle of Observable I/O: The observable behaviour of a tested process is precisely
   its input/output behaviour.

In the paper, Moshe and Sumit apply their approach to transducers, and show that, once the aforementioned three principles are applied, there is a trace-based equivalence that is adequate and fully abstract.

As the authors state in the paper "In conclusion, this paper puts forward an, admittedly provocative, thesis, which is that process-equivalence theory allowed itself to wander in the “wilderness” for lack of accepted guiding principles. The obvious definition of contextual equivalence was not scrupulously adhered to, and the underspecificity of the formalisms proposed led to too many interpretations of equivalence.While one may not realistic expect a single paper to overwrite about 30 years of research, a more modest hope would be for a renewed discussion on the basic principles of process-equivalence theory."

What do you think?

Rivest Wins Marconi Prize

MIT's Department of Electrical Engineering and Computer Science continues its rich harvest of awards. My RSS feeds monitor has informed me that Ron Rivest has been awarded the Marconi prize. See here for the MIT news item. Rivest has been named the 2007 Marconi Fellow and prize-winner for his pioneering work in the field of cryptography, computer and network security.

The Parking Algorithm

Furio Honsell is one of Italy's best known theoretical computer scientists. His research covers many areas within volume B TCS, and he was one of the proposers of the ‘Anti-Foundation Axiom’ for non-well-founded set theory. Furio was the first computer scientist to become rector of an Italian university, Università di Udine to be precise, and is now serving his second mandate as rector.

Unlike most of us, Furio is also known to the general Italian public for his participation in the TV show Che tempo che fa, where he discusses topics related to computer science and mathematics in a way that makes them accessible to a general audience. My mother, for instance, is fascinated by his witty and very clear discussions of topics that normally would not be aired on a TV show.

What has this all to do with "The Parking Algorithm"? A few days ago, walking back to my deck chair after a swim in the Adriatic sea, I saw a man read a volume by Furio entitled "L'Algoritmo del Parcheggio" ("The Parking Algorithm"), published by Mondadori, which is a major Italian publishing house. I was amazed. I stopped and asked this man whether I could write down the bibliographic details for the book, which I simply had to buy!

Furio is definitely doing a lot for promoting an appreciation for computer science and mathematics amongst the general educated public in Italy, and he must be doing it right if people read his book on the beach! I know that this is one of my, possibly boring, mantras, but we badly need more people who, like him, are not afraid to devote some of their time to writing books and articles for the general public, and who have the charisma to appear on TV and captivate viewers like my mother or that man who ended up buying his book and reading it under the sun-shade. (I also admire his time-management skills. Being a rector does not leave him a lot of time for research or book writing.)

For the record, I did buy Furio's book, but I'll have to wait for my mother to finish reading it before having a close look at it. I'll review Furio's book at some point in the future, but don't hold your breath.

"Reactive Systems" Is Out: Buy Your Copy Now!

A few days ago, I checked the web page at Amazon.co.uk for my latest book Reactive Systems: Modelling, Specification and Verification, which I have already shamelessly advertised in previous postings. I was surprised to read that only four copies were left in stock (and only one is in stock right now, so hurry!), especially because the official publication date for the book is 9 August 2007.

My copy of the book landed in my mailbox yesterday, as partial compensation for the departure of the hard disk in my laptop, the only computer I own :-( It was quite an experience to browse through the results of a few years of work while wondering whether I really had any part in writing the text filling those pages. This is how I often feel whenever I look at some work of mine. Was it really I who contributed to write/do that work? Something to ponder while waiting for a new hard disk, even though I know that it was really a different person from the one typing these characters who did it.

Anyway, I hope some of you will like the book, whoever wrote it.