Segundo parcial 24/11/2022 (IngSoft2)
De Cuba-Wiki
Ejercicio 1
a) Dibuje los LTS para AB y ABC
A = (a -> c -> A). B = (b -> d -> B). ||AB = (A||B)\{c,d}. C = (c -> C). ||ABC = (AB || C).
b) Proponga un LTS que sea débilmente equivalente a AB pero con menos estados. Demuestre que son equivalentes
Para demostrar que son débilmente bisimilaresbasta con dar la relación de bisimilitud: [(0,0), (1,0), (2,0), (3,0)].
(Puede ser difícil ver por qué valen (1,0), (2,0) y (3,0), dejo la justificación de (1,0) a partir de la definición formal, las otras dos son análogas:
Sea Q el LTS de un nodo, 0ab el estado 0 del LTS AB y 0q el estado 0 de Q: - 1ab -a-> 2ab y 0q =a=> 0q y (2,0) esta en la relacion - 0q -b-> 0q y 1ab =b=> 1ab (porque 1 -tau-> 0 -b-> 1) y (1,0) esta en la relacion - 0q -a-> 0q y 1ab =a=> 2ab y (2,0) esta en la relacion
)