Re: [tlaplus] Re: Meaning of "equivalence" of specifications

[Hemanth Kapila <saihemanth@xxxxxxxxx>]

On Fri, Oct 28, 2022 at 8:33 PM Andrew Helwer <andrew.helwer@xxxxxxxxx> wrote:
>
> Oops forgot to also say the definition of spec equivalence. Two specs are equivalent if they generate the same set of behaviours, optionally with consistent renaming of variables. Saying that spec A implies spec B  (so A implements B) is saying that if you take the set of behaviours generated by A, and project those behaviours to a subset of A's variables (optionally with consistent renaming), then it is the same set of behaviours as generated by B. So if you have A => B and B => A, then A and B are equivalent, because if two sets are subsets of each other then they must be equivalent - so the behaviors of A and B are equivalent when looking at all variables.
>
> Andrew
Is equivalence the same as Bisimulation [0]?
[0]https://en.wikipedia.org/wiki/Bisimulation

-- 
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/CANOK7kudhbzGb-sq5Be73DaZVZWXXVK%2BGqQt_6BqLpW0TW-F6g%40mail.gmail.com.