[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