Segundo parcial 24/11/2022 (IngSoft2)

De Cuba-Wiki
Revisión del 16:55 4 dic 2022 de Makopia (discusión | contribs.) (ejercicio 1 2p InsgSoft2 2c2022)
(difs.) ← Revisión anterior | Revisión actual (difs.) | Revisión siguiente → (difs.)

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).
LTS composición de A y B, con cuatro estados: 0,1,2 y 3. Las transiciones son: 0 a 1 con etiqueta b, 1 a 0 con tau, 1 a 2 con a, 2 a 1 con tau, 2 a 3 con tau, 3 a 2 con b, 0 a 3 con a, y 3 a 0 con tau.
LTS AB - ejercicio 1a 2parcial 2c2022 IngSoft2
LTS composición de AB y C. Igual al de AB, pero con una transición saliente extra por nodo, que sale del nodo y vuelve al mismo nodo con etiqueta c.
LTS ABC - ejercicio 1a 2parcial 2c2022 IngSoft2

b) Proponga un LTS que sea débilmente equivalente a AB pero con menos estados. Demuestre que son equivalentes

LTS con un nodo, 0 con dos transiciones salientes hacia sí mismo, con etiquetas a y b.
LTS débilmente bisimilar a AB - ejercicio 1b 2parcial 2c2022 IngSoft2

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

)

Obtenido de «https://www.cubawiki.com.ar/index.php?title=Segundo_parcial_24/11/2022_(IngSoft2)&oldid=14804»