I have been asked to announce that the deadlines for submission to FSEN 2009 have been extended.
The revised deadlines are as follows.
Abstract Submission: November 3, 2008
Paper Submission: November 10, 2008
The conference is held in what looks like a beautiful location in the Persian Gulf, and features top-class invited speakers.
Do consider submitting one of your papers.
Wednesday, October 22, 2008
Monday, October 06, 2008
New Centre of Excellence in Denmark
I recently learnt about the existence of a new centre of excellence in Denmark, the MT-Lab, devoted to topics close to my research area. The centre will officially open its activities in the second half of November.
Anna and I know basically all the consortium members very well, and it would take another post to describe our connections with several of them. These scientists are at the forefront of their research areas in computer science and control theory, and have been collecting centre-of-excellence funding from Danish governmental funding bodies before and on a regular basis. I have no doubt that the MT-Lab will become one of the most successful research centres in the world in its fields of expertise, and I am looking forward to monitoring its progress. Congratulations to the consortium members for the establishment of the centre!
A very interesting aspect of this centre of excellence is that this time around the 25 million DKK funding it (roughly € 3.35 million) are being provided by a private foundation, The Villum Kann Rasmussen Foundation. (See also this page to find out what other things they fund.)The existence of such foundations is one of the (many) strengths in the Danish funding for basic research, and I do not find it at all surprising that Denmark is home to a good collection of centres of excellence with very good international visibility and impact. With centres of this calibre, it is easy for Denmark to attract top-class scientists from abroad and to entice them to relocate to a country with good resources, a top-class welfare state and an excellent quality of life overall. (Yes, one pays very high taxes in Denmark, but, at times like the ones we are living, the sense of security that a well-oiled welfare state gives one becomes even more important than ever before.)
The Danish model for research funding has also inspired recent developments in the funding schemes available at European level. Let's see how much of this will survive the present turmoil on the financial markets.
Anna and I know basically all the consortium members very well, and it would take another post to describe our connections with several of them. These scientists are at the forefront of their research areas in computer science and control theory, and have been collecting centre-of-excellence funding from Danish governmental funding bodies before and on a regular basis. I have no doubt that the MT-Lab will become one of the most successful research centres in the world in its fields of expertise, and I am looking forward to monitoring its progress. Congratulations to the consortium members for the establishment of the centre!
A very interesting aspect of this centre of excellence is that this time around the 25 million DKK funding it (roughly € 3.35 million) are being provided by a private foundation, The Villum Kann Rasmussen Foundation. (See also this page to find out what other things they fund.)The existence of such foundations is one of the (many) strengths in the Danish funding for basic research, and I do not find it at all surprising that Denmark is home to a good collection of centres of excellence with very good international visibility and impact. With centres of this calibre, it is easy for Denmark to attract top-class scientists from abroad and to entice them to relocate to a country with good resources, a top-class welfare state and an excellent quality of life overall. (Yes, one pays very high taxes in Denmark, but, at times like the ones we are living, the sense of security that a well-oiled welfare state gives one becomes even more important than ever before.)
The Danish model for research funding has also inspired recent developments in the funding schemes available at European level. Let's see how much of this will survive the present turmoil on the financial markets.
Thursday, September 25, 2008
Vardi Receives The Blaise Pascal Medal in Computer Science For 2008
I just learned that Moshe Vardi is the recipient of the Blaise Pascal Medal in Computer Science for 2008 of the European Academy of Sciences. This is outstanding news for TCS as a whole and for the logic in computer science community in particular.
The motivation for the prize reads:
Moshe also contributes to the development of activities in TCS in my small corner of the world by sitting on the advisory board of ICE-TCS.
Congrats to Moshe! Somehow I feel that there will be more and even more prestigious awards in store for him.
The motivation for the prize reads:
In recognition of his outstanding contributions in several areas of computer science connected by their use of logic as an underlying methodology. His work has had fundamental and lasting impact on automatic verification, logic of knowledge, database theory, and finite-model theory.
Moshe also contributes to the development of activities in TCS in my small corner of the world by sitting on the advisory board of ICE-TCS.
Congrats to Moshe! Somehow I feel that there will be more and even more prestigious awards in store for him.
Monday, September 15, 2008
Concurrency column for the October issue of the BEATCS
I just posted the instalment of the concurrency column for the October issue of the Bulletin of the EATCS. The article, entitled Formalizing operational semantic specifications in logic, has been contributed by Dale Miller.
I strongly recommend this article not only to the standard readership of the concurrency column, but also to those readers who normally focus on logic in computer science and on programming languages amongst others. By publishing it, I feel like I am killing at least three birds with a stone.
Enjoy.
I strongly recommend this article not only to the standard readership of the concurrency column, but also to those readers who normally focus on logic in computer science and on programming languages amongst others. By publishing it, I feel like I am killing at least three birds with a stone.
Enjoy.
Wednesday, September 10, 2008
TCS 2008: Take Two
I am attending the session before lunch of TCS 2008, after which I will go to Milan central station to catch a train back to Pescara, my home town.
Today's invited talks were delivered by two Italian computer scientists, Antonio Restivo and Luca Cardelli.
Over the last 35 years or so, Restivo has been one of the prime movers in the Italian community of researchers working on automata and formal language theory. In his talk, he addressed the following basic question:
He described the approach he has developed with his co-workers, which is based on the notions of locality and projection. This notion turns out to coincide with the class of picture languages that are definable using existential monadic second-order logic. This leads Restivo to believe that it is the "right" notion of recognizable 2D language.
The notion of recognizable 2D language offers some surprises, at least for a non-expert like me. For instance, the language consisting of the square pictures over alphabet {a,b} that contain an equal number of a's and b's is recognizable, and so is the language of pictures of a's whose sides have prime length.
Luca Cardelli needs no introduction. In his talk, which was based on this paper, Luca presented a basic process-algebraic language that can be used to describe the ordinary differential equations that one meets in (bio-)chemistry. He showe several interesting applications of this language and how it can be used to investigate the discrete vs. continuous modelling dichotomy. The talk was excellent, as usual, and I am sure that the slides will appear very soon on this web page. It was great to see that a simple process calculus based on a stochastic version of Milner's CCS can be used to specify ODEs in a compositional way. For TCS people like us, the automata described by terms in the language "explain" the ODEs and why they take they form they take. Luca also showed us that his compilation of terms into ODEs produces exactly the known ODEs for some classic examples, such as the predator-prey one.
Yesterday, Tim Roughgarden gave a very interesting and beautifully delivered invited talk entitled Algorithmic Game Theory: Some Greatest Hits and Future Directions. You can read the paper here.
Today's invited talks were delivered by two Italian computer scientists, Antonio Restivo and Luca Cardelli.
Over the last 35 years or so, Restivo has been one of the prime movers in the Italian community of researchers working on automata and formal language theory. In his talk, he addressed the following basic question:
What is the "right" way of extending the notion of recognizability from word languages to picture languages?
He described the approach he has developed with his co-workers, which is based on the notions of locality and projection. This notion turns out to coincide with the class of picture languages that are definable using existential monadic second-order logic. This leads Restivo to believe that it is the "right" notion of recognizable 2D language.
The notion of recognizable 2D language offers some surprises, at least for a non-expert like me. For instance, the language consisting of the square pictures over alphabet {a,b} that contain an equal number of a's and b's is recognizable, and so is the language of pictures of a's whose sides have prime length.
Luca Cardelli needs no introduction. In his talk, which was based on this paper, Luca presented a basic process-algebraic language that can be used to describe the ordinary differential equations that one meets in (bio-)chemistry. He showe several interesting applications of this language and how it can be used to investigate the discrete vs. continuous modelling dichotomy. The talk was excellent, as usual, and I am sure that the slides will appear very soon on this web page. It was great to see that a simple process calculus based on a stochastic version of Milner's CCS can be used to specify ODEs in a compositional way. For TCS people like us, the automata described by terms in the language "explain" the ODEs and why they take they form they take. Luca also showed us that his compilation of terms into ODEs produces exactly the known ODEs for some classic examples, such as the predator-prey one.
Yesterday, Tim Roughgarden gave a very interesting and beautifully delivered invited talk entitled Algorithmic Game Theory: Some Greatest Hits and Future Directions. You can read the paper here.
Tuesday, September 09, 2008
TCS 2008: Invited Speakers for the First Day
I am in Milan for TCS 2008, the bi-annual conference organized by IFIP TC1 in conjunction with the World Computer Congress (WCC). TCS 2008 aims at covering both volume A and volume B TCS, and this year features as many as seven 45-minute invited talks over three days. (IMHO, this is an exceptional number of invited talks for such a short conference.)
Being part of an event like the WCC, which features many events for IT professionals, makes TCS a very expensive TCS conference to attend, and the atmosphere is somewhat different from that of the typical conference TCS folks tend to attend. The early registration fee for an IFIP member was 525 euros (the late one is 680 euros for IFIP members and 800 euros for non-members), it does not include lunches and at the coffee breaks we get just coffee! Not surprisingly attendance at the conference is small and, despite the number of CS departments in Milan and surrounding areas, there are preciously few locals taking part in the event. I guess that there is a definite lesson to be learnt here.
Here I will limit myself to discussing some of the invited talks at the conference. TCS 2008 was kicked off by a presentation delivered by Grzegorz Rozenberg entitled Natural Computing. In his talk, he discussed models of computation inspired by nature and how they differ from classical computational models we use in computer science. I have not found his presentation on line, but you can read Rozenberg's views on the subject of natural computing vis-a-vis classical computer science in his acceptance speech for a honorary degree he received from the University of Bologna as well as in the many (and I really mean "many") technical papers he has written on the topic.
Rozenberg's invited talk was followed by a truly remarkable presentation by Javier Esparza. Javier was one of our invited speakers at ICALP 2008 and I already sang the praises for his presentation in Reykjavík. I really wish that more students had been there to see how to deliver an excellent talk despite a lack of slides for the first ten minutes or so because of technical problems. This was an example of how very good story-telling skills can easily overcome technological failures (at least at the beginning of a technical talk). After all, a conference speaker or a teacher are not so different from ancient story tellers, minstrels or gurus.
Javier's talk reported on results that he has obtained with his students on the solution of monotonic polynomial equations, a subject that one would expect to have been completely settled by mathematicians a long time ago, and that instead has been the source of interesting recent developments in the computer-science literature. The key point here is that one can obtain very strong results on methods for solving polynomial fixed-point equations if one restricts oneself to monotonic equations. I let you browse through Javier's slides since nothing I could write here would do justice to the many exciting results he has achieved with his students. The slide also list some interesting open problems. In particular, consider the problem
MSPE-DECISION: Given an MSPE X = f (X) with rational coefficients and k rational, decide whether the first component of the least solution of that system of monotonic polynomial equations is at most k.
The above problem is in PSPACE and unlikely to be in P. It might be solvable using a polynomial number of arithmetic operations. According to Javier, a proof of this fact would be a sensational result. Some of you might like to sharpen their pencils and try to solve this problem.
I was again pleased to be in the room to listen to yet another inspiring talk by Javier, who is rapidly becoming one of the favourite invited speakers at European TCS conferences.
I will try to report on the other invited talks I heard at some point soon.
Being part of an event like the WCC, which features many events for IT professionals, makes TCS a very expensive TCS conference to attend, and the atmosphere is somewhat different from that of the typical conference TCS folks tend to attend. The early registration fee for an IFIP member was 525 euros (the late one is 680 euros for IFIP members and 800 euros for non-members), it does not include lunches and at the coffee breaks we get just coffee! Not surprisingly attendance at the conference is small and, despite the number of CS departments in Milan and surrounding areas, there are preciously few locals taking part in the event. I guess that there is a definite lesson to be learnt here.
Here I will limit myself to discussing some of the invited talks at the conference. TCS 2008 was kicked off by a presentation delivered by Grzegorz Rozenberg entitled Natural Computing. In his talk, he discussed models of computation inspired by nature and how they differ from classical computational models we use in computer science. I have not found his presentation on line, but you can read Rozenberg's views on the subject of natural computing vis-a-vis classical computer science in his acceptance speech for a honorary degree he received from the University of Bologna as well as in the many (and I really mean "many") technical papers he has written on the topic.
Rozenberg's invited talk was followed by a truly remarkable presentation by Javier Esparza. Javier was one of our invited speakers at ICALP 2008 and I already sang the praises for his presentation in Reykjavík. I really wish that more students had been there to see how to deliver an excellent talk despite a lack of slides for the first ten minutes or so because of technical problems. This was an example of how very good story-telling skills can easily overcome technological failures (at least at the beginning of a technical talk). After all, a conference speaker or a teacher are not so different from ancient story tellers, minstrels or gurus.
Javier's talk reported on results that he has obtained with his students on the solution of monotonic polynomial equations, a subject that one would expect to have been completely settled by mathematicians a long time ago, and that instead has been the source of interesting recent developments in the computer-science literature. The key point here is that one can obtain very strong results on methods for solving polynomial fixed-point equations if one restricts oneself to monotonic equations. I let you browse through Javier's slides since nothing I could write here would do justice to the many exciting results he has achieved with his students. The slide also list some interesting open problems. In particular, consider the problem
MSPE-DECISION: Given an MSPE X = f (X) with rational coefficients and k rational, decide whether the first component of the least solution of that system of monotonic polynomial equations is at most k.
The above problem is in PSPACE and unlikely to be in P. It might be solvable using a polynomial number of arithmetic operations. According to Javier, a proof of this fact would be a sensational result. Some of you might like to sharpen their pencils and try to solve this problem.
I was again pleased to be in the room to listen to yet another inspiring talk by Javier, who is rapidly becoming one of the favourite invited speakers at European TCS conferences.
I will try to report on the other invited talks I heard at some point soon.
Monday, September 01, 2008
Bereavement in Italian Theoretical Computer Science
On the night between August 19 and August 20, Italian TCS prematurely lost Stefano Varricchio (University of Rome "Tor Vergata") while he was on holiday with his family. He was 48, or so I am told.
Stefano's research was in the classic areas combinatorics on words, automata theory and formal languages. I am not qualified to offer an assessment of his research contributions, and I hope that some of my readers who work on the aforementioned topics will post comments on Varricchio's work. I met him once a few years ago during a visit to the University of L'Aquila, where he was a full professor at the time. I recall that, after my presentation based on this paper, he kindly pointed out the relevance of a famous theorem by Fine and Wilf for some of the results I presented.
Here is the theorem.
Theorem (Fine and Wilf, 1965) If a word x has periods p and q, and has length at least p + q − gcd(p, q), then x has also a period gcd(p, q).
A relative of mine and his wife, who followed Stefano's compilers course in L'Aquila, told me that he was one of the best teachers they had during their studies.
To quote a poem by Giuseppe Ungaretti,
Stefano's research was in the classic areas combinatorics on words, automata theory and formal languages. I am not qualified to offer an assessment of his research contributions, and I hope that some of my readers who work on the aforementioned topics will post comments on Varricchio's work. I met him once a few years ago during a visit to the University of L'Aquila, where he was a full professor at the time. I recall that, after my presentation based on this paper, he kindly pointed out the relevance of a famous theorem by Fine and Wilf for some of the results I presented.
Here is the theorem.
Theorem (Fine and Wilf, 1965) If a word x has periods p and q, and has length at least p + q − gcd(p, q), then x has also a period gcd(p, q).
A relative of mine and his wife, who followed Stefano's compilers course in L'Aquila, told me that he was one of the best teachers they had during their studies.
To quote a poem by Giuseppe Ungaretti,
Si sta come, d'autunno, sugli alberi, le foglie.
G. Ungaretti - Soldati Bosco di Courton luglio 1918
Tuesday, July 29, 2008
Desperately Seeking Mathematical Truth
The August issue of the Notices of the AMS includes an opinion piece entitled "Desperately Seeking Mathematical Truth" by Melvyn B. Nathanson. At the risk of oversimplifying the message in that opinion piece, the gist of the article can be summarized as follows, using direct quotes from Nathanson's opinion piece.
Yes, proofs of several published theorems contain mistakes. However, more often than not, the mistakes can be fixed and the results turn out to live to see the day after all.
Of course, I expect that mathematicians will want to improve upon the social notion of proof that underlies their profession. Quoting again from the opinion piece by Nathanson:
Do any of you think that proof-checking of research-level mathematical proofs will become commonplace in our lifetime?
Addendum dated 5 August 2008: I should have known that Doron Zeilberger would have commented on Nathanson's opinion piece. Of course, Dr. Z's opinion is thought provoking as usual. You can read it here. In summary, Dr. Z suggests two ways for improving the reliability of mathematical knowledge.
Regarding the second suggestion, I am not so sure that abandoning anonymity in refereeing would have such a great effect on the reliability of mathematical literature. The bottom line is that one should exercise the greatest amount of professionalism in all aspects of the academic profession, regardless of whether one does something anonymously or not. Excellent referees are a great resource to have, and editors and PC members soon build a trusted core of referees that can be relied upon to provide high-quality feedback to authors and editors alike. Referees who do not do a good job tend to be ignored after a while, as do editors who act as black holes for the papers that are submitted to them.
- "Our knowledge of the truth of a theorem depends on the correctness of its proof and on the correctness of all of the theorems used in its proof. It is a shaky foundation" because "many great and important theorems don’t actually have proofs. They have sketches of proofs, outlines of arguments, hints and intuitions that were obvious to the author (at least, at the time of writing) and that, hopefully, are understood and believed by some part of the mathematical community."
- Recognizing mathematical truth is harder than one might think at first. "If a theorem
has a short complete proof, we can check it. But if the proof is deep, difficult, and already fills 100 journal pages, if no one has the time and energy to fill in the details, if a “complete” proof would be 100,000 pages long, then we rely on the judgments of the bosses in the field. In mathematics, a theorem is true, or it’s not a theorem. But even in mathematics, truth can be political."
Yes, proofs of several published theorems contain mistakes. However, more often than not, the mistakes can be fixed and the results turn out to live to see the day after all.
Of course, I expect that mathematicians will want to improve upon the social notion of proof that underlies their profession. Quoting again from the opinion piece by Nathanson:
How can the reliability of mathematical proofs be improved? When should a proof be deemed to be "complete"? As a computer scientist, I'd say that a proof is really "complete" when it can be verified by a computer-based proof checker and it has been independently verified using a few such software tools. I know that this is a very stringent requirement, which will most likely never be implemented, but either we are ready to accept that mathematical truth is an unreliable but remarkably robust notion or we enlist the help of our computers to try and make it more reliable.
We mathematicians like to talk about the “reliability” of our literature, but it is, in fact, unreliable.
Part of the problem is refereeing. Many (I think most) papers in most refereed journals are not refereed. There is a presumptive referee who looks at the paper, reads the introduction and the statements of the results, glances at the proofs, and, if everything seems okay, recommends publication. Some referees do check proofs line-by-line, but many do not. When I read a journal article, I often find mistakes. Whether I can fix them is irrelevant. The literature is unreliable.
Do any of you think that proof-checking of research-level mathematical proofs will become commonplace in our lifetime?
Addendum dated 5 August 2008: I should have known that Doron Zeilberger would have commented on Nathanson's opinion piece. Of course, Dr. Z's opinion is thought provoking as usual. You can read it here. In summary, Dr. Z suggests two ways for improving the reliability of mathematical knowledge.
- In his words, "First computerize! Computers are much more reliable than humans, and as more and more mathematics is becoming amenable to computer checking, this is the way to go."
- Abandon anonymous refereeing.
Regarding the second suggestion, I am not so sure that abandoning anonymity in refereeing would have such a great effect on the reliability of mathematical literature. The bottom line is that one should exercise the greatest amount of professionalism in all aspects of the academic profession, regardless of whether one does something anonymously or not. Excellent referees are a great resource to have, and editors and PC members soon build a trusted core of referees that can be relied upon to provide high-quality feedback to authors and editors alike. Referees who do not do a good job tend to be ignored after a while, as do editors who act as black holes for the papers that are submitted to them.
Wednesday, July 23, 2008
Third ICE-TCS Annual Report
The third ICE-TCS annual report has been available since June 12, but I never mentioned its availability on this blog. If you are interested in keeping abreast of what is happening in our little TCS centre here in Reykjavík, do have a look.
Some of the people who attended ICALP 2008 asked us what we are going to do with the centre when funding runs out. Our answer was, "What funding?" The centre operates with very few resources and without specific funding to support its activities. We try to raise money in ad hoc and haphazard ways.
The Icelandic Fund for Research announced the availability of centre-building funding for the first time ever last spring. A consortium led by ICE-TCS sent in a pre-proposal, but our expression of interest was not one of the ten that were selected for further consideration, alas. Such is life, I guess, but, if I may say so, the list of ten selected pre-proposals is somewhat surprising on purely scientific grounds and hardly fulfils the requirements concerning international collaboration. (Our pre-proposal had BRICS, CISS, FUNDIM and the Centre for Computational Molecular Biology at Brown University as some of its cooperating centres.)
Anyway, we will try to maintain a decent level of activity in TCS on this remote, but rather attractive, island in the north Atlantic :-) For present activity on another much smaller, but also much hotter, island, see Luca Trevisan's in theory.
Some of the people who attended ICALP 2008 asked us what we are going to do with the centre when funding runs out. Our answer was, "What funding?" The centre operates with very few resources and without specific funding to support its activities. We try to raise money in ad hoc and haphazard ways.
The Icelandic Fund for Research announced the availability of centre-building funding for the first time ever last spring. A consortium led by ICE-TCS sent in a pre-proposal, but our expression of interest was not one of the ten that were selected for further consideration, alas. Such is life, I guess, but, if I may say so, the list of ten selected pre-proposals is somewhat surprising on purely scientific grounds and hardly fulfils the requirements concerning international collaboration. (Our pre-proposal had BRICS, CISS, FUNDIM and the Centre for Computational Molecular Biology at Brown University as some of its cooperating centres.)
Anyway, we will try to maintain a decent level of activity in TCS on this remote, but rather attractive, island in the north Atlantic :-) For present activity on another much smaller, but also much hotter, island, see Luca Trevisan's in theory.
Monday, July 21, 2008
General Assembly of the EATCS at ICALP 2008
The EATCS holds its annual General Assembly (GA) during ICALP. This year's GA was held during ICALP 2008 on Tuesday, 8 July, after Peter Winkler's master class on mathematical puzzles. I have already covered some of the highlights of the GA in earlier posts (e.g., the best paper awards for ICALP 2008 and the proposed new young research prize in TCS). Here I will limit myself to highlighting a few of the many issues under discussion within the EATCS Council that you might be interested in commenting on. In general, the EATCS strongly encourages feedback and suggestions from the members of the TCS community at large. I will pass on to the Council any suggestion/comment/criticism you might have.
First of all, here are some statistics presented by Leslie Ann Goldberg regarding track A of ICALP 2008. Track A had 133 submissions that could be classified as dealing with Design and Analysis of Algorithms, 87 for Complexity Theory and 67 under the heading Approximation. The most successful topic as far as percentage of acceptances was concerned was Quantum Computation (6 selected out of 14 submissions, 43% selection rate); Randomness was second with 15 selected out of 39 submissions (38% selection rate). Overall, Germany, Israel and the USA contributed 120 submissions to track A.
For track B, there were 8 selected papers under the heading Verification, 7 on Words and Trees and 6 on Logic and Complexity. Germany and France led the number of authors with 39 and 39 authors each. The UK, the USA and Italy were next in line with 32, 29 and 25 authors, respectively. Spain was next with 13 authors.
No comparable statistics were presented for track C. However, Ivan Damgaard remarked that it was noteworthy that no accepted paper for track C dealt with the formal specification and verification of security protocols.
The General Assembly approved the suggestion of the Council that ICALP 2010 be organized in Bordeaux, France. Igor Walukiewicz presented the bid from Bordeaux, highlighting many reasons for having ICALP there. The GA also discussed possible alternatives for ICALP 2011. In particular, Giorgio Ausiello mentioned that the sister society AAAC (Asian Association for Algorithms and Computation) has invited ICALP to Japan. Concerning 2012, Giorgio Ausiello mentioned that, in the occasion of the centennial of Turing's birth, a special event should take place in Cambridge, UK. The EATCS is considering the co-location of ICALP 2012 with the events in the Turing centennial.
Jan van Leeuwen reported on possible connections netween the EATCS and Computability in Europe, a new association that "aims to widen understanding and appreciation of the importance of the concepts and techniques of computability theory, and to support the development of a vibrant multi-disciplinary community of researchers focused on computability-related topics."
The EATCS Council has formed a new publication committee which I have been asked to chair. Apart from me, the committee will consist of Josep Diaz, Juhani Karhumaki, Burkhard Monien, Catuscia Palamidessi, Valdimiro Sassone and Maria Serna (the new editor of the Bulletin of the EATCS). One of the important roles that this committee will have is to propose future developments for the Bulletin, which is the flagship publication of the EATCS. I would be very happy to hear your opinions on and wishes for the BEATCS.
Amongst the many developments within the EATCS let me finish by mentioning that the EATCS Council has decided that the Secretarial Office will move to CTI. The Secretarial support will be partly paid by EATCS, partly sponsored by CTI. The experiment will be carried on for a period of three years. An important role that the new Secretarial Office will play is in maintaining an ongoing connection between the EATCS and its members. The latest membership figures show a worrying decrease in the number of members at a time when the EATCS needs the support of the TCS community to foster its increasing number of high-profile activities. The number of members of the EATCS has gone down from 1036 in 2006 to 882 in 2007, and has hit an all-time low in 2008 (with 678 members). I hope that the success of ICALP 2008 will help the association a little.
Many photos from ICALP 2008 are available by following the links from this web page.
First of all, here are some statistics presented by Leslie Ann Goldberg regarding track A of ICALP 2008. Track A had 133 submissions that could be classified as dealing with Design and Analysis of Algorithms, 87 for Complexity Theory and 67 under the heading Approximation. The most successful topic as far as percentage of acceptances was concerned was Quantum Computation (6 selected out of 14 submissions, 43% selection rate); Randomness was second with 15 selected out of 39 submissions (38% selection rate). Overall, Germany, Israel and the USA contributed 120 submissions to track A.
For track B, there were 8 selected papers under the heading Verification, 7 on Words and Trees and 6 on Logic and Complexity. Germany and France led the number of authors with 39 and 39 authors each. The UK, the USA and Italy were next in line with 32, 29 and 25 authors, respectively. Spain was next with 13 authors.
No comparable statistics were presented for track C. However, Ivan Damgaard remarked that it was noteworthy that no accepted paper for track C dealt with the formal specification and verification of security protocols.
The General Assembly approved the suggestion of the Council that ICALP 2010 be organized in Bordeaux, France. Igor Walukiewicz presented the bid from Bordeaux, highlighting many reasons for having ICALP there. The GA also discussed possible alternatives for ICALP 2011. In particular, Giorgio Ausiello mentioned that the sister society AAAC (Asian Association for Algorithms and Computation) has invited ICALP to Japan. Concerning 2012, Giorgio Ausiello mentioned that, in the occasion of the centennial of Turing's birth, a special event should take place in Cambridge, UK. The EATCS is considering the co-location of ICALP 2012 with the events in the Turing centennial.
Jan van Leeuwen reported on possible connections netween the EATCS and Computability in Europe, a new association that "aims to widen understanding and appreciation of the importance of the concepts and techniques of computability theory, and to support the development of a vibrant multi-disciplinary community of researchers focused on computability-related topics."
The EATCS Council has formed a new publication committee which I have been asked to chair. Apart from me, the committee will consist of Josep Diaz, Juhani Karhumaki, Burkhard Monien, Catuscia Palamidessi, Valdimiro Sassone and Maria Serna (the new editor of the Bulletin of the EATCS). One of the important roles that this committee will have is to propose future developments for the Bulletin, which is the flagship publication of the EATCS. I would be very happy to hear your opinions on and wishes for the BEATCS.
Amongst the many developments within the EATCS let me finish by mentioning that the EATCS Council has decided that the Secretarial Office will move to CTI. The Secretarial support will be partly paid by EATCS, partly sponsored by CTI. The experiment will be carried on for a period of three years. An important role that the new Secretarial Office will play is in maintaining an ongoing connection between the EATCS and its members. The latest membership figures show a worrying decrease in the number of members at a time when the EATCS needs the support of the TCS community to foster its increasing number of high-profile activities. The number of members of the EATCS has gone down from 1036 in 2006 to 882 in 2007, and has hit an all-time low in 2008 (with 678 members). I hope that the success of ICALP 2008 will help the association a little.
Many photos from ICALP 2008 are available by following the links from this web page.
Friday, July 18, 2008
CadiaPlayer Strikes Again
About one year ago, CADIAPlayer, developed by Yngvi Björnsson and his MSc student Hilmar Finsson within CADIA, our centre for AI research won the General Game Playing (GPP) competition at AAAI 2007. (The aim of the GGP competitions is to help develop systems that can accept a formal description of an arbitrary game and, without further human interaction, can play the game effectively.)
I am happy to report that, in a repeat of last year's final, CadiaPlayer confirmed its world-champion status in GGP at AAAI 2008 in Chicago by defeating ClunePlayer from the University of California, Los Angeles. (ClunePlayer has now been runner-up for three years in a row, and was the world champion in 2005.)
This is great news for the School of Computer Science at Reykjavík University. Congrats to Yngvi, Hilmar and Gylfi.
I am happy to report that, in a repeat of last year's final, CadiaPlayer confirmed its world-champion status in GGP at AAAI 2008 in Chicago by defeating ClunePlayer from the University of California, Los Angeles. (ClunePlayer has now been runner-up for three years in a row, and was the world champion in 2005.)
This is great news for the School of Computer Science at Reykjavík University. Congrats to Yngvi, Hilmar and Gylfi.
Wednesday, July 16, 2008
June Issue of the Bulletin of the EATCS
Continuing the open access policy of the EATCS, the June issue of the BEATCS is now available here for free download. I trust that you will find something of interest to you in this volume, which also features a little technical contribution by your truly.
Let me take this opportunity to encourage all of you to become members of the EATCS. Becoming a member is cheap (30 €) and easy. Moreover, by becoming a member you will support the activities of the TCS community at large not just in Europe, but across the world. These are busy times for the EATCS, and the organization needs your support to thrive.
For instance, I can tell you that, during its meeting at ICALP 2008 in Reykjavík, the EATCS Council decided to create a new Award for Young Researchers. The new award committee of the EATCS will soon define the details for the prize. The EATCS aims at having the rules set by ICALP 2009, so that after that conference, it can distribute the call for nominations, appoint the evaluation committee and set the deadlines with the aim to deliver the award for the first time at ICALP 2010. More news on the EATCS General Assembly held at ICALP 2008 will follow soon.
Let me take this opportunity to encourage all of you to become members of the EATCS. Becoming a member is cheap (30 €) and easy. Moreover, by becoming a member you will support the activities of the TCS community at large not just in Europe, but across the world. These are busy times for the EATCS, and the organization needs your support to thrive.
For instance, I can tell you that, during its meeting at ICALP 2008 in Reykjavík, the EATCS Council decided to create a new Award for Young Researchers. The new award committee of the EATCS will soon define the details for the prize. The EATCS aims at having the rules set by ICALP 2009, so that after that conference, it can distribute the call for nominations, appoint the evaluation committee and set the deadlines with the aim to deliver the award for the first time at ICALP 2010. More news on the EATCS General Assembly held at ICALP 2008 will follow soon.
Some Recent Awards
A few awards and prizes have recently been handed out to members of the TCS community.
The LICS test-of-time award 2008 has been given to Martín Abadi and Leslie Lamport for their paper The Existence of Refinement Mappings. In Lamport's own words:
Finally, the European Mathematical Society (EMS) awarded its prizes at the 5th European Congress of Mathematics, held this week in Amsterdam (The Netherlands). The EMS prizes are awarded to young researchers not older than 35 years, in recognition of distinguished contributions in mathematics, and are presented every four years at the European Congress of Mathematics. One of the recipients of the EMS prizes is Assaf Naor, who is honoured for "his groundbreaking contributions to functional analysis, the theory of algorithms, and combinatorics".
Congrats to the award recipients!
The LICS test-of-time award 2008 has been given to Martín Abadi and Leslie Lamport for their paper The Existence of Refinement Mappings. In Lamport's own words:
The first CAV award has just been given to Rajeev Alur and David Dill for the invention of the formalism of timed automata. See the full announcement for more details. This is a well deserved recognition to Rajeev and David for a fundamental contribution to the theory of real-time systems verification. Timed automata have been the subject of extensive theoretical investigation since the original paper by Rajeev and David and form the basis for software tools for the specification and verification of real-time systems such as Uppaal. Readers who are interested in a leisurely introduction to the basic theory of timed automata might wish to read part II of this book.
The method of proving that one specification implements another by using a refinement mapping was well-established by the mid-80s. ..... It was known that constructing the refinement mapping might require adding history variables to the implementation. Indeed, Lam and Shankar essentially constructed all their refinement mappings with history variables. Jim Saxe discovered a simple example showing that history variables weren't enough. To handle that example, he devised a more complicated refinement-mapping rule. I realized that I could eliminate that complicated rule, and use ordinary refinement, by introducing a new kind of dummy variable that I called a prophecy variable. A prophecy variable is very much like a history variable, except it predicts the future instead of remembering the past. (Nancy Lynch later rediscovered Saxe's rule and used it to "simplify" refinement proofs by eliminating prophecy variables.) I then remembered a problematic example by Herlihy and Wing in their classic paper Linearizability: A Correctness Condition for Concurrent Objects that could be handled with prophecy variables.This paper was my first collaboration with Abadi. Here's my recollection of how it was written. I had a hunch that history and prophecy variables were all one needed. Abadi had recently joined SRC, and this seemed like a fine opportunity to interest him in the things I was working on. So I described my hunch to him and suggested that he look into proving it. He came back in a few weeks with the results described in the paper. My hunch was right, except that there were hypotheses needed that I hadn't suspected. Abadi, however, recalls my having had a clearer picture of the final theorem, and that we worked out some of the details together when writing the final proof.
I had just developed the structured proof style described in [100], so I insisted that we write our proofs in this style, which meant rewriting Abadi's original proofs. In the process, we discovered a number of minor errors in the proofs, but no errors in the results.
Finally, the European Mathematical Society (EMS) awarded its prizes at the 5th European Congress of Mathematics, held this week in Amsterdam (The Netherlands). The EMS prizes are awarded to young researchers not older than 35 years, in recognition of distinguished contributions in mathematics, and are presented every four years at the European Congress of Mathematics. One of the recipients of the EMS prizes is Assaf Naor, who is honoured for "his groundbreaking contributions to functional analysis, the theory of algorithms, and combinatorics".
Congrats to the award recipients!
Sunday, July 13, 2008
Leslie Valiant's EATCS Award Talk
An anonymous comment to my previous post on ICALP 2008 asked
I'm very curious what Valiant talked about Evolution, Intelligence and Human Brain. In particular if he said anything concrete.Here are some recollections I have from Leslie Valiant's talk. I apologize if I have misinterpreted the main messages from his presentation.
Leslie started his talk by recalling that the first conference he ever attended was ALP 1972 in Paris, which would later become the first ICALP conference. He also quoted an excerpt from the preface of the proceedings for that conference, which I did copy verbatim, written by Maurice Nivat:
“If I were asked, in this preface, to explain how each of these forty five papers contributes to the solution of the main problems in Computer Science, I would be very embarrassed."I leave it to you to interpret this quote :-)
The bulk of Leslie's presentation was supposed to deal with three topics that interest him right now, namely:
- Evolution
- Intelligence
- Human Brain.
Regarding evolution, Leslie Valiant remarked that in the 19th century Darwin and Wallace posited an algorithmic mechanism for evolution: “random variation and natural selection.” Up to this day, there are no serious rivals to the Darwin/Wallace theory, but computer simulations of “random variation and selection” offer rather unimpressive results in evolving complex mechanisms.
Leslie mentioned the "quantitative mystery" behind evolution:
- How can such wonderful 3 billion length DNA strings be found in only 3 billion years?
- Does evolving complex circuits take exponential time?
V. Feldman. Evolvability from learning algorithms, Proc. 40th ACM Symposium on Theory of Computing (2008).
Regarding intelligence, Leslie started by asking
What are people good at that computers are bad at?His answer was "common-sense knowledge". He then provided the example of word completion (that he used in some recent experiments) and introduced the concept of robust logic, which he introduced about eight years ago. In his own words:
Robust Logic gives a common semantics for learning and reasoning, polynomial time algorithms for both, and soundness and completeness for reasoning.Leslie described a recent experiment he carried out with Michael in which they developed a system to analyze about 500,000 sentences from the Wall Street Journal. They used a parser to find the structure of the sentences, learned rules to predict erased words and investigated whether chaining these rules leads to an improvement over baseline methods in predicting missing words. The results were a little better than those obtained using baseline methods.
Leslie concluded by saying that we need good "teaching material" for systems like the one Michael and he developed.
Friday, July 11, 2008
ICALP 2008
ICALP 2008 is now over, but the last six satellite workshops will take place over the coming week-end. MohammadReza Mousavi has already reported on some of the talks at the conference in a series of guest posts. Here I will just limit myself to a few remarks on the main events that took place since Wednesday. I will try to devote future posts to some of the other news from the conference.
On Wednesday, Bruno Courcelle (Labri, Universitè Bordeaux, France) delivered a plenary invited talk entitled Graph Structure and Monadic Second-order Logic: Language Theoretical Aspects. Courcelle is one of the 15 most cited French scientists and the most cited French computer scientist. (See http://www.labri.fr/perso/courcell/PrixCitations2004.doc .) In addition, he has become a member of the very prestigious Institut Universitaire de France (see http://iuf.amue.fr/author/bcourcelle/ ). Courcelle is one of the grand "old" men in theoretical computer science. In a career spanning about 35 years he has given fundamental contributions to the study of the logical, language-theoretic and algorithmic aspects of the theory of graphs. He is also one of the founders of, and main contributors to, algebraic semantics. In his talk, Bruno described the role that hierarchical decompositions and Monadic Second-order Logic play in the extension of methods and results from classic Formal Language Theory to the description of sets of finite graphs. Bruno is putting the final touches to a monograph on this topic that will be published by Cambridge University Press. (Present state of the work Part 1 : Chapters 1-6. Part 2 : Chapters 7-11.)
The scientific programme on Thursday was kicked off by an invited plenary talk by Peter Winkler (Dartmouth, USA). The talk, entitled Optimality and Greed in Dynamic Allocation, described a method for proving optimality in dynamic allocation problems that relies on the assumption that "it's right to be greedy." The method was developed while Peter was working on two problems which arose at Lucent Technologies.
The scientific programme for Thursday reached its climax with the award ceremony, during which the EATCS award and the Gödel prize where handed out. After receiving the EATCS award, Leslie G. Valiant (Harvard, USA) delivered an excellent 30-minute presentation focusing on three topics that interest him right now. The topics are:
The Gödel prize talk, delivered by Daniel A. Spielman (Yale, USA), provided an outstanding finale for the day. In his talk, Dan explained the idea of smooth anallysis, how Teng and he thought of it and what he hopes the future will bring. Shang-Hua Teng (Boston University, USA) gave a personal and heartfelt introduction to the work they did to merit such a prestigious award.
The main event during the final day at ICALP was an invited plenary talk delivered by Javier Esparza (Technische Universität München, Germany). Javier's presentation was entitled Newtonian Program Analysis and presented recent work by his students and him that aims at using a computational approach to solving equations developed by Isaac Newton about 300 years ago in the analysis of computer programs. The talk presented exciting work and was beautifully and enthusiastically delivered. After the talk, Peter Winkler commented to us: "You saved the best for the last!" Javier closed the talk by saying that "Newton did it all 300 years ago, but he never saw Iceland!"
On Wednesday, Bruno Courcelle (Labri, Universitè Bordeaux, France) delivered a plenary invited talk entitled Graph Structure and Monadic Second-order Logic: Language Theoretical Aspects. Courcelle is one of the 15 most cited French scientists and the most cited French computer scientist. (See http://www.labri.fr/perso/
The scientific programme on Thursday was kicked off by an invited plenary talk by Peter Winkler (Dartmouth, USA). The talk, entitled Optimality and Greed in Dynamic Allocation, described a method for proving optimality in dynamic allocation problems that relies on the assumption that "it's right to be greedy." The method was developed while Peter was working on two problems which arose at Lucent Technologies.
The scientific programme for Thursday reached its climax with the award ceremony, during which the EATCS award and the Gödel prize where handed out. After receiving the EATCS award, Leslie G. Valiant (Harvard, USA) delivered an excellent 30-minute presentation focusing on three topics that interest him right now. The topics are:
- Evolution
- Intelligence
- Human Brain.
The Gödel prize talk, delivered by Daniel A. Spielman (Yale, USA), provided an outstanding finale for the day. In his talk, Dan explained the idea of smooth anallysis, how Teng and he thought of it and what he hopes the future will bring. Shang-Hua Teng (Boston University, USA) gave a personal and heartfelt introduction to the work they did to merit such a prestigious award.
The main event during the final day at ICALP was an invited plenary talk delivered by Javier Esparza (Technische Universität München, Germany). Javier's presentation was entitled Newtonian Program Analysis and presented recent work by his students and him that aims at using a computational approach to solving equations developed by Isaac Newton about 300 years ago in the analysis of computer programs. The talk presented exciting work and was beautifully and enthusiastically delivered. After the talk, Peter Winkler commented to us: "You saved the best for the last!" Javier closed the talk by saying that "Newton did it all 300 years ago, but he never saw Iceland!"
Wednesday, July 09, 2008
Dijkstra Prize 2008 to Baruch Awerbuch and David Peleg
During the meeting of the EATCS Council at ICALP 2008, I learned that the Dijkstra Award Committee has selected Baruch Awerbuch and David Peleg as the recipients of this year Edsger W. Dijkstra Prize in Distributed Computing. The price is given to them for their outstanding paper: "Sparse Partitions" published in FOCS 1990.
The prize is given for outstanding papers on the principles of distributed computing, whose significance and impact on the theory and/or practice of distributed computing has been evident for at least a decade. The Prize includes an award of $2000.
My Third Day @ ICALP 2008 (Guest Post by MohammadReza Mousavi)
This is the third guest post by MohammadReza Mousavi on ICALP 2008.
Ran Canetti: Composable Formal Security Analysis (Invited Speech)
Ran underscored the fact that the most challenging part of verifying security is to guarantee that protocols remain secure when put in arbitrary contexts and composed with other protocols. He defined a notion of security which basically requires that the observational behavior of a protocol in the presence of an "environment" machine (which can interfere in all possible ways) emulates the behavior of a perfectly secure protocol with a trusted third party. Combining symbolic methods with concrete cryptographic protocols is another aspect of composition theorem. Explicit analysis of all possible combination of such protocols is infeasible.
The message of the talk can be nicely summarized in the following nice quote (unfortunately forgot from whom):
Patricia Bouyer: On Expressiveness and Complexity in Real-time Model Checking
Metric Temporal Logic (MTL) is a popular extension of Linear Temporal Logic (LTL) with quantitative timing, for which model-checking problem over dense-time models is undecidable. The main culprit for the undecidability is the presence of punctuality, i.e., formulae in which one can talk about exact time moments of events. Thus, punctuality-free fragments of MTL, such Metric Interval Temporal Logic (MITL), are proposed which are decidable. Patricia introduced a new subset of MTL, called coFlat-MTL, which can express properties such as global invariance, bounded response, and some kinds of punctuality (e.g., punctual response), for which model-checking over timed-automata models is in EXPSPACE. She also gave a tableau construction algorithm for this logic.
Antonin Kucera: Controller Synthesis and Verification of Markov Decision Processes
Antonin first showed why we need randomized and history dependent strategies (even bounded memory is insufficient) to control CMDP in order to satisfy qPCTL formulae. Then he presented a study of the complexity of the controller synthesis problem for Markov Decision Processes, which is the following question:
(qPCTL is an extension of CTL, which allows for specifying properties like: with a probability less than .5, a state with a certain property will be reached.) According to his study, if I remember well, the controller synthesis problem for qPCTL(*) formulae is (2-)EXPTIME-complete in the size of the formula and polynomial in the size of the MDP.
Ran Canetti: Composable Formal Security Analysis (Invited Speech)
Ran underscored the fact that the most challenging part of verifying security is to guarantee that protocols remain secure when put in arbitrary contexts and composed with other protocols. He defined a notion of security which basically requires that the observational behavior of a protocol in the presence of an "environment" machine (which can interfere in all possible ways) emulates the behavior of a perfectly secure protocol with a trusted third party. Combining symbolic methods with concrete cryptographic protocols is another aspect of composition theorem. Explicit analysis of all possible combination of such protocols is infeasible.
The message of the talk can be nicely summarized in the following nice quote (unfortunately forgot from whom):
Addendum from Luca: Ran attributed the above quote to Dave Safford.
"In security, the sum of the parts is a hole."
Patricia Bouyer: On Expressiveness and Complexity in Real-time Model Checking
Metric Temporal Logic (MTL) is a popular extension of Linear Temporal Logic (LTL) with quantitative timing, for which model-checking problem over dense-time models is undecidable. The main culprit for the undecidability is the presence of punctuality, i.e., formulae in which one can talk about exact time moments of events. Thus, punctuality-free fragments of MTL, such Metric Interval Temporal Logic (MITL), are proposed which are decidable. Patricia introduced a new subset of MTL, called coFlat-MTL, which can express properties such as global invariance, bounded response, and some kinds of punctuality (e.g., punctual response), for which model-checking over timed-automata models is in EXPSPACE. She also gave a tableau construction algorithm for this logic.
Antonin Kucera: Controller Synthesis and Verification of Markov Decision Processes
Antonin first showed why we need randomized and history dependent strategies (even bounded memory is insufficient) to control CMDP in order to satisfy qPCTL formulae. Then he presented a study of the complexity of the controller synthesis problem for Markov Decision Processes, which is the following question:
Is there a history dependent randomized strategy such that a given model satisfies a given qPCTL(*) formula?
(qPCTL is an extension of CTL, which allows for specifying properties like: with a probability less than .5, a state with a certain property will be reached.) According to his study, if I remember well, the controller synthesis problem for qPCTL(*) formulae is (2-)EXPTIME-complete in the size of the formula and polynomial in the size of the MDP.
Tuesday, July 08, 2008
Best Paper Awards at ICALP 2008
The best paper awards for ICALP 2008 were delivered this evening during the EATCS General Assembly.
The best paper award for track A went to the paper The complexity of Boolean formula minimization by David Buchfuhrer and Christopher Umans. The best student paper for track A was given to Jeff Phillips for his paper Algorithms for epsilon-approximations of Terrains.
The awards for track B were made to the papers
There is a lot more to report from the conference, but time is short right now. Let me just point out that today ICALP 2008 featured a very special event, which was attended by about 300 participants, including the Icelandic Math Olympiad team, high school teachers of mathematics and members of the public at large. Peter Winkler (Dartmouth, USA) delivered a truly outstanding master class on mathematical puzzles entitled Puzzles You Think You Must Not Have Heard Correctly. It is the first time that ICALP features this type of event bringing a TCS conference of this calibre to a wider audience. Anna, Magnús and I are very happy to see how well it all went. Thanks to Peter for a truly inspirational talk!
When Peter presented the "Boxes in Boxes" puzzle, he said that
The best paper award for track A went to the paper The complexity of Boolean formula minimization by David Buchfuhrer and Christopher Umans. The best student paper for track A was given to Jeff Phillips for his paper Algorithms for epsilon-approximations of Terrains.
The awards for track B were made to the papers
- Mai Gehrke, Serge Grigorieff and Jean-Eric Pin. Duality and equational theory of regular languages (best paper) and
- Christian Mathissen. Weighted Logics for Nested Words and Algebraic Formal Power Series (best student paper).
There is a lot more to report from the conference, but time is short right now. Let me just point out that today ICALP 2008 featured a very special event, which was attended by about 300 participants, including the Icelandic Math Olympiad team, high school teachers of mathematics and members of the public at large. Peter Winkler (Dartmouth, USA) delivered a truly outstanding master class on mathematical puzzles entitled Puzzles You Think You Must Not Have Heard Correctly. It is the first time that ICALP features this type of event bringing a TCS conference of this calibre to a wider audience. Anna, Magnús and I are very happy to see how well it all went. Thanks to Peter for a truly inspirational talk!
When Peter presented the "Boxes in Boxes" puzzle, he said that
Magnús remarked that this is definitely true in Iceland for all train stations here. This is an example of logic at its best, and I'll use it next time I have to teach universal quantification over an empty set :-)
At many train stations, post offices and currier services around the world, the cost of sending a
rectangular box is determined by the sum of its dimensions; that is, length plus width plus height.
My Second Day @ ICALP 2008 (Guest Post by MohammadReza Mousavi)
This is the second guest post by MohammadReza Mousavi on ICALP 2008. Thanks to Mohammad for contributing this post! Further information on ICALP may be found at /dev/collective. See here for photos from the conference.
Track B of ICALP started today (7 July) afternoon. My body is not yet totally accustomed to the 24-hours-light scheme here in Reykjavik and thus, I decided take a leave from the morning sessions of Tracks A and C. What you read is a summary of a few talks given at Track B this afternoon. Some of the talks went beyond my limited understanding of their subject matters and thus, you may find inaccuracies in my report of the results, for which I apologize in advance.
Wim Martens: NFA Minimization
There exist well-known efficient state-minimization algorithms for DFA's. It is also known that bisimulation reduction for NFA's is efficient but it does not give you the minimal-state NFA. If I got it well, the bottom line, partially established by the ICALP'08 paper, is that all "interesting" state-minimization problems to non-DFA's (e.g., DFA's with multiple starting states or multiple, no matter how few, transitions with the same label) are NP-hard. By interesting Wim means, if I understood well, those minimizations that can lead to exponential reduction in size.
Hermann Gruber: RE Size
The minimal size of the regular expression for an automaton is known to be exponentially larger than the number of states, given that the alphabet is sufficiently large (due to Ehrenfeucht and Zeiger, JCSS, 1976; preprint available from here). In the present paper, the same result is extended to the case where the alphabet contains at least two elements.
Magnus Johansson: Extended Pi
Magnus presented an interesting extension of Pi in which names are replaced by arbitrary terms which can be equated using arbitrary equational theories (satisfying certain natural properties such as equivariance and equivalence) and also, aliasing for arbitrary terms is allowed (aliasing, or active substitution, basically introduces a new equation). The notion of bisimulation that comes with this this calculus (calculi, parameterized by the equational theory), is a very natural one: it requires the aliases of the two processes to be the same (up to the present equational theory) and the two processes to show the same behavior even under equational theories extended with new equations.
Track B of ICALP started today (7 July) afternoon. My body is not yet totally accustomed to the 24-hours-light scheme here in Reykjavik and thus, I decided take a leave from the morning sessions of Tracks A and C. What you read is a summary of a few talks given at Track B this afternoon. Some of the talks went beyond my limited understanding of their subject matters and thus, you may find inaccuracies in my report of the results, for which I apologize in advance.
Wim Martens: NFA Minimization
There exist well-known efficient state-minimization algorithms for DFA's. It is also known that bisimulation reduction for NFA's is efficient but it does not give you the minimal-state NFA. If I got it well, the bottom line, partially established by the ICALP'08 paper, is that all "interesting" state-minimization problems to non-DFA's (e.g., DFA's with multiple starting states or multiple, no matter how few, transitions with the same label) are NP-hard. By interesting Wim means, if I understood well, those minimizations that can lead to exponential reduction in size.
Hermann Gruber: RE Size
The minimal size of the regular expression for an automaton is known to be exponentially larger than the number of states, given that the alphabet is sufficiently large (due to Ehrenfeucht and Zeiger, JCSS, 1976; preprint available from here). In the present paper, the same result is extended to the case where the alphabet contains at least two elements.
Magnus Johansson: Extended Pi
Magnus presented an interesting extension of Pi in which names are replaced by arbitrary terms which can be equated using arbitrary equational theories (satisfying certain natural properties such as equivariance and equivalence) and also, aliasing for arbitrary terms is allowed (aliasing, or active substitution, basically introduces a new equation). The notion of bisimulation that comes with this this calculus (calculi, parameterized by the equational theory), is a very natural one: it requires the aliases of the two processes to be the same (up to the present equational theory) and the two processes to show the same behavior even under equational theories extended with new equations.
Monday, July 07, 2008
My First Day @ ICALP 2008 (Guest Post by MohammadReza Mousavi)
I am happy to provide a guest post by MohammadReza Mousavi, one of the workshop co-organizers for ICALP 2008, on his first day at ICALP 2008. Thanks to Mohammad for contributing this post!
Sunday July 6, 2008 was my first day at ICALP 2008. The conference was commenced the day before with the first day of the Dynamo workshop, but I had to be at a friend's Ph.D. defense session and an affiliated workshop. Thus, I lost the opportunity of being here right from the beginning. But there is Persian proverb which says: no matter when you catch a fish, it is fresh!
My first day was mostly spent at the SOS'08 workshop. It is nice to see fresh blood in the SOS community; there were a couple of graduate and Ph.D. students present at SOS'08 who have just started with SOS as their research subject. A warm welcome to all of them.
What follows is a biased overview of the talks presented in this very interesting workshop. Bartek and Matthew did an excellent job in organizing and chairing SOS'08; thank you very much Bartek and Matthew.
Vincent Danos: solid state concurrency
Vincent presented a general picture of biological systems and their huge dimensions which make any explicit state-exploration technique totally obsolete. He introduced the basics of the Kappa language which provides an abstract model for the (local) rules of interaction among biological agents. He presented a symbolic probabilistic abstraction for such systems (presented at VMCAI'08). There is a strong similarity between the situation here and that of random graphs as studied in statistical physics.
Observation: I found this talk extremely fascinating and very close and related to the ongoing work on the verification of distributed algorithms such as epidemic and gossiping protocols.
Michele Lorieti: Stochastic extension of process calculus, called CASPIS, for service oriented computing (SOC), which are by the way all the rage. The extension adds rates (for a negative exponential distribution) to synchronization constructs, and the rates are calculate in the same way as in PEPA.
Observation: Mixing synchronization with rates makes the semantics very difficult. Perhaps IMC and Markov Decision Processes are the way to go.
Muck van Weerdenburg: Automating soundness proofs
Muck translates SOS rules and the transfer condition for bisimulation into first order logic formulae and then by feeding a witnessing bisimulation relation for each axiom, the proof tool (initially Coq, then replaced by Muck's own proof tool). He has applied his tool . He even has a web-interface for his prototype.
Observation: Nice work. We need more of this kind of formalized proof environments for SOS.
Gustavo Ospina: Formalisation of C Language Interfaces
I must say I was a bit distracted during this talk. It reported on operational semantics of interfacing between C and another language called Russel, but the details have escaped my mind.
Michel Reniers, SOS with First Order Logic
Michel reported on a nice improvement over ourjoint SOS'07 paper on extending SOS with quantifiers. In his paper (joint with Muck van Weerdenburg), he presents a framework and congruence format for SOS which supports first order logic formulae (with infinitary conjunction) in the premise of the deduction rules.
Bartek and Luca raised the question whether we need such an expressive logic to specify the premises of the SOS rules and whether we can specify the same phenomenon with fragments of first order logic.
Eike Best: Relational Semantics
He presented the relational approach to operational semantics for non-deterministic sequential programs. Then, he presented the standard (denotational) semantics for such programs for both partial and total order semantics using Hoare and Smyth power domains. Then, he gave a generic way of presenting these semantics in a set-theoretic fashion by tailoring the definition of subset relation and relational compositions in each case.
Observation: Very neat talk to the foundations of semantics; reminding me of my first expositions to formal methods.
Dale Miller: Formalizing SOS in Logic
Dale started off by pointing out a dichotomy in the interpretation of computation, namely, computation as model (e.g., function, relation, or LTS) versus computation as deduction (e.g., in lambda calculus and logic programming). Being a logician, he stated his clear preference for the latter interpretation. Then, he gave an overview of syntax, from abstract to concrete, from strings to lambda-trees. Then he gave an introduction to the specification of operational semantics as a logical specification, showing that the traditional treatment of semantics as a logical formulae for nominal formalisms, such as pi calculus, is insufficient for proving impossibility of transitions and as a result bisimulation. He introduced then the nabla operator, as a substitute for universal quantification, which would enable us to prove impossibility of transitions (since it essentially enables us to prove that \lambda x . x cannot be unified with \lambda x .w).
Addendum by Luca: Dale had some great one-liners in his talk. The one I liked best was one he used in his reply to a question from Matthew Hennessy: "The world is too small for two self-dual quantifiers."
Peter Mosses: Implicit Propagation in SOS
SOS specifications often contain "redundant" information, i.e., they carry over lots of information that do not change along a transition or change in a very standand way (the change is propagated from the source of the conclusion to the source of the premise(s) and then from the target of the premises to the target of the conclusion). Peter presented an elegant way of "factoring out" such information and making SOS specs much more readable and also more reusable.
Together with Michel, we presented some initial ideas on writing a textbook about SOS. Peter Mosses suggested creating a wikipedia page for SOS, which is missing at the moment.
P.S.: Arnar updates his photos from ICALP'08 on a daily basis. Thanks to Arnar, Anna, Luca, Magnus and all the organizers for their excellent hard work.
Sunday July 6, 2008 was my first day at ICALP 2008. The conference was commenced the day before with the first day of the Dynamo workshop, but I had to be at a friend's Ph.D. defense session and an affiliated workshop. Thus, I lost the opportunity of being here right from the beginning. But there is Persian proverb which says: no matter when you catch a fish, it is fresh!
My first day was mostly spent at the SOS'08 workshop. It is nice to see fresh blood in the SOS community; there were a couple of graduate and Ph.D. students present at SOS'08 who have just started with SOS as their research subject. A warm welcome to all of them.
What follows is a biased overview of the talks presented in this very interesting workshop. Bartek and Matthew did an excellent job in organizing and chairing SOS'08; thank you very much Bartek and Matthew.
Vincent Danos: solid state concurrency
Vincent presented a general picture of biological systems and their huge dimensions which make any explicit state-exploration technique totally obsolete. He introduced the basics of the Kappa language which provides an abstract model for the (local) rules of interaction among biological agents. He presented a symbolic probabilistic abstraction for such systems (presented at VMCAI'08). There is a strong similarity between the situation here and that of random graphs as studied in statistical physics.
Observation: I found this talk extremely fascinating and very close and related to the ongoing work on the verification of distributed algorithms such as epidemic and gossiping protocols.
Michele Lorieti: Stochastic extension of process calculus, called CASPIS, for service oriented computing (SOC), which are by the way all the rage. The extension adds rates (for a negative exponential distribution) to synchronization constructs, and the rates are calculate in the same way as in PEPA.
Observation: Mixing synchronization with rates makes the semantics very difficult. Perhaps IMC and Markov Decision Processes are the way to go.
Muck van Weerdenburg: Automating soundness proofs
Muck translates SOS rules and the transfer condition for bisimulation into first order logic formulae and then by feeding a witnessing bisimulation relation for each axiom, the proof tool (initially Coq, then replaced by Muck's own proof tool). He has applied his tool . He even has a web-
Observation: Nice work. We need more of this kind of formalized proof environments for SOS.
Gustavo Ospina: Formalisation of C Language Interfaces
I must say I was a bit distracted during this talk. It reported on operational semantics of interfacing between C and another language called Russel, but the details have escaped my mind.
Michel Reniers, SOS with First Order Logic
Michel reported on a nice improvement over our
Bartek and Luca raised the question whether we need such an expressive logic to specify the premises of the SOS rules and whether we can specify the same phenomenon with fragments of first order logic.
Eike Best: Relational Semantics
He presented the relational approach to operational semantics for non-deterministic sequential programs. Then, he presented the standard (denotational) semantics for such programs for both partial and total order semantics using Hoare and Smyth power domains. Then, he gave a generic way of presenting these semantics in a set-theoretic fashion by tailoring the definition of subset relation and relational compositions in each case.
Observation: Very neat talk to the foundations of semantics; reminding me of my first expositions to formal methods.
Dale Miller: Formalizing SOS in Logic
Dale started off by pointing out a dichotomy in the interpretation of computation, namely, computation as model (e.g., function, relation, or LTS) versus computation as deduction (e.g., in lambda calculus and logic programming). Being a logician, he stated his clear preference for the latter interpretation. Then, he gave an overview of syntax, from abstract to concrete, from strings to lambda-trees. Then he gave an introduction to the specification of operational semantics as a logical specification, showing that the traditional treatment of semantics as a logical formulae for nominal formalisms, such as pi calculus, is insufficient for proving impossibility of transitions and as a result bisimulation. He introduced then the nabla operator, as a substitute for universal quantification, which would enable us to prove impossibility of transitions (since it essentially enables us to prove that \lambda x . x cannot be unified with \lambda x .w).
Addendum by Luca: Dale had some great one-liners in his talk. The one I liked best was one he used in his reply to a question from Matthew Hennessy: "The world is too small for two self-dual quantifiers."
Peter Mosses: Implicit Propagation in SOS
SOS specifications often contain "redundant" information, i.e., they carry over lots of information that do not change along a transition or change in a very standand way (the change is propagated from the source of the conclusion to the source of the premise(s) and then from the target of the premises to the target of the conclusion). Peter presented an elegant way of "factoring out" such information and making SOS specs much more readable and also more reusable.
Together with Michel, we presented some initial ideas on writing a textbook about SOS. Peter Mosses suggested creating a wikipedia page for SOS, which is missing at the moment.
P.S.: Arnar updates his photos from ICALP'08 on a daily basis. Thanks to Arnar, Anna, Luca, Magnus and all the organizers for their excellent hard work.
Subscribe to:
Posts (Atom)