Characteristic Formulae (continued)

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

A classic result on characteristic formulae was obtained in the paper

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

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

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

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

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

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

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

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

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

Bulletin of the EATCS, October 2006

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

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

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

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

Characteristic Formulae

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

New Rector at Reykjavík University

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

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

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

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

Fingers crossed.

Predicting the Future

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

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

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

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

Thanks for the further publicity Timothy!

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

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

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

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

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

Spinoza

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

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

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

Spinoza wrote:

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

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

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

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

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

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

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

The Number of Labelled Trees over n Nodes

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

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

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

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

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

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

Advice from David Patterson

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

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

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

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

Work at home alone during those time slots

Do creative work uninterrupted at most creative time

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

Other pieces of advice from him include the following nuggets.

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

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

Make daily, weekly, semester to do lists

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

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

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

Travel is #1 time synch; budget it appropriately

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

Do the Patterson rules apply to your work practices?

Workshop on Emerging Trends in Concurrency Theory

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

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

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

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

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

Book off to the Publisher

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

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

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

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

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

Brief News from the Math World

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

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

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

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

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

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

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

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

Process Algebra on Lambda the Ultimate

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

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

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

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

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

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

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