IngSoft2 2recu 05-12-22
De Cuba-Wiki
Ejercicio 1[editar]
a) Dibuje los LTS para A, B y AB[editar]
property A = (a -> c -> A) + {b}.
B = (c -> B).
||AB = (A || B).
Resolución[editar]
TODO
b) Diga si los siguientes LTS son bisimilares. Justifique[editar]
A = (a -> (b -> A | c -> A)). B = (a -> b -> B | a -> c -> B).
Resolución[editar]
TODO
Ejercicio 2[editar]
En el siguiente ejemplo, el proceso TWOCOIN satisface las propiedades P y Q? Explique.[editar]
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[editar]
TODO
Ejercicio 3[editar]
Verdadero o Falso? Justifique.[editar]
- a) []<>p es una propiedad de safety y una propiedad de liveness.
- b) ([]p) -> <>q es equivalente a [](p -> <>q).
Resolución[editar]
TODO
Ejercicio 4[editar]
Se perdio en la matrix porque lo escribieron en el pizarron ¯\_(ツ)_/¯[editar]
Resolución[editar]
TODO
Ejercicio 5[editar]
Dado el büchi generalizado definido mas abajo, aplique el procedimiento para definir un büchi no-generalizado[editar]
- 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[editar]
TODO
