Talk:Simulation preorder

From Wikipedia, the free encyclopedia

I think that there is an error in the generalization of simulation to two separate labeled state transition systems. In particular, it seems odd that one would take the disjoint union of the labels of the two systems, for surely the simulation relation would then be empty.

[edit] Largest simulation?

I do not understand why \leq is a simulation, since p \leq q is defined to mean there is a simulation R such that qRp -- I would have thought it would be pRq. It seems clear to me that if it were defined the other way around, it would be a simulation, and in fact it would be the union of all simulations and hence the largest simulation. Claiming that \leq as given is the largest simulation would thus indicate that it is the same as the inverse relation \geq, which is clearly not true since similarity is not symmetric. Clearly I am missing something critical here, but even so it points to a weakness in the article!

I don't dispute the definitions (I looked them up in Milner's Communicating and Mobile Systems: the π-calculus to be sure), but if it is true that \leq is a simulation I think the article needs to give the proof. Cjoev 21:28, 13 April 2006 (UTC)

I think (please correct me if I'm wrong) that your confusion is arising due to a change in symbol ordering in the article. It begins by talking about pRq. However, the definition of simulation is given as (quoting from the article):
Given two states p and q in S, p simulates q, written q ≤ p if there is a simulation R such that (q, p) ∈ R. In such case p and q are said to be similar and ≤ is called the similarity relation.
That text reverses the order of p and q in the simulation expressions. I believe it is saying what you thought it should say (i.e. p \leq q defined as R such that pRq). Should be and easy fix to make. Or perhaps I'm missing something... --Allan McInnes (talk) 23:05, 13 April 2006 (UTC)
You're right, I did not notice that. Okay, let's see if I've got this straight. If p simulates q, then there is a simulation R such that (q,p) ∈ R, which means that if q \to q' then there is a p' such that p \to p' and (q',p') ∈ R. Thus if p simulates q, then p can match any step q can take, up to R. Fair enough. Making "≤" the inverse of "simulates" ensures that ≤ is a simulation (and clearly the largest one). Also fine. Is there any reason we can't switch around the q's and p's so that every time we write something of the form "(_,_) ∈ R" in these definitions they are in the same order? Surely that would be less confusing. Cjoev 00:42, 14 April 2006 (UTC)
Your summary reflects my understanding of simulation. I have absolutely no idea why the p's and q's are reversed halfway through the article. It does make things confusing. I was going to suggest making things more consistent. I guess this is a good indication that we all need to mind our p's and w's ;-) -- Allan McInnes (talk) 04:10, 18 April 2006 (UTC)