2. Modelando Sistemas Concurrentes
Un pre-requisito para la verificación de modelos(model checking) es un modelo del sistema bajo consideración. Este capítulo introduce a los sistemas de transición, una clase estándar de representar sistemas de software y hardware.
Este post es un resumen y anotaciones del libro Principios de Model Checking (Principles of Model Checking)
2.1 Sistemas de transición
Los sistemas de transición son a menudo usados en ciencia de la computación como modelos que describen el comportamiento de los sistemas. Son básicamente grafos donde los nodos representan estados, y las aristas del modelo transiciones (Imagen 1), por ejemplo cambios de estado.
- Un estado describe cierta información sobre un sistema en un momento determinado de su comportamiento.
- Las transiciones especifican como el sistema puede evolucionar de un estado a otro.
Se han propuesto diferentes tipos de sistemas de transición. Se usará el sistema de transición con:
- Proposiciones atómicas(atomic propositions) para los estados, son usadas para formalizar características temporales. Son denotadas por letras al inicio del alfabeto(a, b, c)
- Nombres de acción(action names) para las transiciones, pueden ser usados para describir el mecanismo de comunicación entre procesos. Se usa las letras al comienzo del alfabeto griego(α,β, etc).
Ejemplos de proposiciones atómicas son : “x es igual a 0 ”, o “x es mas pequeño que 200” para alguna variable entera x. Otros ejemplos son “Hay más de un litro de líquido en el tanque”, o “no hay clientes en la tienda”.
Definición 2.1 Sistema de transición
TS del inglés Transition System
Un sistema de transición TS es una tupla (S,Act, →, I, AP, L) donde
- S es un conjunto de estados,
- Act es un conjunto de acciones,
- →⊆ S x Act x S es una relación de transición,
- I ⊆ S es un conjunto de estados iniciales,
- AP es un conjunto de proposiciones atómicas, y
- L : S → 2^(AP) es una función de etiquetado que asigna a cada estado un conjunto de proposiciones atómicas de un AP establecido.
⮞ TS es llamado finito si S, Act y AP son finitos.
El comportamiento de un sistema de transición puede ser descrito de la siguiente manera:
- El sistema de transición empieza en algún estado inicial S₀ ∈ I y evoluciona de acuerdo a la relación de transición ⟶, evoluciona de S →S’ hasta que el siguiente estado no tenga una relación de salida.
- Si el conjunto I está vacío, el sistema de transición no tiene comportamiento ya que no fue seleccionado ningún estado inicial.
- Si el estado tiene más de una transición de salida la siguiente transición es elegida no deterministamente, por lo tanto el resultado no se conoce a prori y no se puede hacer ninguna declaración sobre la probabilidad con la que selecciona una transición.
- De la misma forma cuando I tiene mas de un estado, el estado inicial es elegido no deterministamente.
Ejemplo 2.2 Máquina expendedora de bebidas
El sistema de transición en la siguiente figura modela un diseño de una máquina expendedora de bebidas.
- La máquina puede entregar cerveza o gaseosa.
- Los estados son representados por óvalos y las transiciones por aristas etiquetadas.
- Los nombres de los estados se representan dentro de los óvalos.
- Los estados iniciales son indicados por una fecha entrante sin procedencia.
- S = {pay, select, soda, beer}.
- I = {pay}
- Act = {insert_coin, get_soda, get_beer, Ƭ }
insert_coin denota la inserción de monedas, get_soda y get_beer denotan la entrega de gaseosa y cerveza respectivamente, mientras que las transiciones no interesantes son denotadas por Ƭ que representan alguna actividad interna de la máquina.
La máquina expendedora,de manera no determinista, puede optar por proporcionar cerveza o gaseosa.
Las proposiciones atómicas en el sistema de transición dependen de las propiedades bajo consideración. Por ejemplo si la única propiedad relevante no refiere a la bebida seleccionada la propiedad sería:
“La máquina expendedora solo entrega una bebida después de proporcionar una moneda”
Sería suficiente usar dos elementos como conjunto de proposiciones atómicas.
AP = {paid, drink}
Vamos a definir el uso de el conjunto de acciones Act y proposiciones atómicas AP.
Las acciones solo son necesarias para modelar el mecanismo de comunicación. En los casos en las que las acciones son irrelevantes, por ejemplo cuando representa una actividad interna del proceso, usamos el símbolo Ƭ o en caso que la acción no es relevante se puede omitir la etiqueta de la acción.
AP es siempre escogido dependiendo de las características de interés. Se asume que AP ⊆ S (el conjunto AP está incluido en el conjunto de estados).
Definición 2.3 Predecesores y sucesores directos
Sea TS = (S,Act, →, I, AP, L) un sistema de transición. Para s ∈ S y α ∈ Act , el conjunto de sucesores-α directos de s esta definido como:
El conjunto de predecesores-α de s está definido por:
Este post es un resumen y anotaciones del libro Principios de Model Checking (Principles of Model Checking)
Definición 2.4. Estado terminal de un sistema de transición
Los estados terminales de un sistema de transición TS son estados sin transiciones de salida. Una vez que el sistema descrito por TS alcanza un estado terminal, el sistema completo se detiene.
El estado s en el sistema de transición TS es llamado terminal si y solo si Post(s) = ∅ (si y solo si el conjunto de sucesores directos es vacío).
Para un sistema de transición que modela un programa de forma secuencial, los estados terminales ocurren como un fenómeno natural que representa la terminación de un programa. Por otro lado en el modelado de sistemas de transiciones paralelos los estados terminales se consideran generalmente no deseados.
2.5 Sistemas de transición deterministas
Sea TS = (S, Act, →, I, AP, L) un sistema de transición.
- TS es llamado acción-determinista si | I | ≤ 1 y Post(s, α) ≤ 1 para todos los estados s y acciones α.
- TS es llamado AP-determinista si |I | ≤ 1 and |Post(s) ∩ { s’ ∈ S | L(s ) = A}| ≤ 1 para todos los estados s y A ∈ 2**(AP).
Lee la siguiente parte aquí.(Ejecuciones de un sistema de transición).
