Date and Time: Thursday, 27 August 2009, 11:15 - 12:15

Location: HG 6.96

Speaker: Rob van Glabbeek (NICTA, Australia)

Title: The coarsest liveness preserving congruence for parallel composition

Abstract:

In this talk I characterise the coarsest congruence on labelled transition systems that respects simple liveness properties. A simple liveness property assumes that our alphabet of atomic actions contains an action "g" (for "good") and says that "something good will eventually happen", i.e. that every complete or infinite trace from a process p will contain this action g. A semantic equivalence ~ respects this simple liveness property iff whenever p ~ q and q has the property, then so does q.

It is already known that under a global fairness assumption (KFAR) the coarsest congruence (for partially synchronous parallel composition and hiding operators) is "fair testing" or "should testing". So here I will investigate the situation without fairness, assuming that if our transition system displays a tau-loop, the represented system may actually diverge and not progress past that point.

This very same question has been addressed before by De Nicola and Hennessy, and they characterised the coarsest congruence as "must-testing", which coincides with the CSP failures equivalence (with catastrophic divergence).

However, they didn't consider parallel composition. Instead they used an interleaving operator. The difference is that if we take a system P that surely will do an action "g" and put it in parallel with a system D that merely does a tau-loop and never interacts with P in any way, them the parallel composition (P || D) will still surely do a "g". The interleaving (P I D) on the other hand may schedule a tau-step from D all the time, so that "g" never happens.

It turns out that requiring ~ to be a congruence for the interleaving operator leads to powerful distinctions between processes, that cannot be made when merely requiring a congruence for parallel composition. But the reverse is also true, so I obtain a congruence that is incomparable with must-testing, and in fact with all finer equivalences from my spectrum II paper.