Seleccione el siguiente ejercicio del Linear Temporal Logic LTL el cual menciona:
A holds at all states s3k and does not hold at all states s3k+1 , s3k+2 , where k = 0, 1, . . ..
Basandonos en lo siguiente relizaremos el problema:
=holds at all states s3k 
En conclusion A solo tiene los estados 0s3,1s3,2s3,3s3... pero no tiene los estados s3+1,2s3+2
¿s3k? sería más bien usando algo tipo siguiente o next o el reverso de until para argumentar que alguna cosa deje de cumplir por siempre en un cierto momento... Aquí falta abarcar bien ese aspecto temporal en tu formulación. Van 3 pts por el intento.
ResponderEliminar