2.1.1 Ejecuciones de un sistema de transición
El comportamiento de sistema de transición ha sido descrito en un nivel intuitivo. Ahora formalizaremos usando la noción de ejecuciones(execution).
Una ejecución describe el posible comportamiento del sistema de transición.
Formalmente:
Definición 2.6. Fragmento de ejecución
Sea TS = (S, Act,→,I, AP, L) un sistema de transición. Un fragmento de ejecución ϱ finito de TS es una secuencia alterna de estados(S) y acciones(Act) que terminan en un estado.
El término fragmento de ejecución puede ser usado para denotar un fragmento de ejecución finito o infinito. El fragmento de ejecución 𝜚= s₀ α₁ … αₙ sₙ (finito) y ⍴= s₀ α₁ s₁ α₂. . .(infinito) pueden ser escritos respectivamente :
Para denotar un fragmento de ejecución finito usamos 𝜚 y para denotar un fragmento de ejecución infinito usamos ⍴ .
Definición 2.7. Fragmento de ejecución máximo e inicial
- Un fragmento de ejecución máximo puede ser un fragmento de ejecución finito que termina en un estado terminal, o simplemente un fragmento de ejecución infinito.
- Un fragmento de ejecución es llamado inicial si el estado en el empieza pertenece al conjunto I.
Ejemplo 2.8. Ejecución de una máquina expendedora de bebidas.
Recordando el ejemplo 2.2. mostrado anteriormente, para simplificar los nombres de acción(action names) los abreviaremos de la siguiente forma:
get_soda→ sget, get_beer→ bget y inset_coin →coin.
Donde :
- S = {pay, select, soda, beer}.
- I = {pay}
- Act = {coin, sget, bget, Ƭ }
Los fragmentos ⍴₁ y 𝜚 son iniciales ya que el estado en el que empieza pertenece al conjunto I, mientras que el estado con el que empieza ⍴₂ no pertenece al conjunto I.
Asumiendo que ⍴₁ y ⍴₂ son infinitos, por lo tanto son máximos. Para que 𝜚 sea máximo dado que es finito, necesita terminar en un estado final y de acuerdo a la definición el sistema no cumple con un estado terminal, por lo tanto 𝜚 no es máximo.
Definición 2.9. Ejecución
Una ejecución de un sistema de transición TS es un fragmento de ejecución máximo e inicial.
En el ejemplo 2.8, ⍴₁ es una ejecución porque es el único que cumple con ser máximo e inicial. Mientras que ⍴₂ y 𝜚 no. Note que ⍴₂ es máximo pero no inicial mientras que 𝜚 es inicial pero no máximo.
Definición 2.10 Estado accesible
Un estado es llamado accesible si hay un fragmento de ejecución que termine en s y empiece en algún estado inicial.
Sea TS = (S, Act,→,I, AP, L) ser un sistema de transición. Un estado s ∈ S es llamado accesible en TS si existe un fragmento de ejecución finito e inicial.
Reach(TS) denota el conjunto de todos los estados accesibles(reachacle) en TS.
Este post es un resumen y anotaciones del libro Principios de Model Checking (Principles of Model Checking)
