Friday, March 16, 2007

Computing Degrees and Careers Information from the ACM

Following up on my previous post, I just saw that the ACM has made available a new brochure to prepare High School students for careers in computing: http://computingcareers.acm.org. The brochure describes the major areas of study available in the field, as well as a wide range of career
opportunities. Of note is also the information on the web site, including Frequently Asked Questions and Top 10 Reasons to Major in Computing.

I will be using this material in my efforts to attract Icelandic students to computer science. I must freely admit that, with all due respect to civil engineering, I find it very difficult to understand why students choose that field of studies in large numbers, and do not even consider computer science. As my Latin ancestors would have said, "De gustibus non disputandum est" ("There is no arguing about tastes").

Thursday, March 15, 2007

Concurrency on Ars Mathematica

The latest post on Ars Mathematica, a very interesting math blog, features concurrency theory! The post mentions a position paper by Samson Abramsky published in the ENTCS volume Essays on Algebraic Process Calculi, which I coedited with Andy Gordon.

It is good to see mathematicians referring to concurrency theory, even if just on their blogs and for a quote from André Weil :-)

Wednesday, March 14, 2007

Enticing Students to Learn CS

It is that time of the year again. Applications are open, and we eagerly monitor the number of students that have elected to apply for one of the degree courses we offer (two year Diploma in Applied Computing, BSc in CS, BSc in Software Engineering, and MSc in CS). The department of CS at Reykjavík University is by far the best in the country, and one of the very best in all areas of science. (I must freely admit that there are only three CS departments in Iceland, so being the best might not mean much after all :-)) There are plenty of well-paid, exciting jobs available out there for CS graduates, and our graduates have many job offers to choose from. Computing is the heart of modern life and society, and offers an unmatched breadth of engaging problems to work on, and the potential for lifelong learning. As Jeannette Wing puts it in her piece on computational thinking, "to reading, writing, and arithmetic, we should add computational thinking to every child’s analytical ability."

Based on these (for us obvious) premises, one would expect student enrollments in our CS degrees to be increasingly high. Unfortunately, as of today, the figures paint a totally different, and utterly inexplicable and depressing, story. The number of applications is at an all-time low, and we are considering many plans to try and stop the rot. At the same time, enrollment in several engineering degrees is increasing. Even female students are now considering engineering as a viable subject to study. Instead, CS does not seem to cross their mind at all.

Could this have to do with the totally wrong equation "computer science = programming"? And what about the stereotype that a computer scientist is an autistic, male, sun-avoiding, coke-drinking nerd who programs and fixes computers all day? I have no answers to these questions. These days I am putting on my travelling salesman clothes, and give (hopefully energetic) talks on the beauty and importance of CS to a few high-school students who bother to show up. Whether this will have any effect I do not know. What I do believe is that it is time to send out the powerful message that computer science is the science of the 21st century Renaissance man. No other science today touches on so many others, and on society as well. What we need are more people like David Harel and Jeannette Wing who have the courage to explain CS and its basic ideas to the rest of society, including our fellow scientists---many of whom just consider computing as a useful technology.

Let's pick up the gauntlet, and put pen to paper.

Friday, March 09, 2007

Some Results on BPA with Interrupt

In case anyone is interested, I recently posted on my recent papers page a study of the equational theory of BPA with the interrupt operator. (See Luca Aceto, Silvio Capobianco and Anna Ingolfsdottir. On the Existence of a Finite Base for Complete Trace Equivalence over BPA with Interrupt. ) This is the same language Anna and I studied in a very pleasant collaboration with Wan Fokkink and Sumit Nain that eventually led to a TCS publication. In that paper we showed that, modulo bisimilarity, there is no finite collection of sound equations that can prove all of the valid closed equations. This holds true even in the presence of a single action.

In the present paper we show that, unlike bisimilarity, complete trace equivalence affords a finite, ground-complete axiomatization, provided that the set of actions is finite. Moreover, we show that, when the set of actions is a singleton, the interrupt operator is a derived BPA-operator, and that complete trace equivalence affords a finite complete axiomatization over BPA with interrupt.

In the presence of at least two distinct actions, we isolate a collection of valid equations. A proof of their (in)completeness has so far escaped us. Feel free to get in touch with me if you have any idea on how to prove this!



Saturday, March 03, 2007

The Equational Theory of Timed CCS

A couple of weeks ago, I posted a paper on my recent publications page presenting some negative results on the equational theory of Wang Yi's Timed CCS (TCCS) modulo timed bisimilarity. The paper, Impossibility Results for the Equational Theory of Timed CCS, is coauthored with Anna Ingolfsdottir and MohammadReza Mousavi. (So my Mousavi number is now 1.)

The aim of the paper is to revisit the study of the equational theory of parallel composition in TCCS by obtaining results in the spirit of those that Faron Moller showed for Milner's CCS. We prove that timed bisimilarity is not finitely based over TCCS. Moreover, unlike in the setting of CCS, adding two "natural" variations on the (timed) left-merge operator to TCCS does not yield a finitely axiomatizable theory.

In passing, we sharpen the so-called Gap Theorem of J.-C. Godskesen and Kim G. Larsen by showing that it holds also in the setting when the set of actions is a singleton. Unlike the proof of the original result by those authors, which goes via a translation to timed automata, ours is entirely process algebraic.

Thanks to Anna and Mohammad for a pleasant, instructive and humbling collaboration. I, for one, am always overawed by the fragility of these results. One has to be very careful in making sure that the technical details work. An apparently innocuous change in the semantics of the operators can make a huge difference in their properties, and thus in the validity of the statements one is trying to prove. Our ICE-TCS seminar speaker yesterday, Freyja Hreinsdóttir, quoted a mathematician as referring to a conjecture as being "obviously true, but unproven". I am afraid that I do not trust those statements. For what it is worth, my "obviously true, but unproven" conjectures turn out to be false more often than not :-(.


Thursday, March 01, 2007

Ready to Preorder

Ready to Preorder: Get Your BCCSP Axiomatization for Free! is the Amazon.com-sounding title of a recent paper by Wan Fokkink, Anna Ingolfsdottir and yours truly. This paper had a nine-month gestation period. We began working on it when Wan paid a visit to Iceland for a week in late May-early June 2006 to deliver a talk at our second ICE-TCS Theory Day, but the paper was only completed in February 2007.

In the paper we offer an algorithm for turning an axiomatization for a behavioural preorder in the linear time-branching time spectrum that includes the ready simulation preorder into an axiomatization for the kernel of the preorder. The algorithm preserves finiteness, ground-completeness and omega-completeness of the axiomatization that it receives as input. The proof of its correctness relies on an analysis of the so-called cover equations for the semantics in the spectrum we study in the paper.

I thoroughly enjoyed working on that paper. The development of the technical details in that work reminded me yet again of a few valuable lessons that I tend to forget when I feel that I am short of time and that I badly need to produce some research output to keep my conscience at bay.
  1. It is easy to make mistakes in proofs unless one is very careful in checking even the seemingly most obvious of claims. (This is what happens to me at least.)
  2. Haste is never a good advisor.
  3. When I feel that a paper is done, I should let it rest for a day, and proof read it once more.
I feel that I need this self-advice more than ever :-) Reading Terence Tao's General Advice on Submissions is a reminder of what I should be doing. I hope that I do not fall way too short of the Platonic ideals Tao sets forth.

Thanks again to Anna and Wan, the coauthors with whom I have written the largest number of papers, for another very instructive and pleasant collaborations. I hope that there will be another one in the near future.