[CST-2] D CommII and TinC

M.Y.W.Y. Becker mywyb2@cam.ac.uk
Mon, 04 Jun 2001 21:03:18 +0100


--On 04 June 2001 20:52 +0100 Shu Yan Chan <syc22@cam.ac.uk> wrote:
> Topic in Concurrency:
>
> Have we been shown any example of an assertion in Hennessy-Milner Logic
> (P.69) at all?   The definition is sort of recursively defined.  My

HM logic is used to introduce the the modal mu-calculus so it's not really 
that important.

> problem is that, I am assuming that the basic element for those
> assertions would be like those used in CCS or CTL, i.e. it could be a set

You are mixing up process algebras and logics! CCS is not a logic, it's a 
process algebra. HM logic basically is mu-calculus minus the fixed point 
bit. So the axioms of the logic are T, F and possibly sets of processes.

> of state/process. Then, how can we be convince that if an assertion is
> true for B, and B is bisimiliar to C, the assertion would also be true
> for C as well?  If the assertion is just true for state/process B, then
> it would not hold true for C...  Clearly I have some big miss
> understanding somewhere...

If B is an element of the assertion (which is a denotation of a set) why 
shouldn't C also be an element of the assertion?

> Also, the definition of observsation congruent (P.75).  On my notes, I
> have some scribble   on my notes saying if alpha is tau, then the '  => '
> with alpha action in this context does not allow the case of zero
> tau-action for q to become q' ?   Is it what Prof  WInskel said?

Sounds a bit confused, and I can't remember he talked much about that. I 
think it's not examinable anyway.

> Or is
> it just a comment by my supervisor?  Or my own speculation?   More
> importantly, is it correct? Is nil  = tau.nil ?

I suppose "=" means "observation congruent"? Then nil=tau.nil since "=" is 
a superset of "squiggly =", and nil "squiggly=" tau.nil is true.


Mo