IngSoft2 2recu 05-12-22

Ejercicio 1

a) Dibuje los LTS para A, B y AB

property A = (a -> c -> A) + {b}.
B = (c -> B).

||AB = (A || B).

Resolución

TODO

b) Diga si los siguientes LTS son bisimilares. Justifique

A = (a -> (b -> A | c -> A)).
B = (a -> b -> B | a -> c -> B).

Resolución

TODO

Ejercicio 2

En el siguiente ejemplo, el proceso TWOCOIN satisface las propiedades P y Q? Explique.

TWOCOIN = (pick -> COIN | pick -> TRICK).
TRICK = (toss -> heads -> TRICK |
         toss -> heads -> TWOCOIN).
COIN = (toss -> heads -> COIN |
        toss -> tails -> COIN).

assert P = []<>tails.
assert Q = ([]<>pick) -> ([]<>tails)

Resolución

TODO

Ejercicio 3

Verdadero o Falso? Justifique.

• a) []<>p es una propiedad de safety y una propiedad de liveness.
• b) ([]p) -> <>q es equivalente a [](p -> <>q).

Resolución

TODO

Ejercicio 4

Se perdio en la matrix porque lo escribieron en el pizarron ¯\_(ツ)_/¯

Resolución

TODO

Ejercicio 5

Dado el büchi generalizado definido mas abajo, aplique el procedimiento para definir un büchi no-generalizado

• Estados = {0, 1}
• Alfabeto = {a, b}
• Transiciones = {(0, a, 1), (1, b, 0), (0, b, 0)}
• Estado inicial = 0
• Estados de aceptacion = {{0}, {1}}

Resolucion

TODO