MODEL CHECKING

En las últimas dos décadas, model checking ha surgido como un enfoque prometedor y
poderoso para la verificación automática de sistemas. En términos generales, un model
checker es un procedimiento que decide si una estructura M dada es un modelo de una
fórmula lógica φ, es decir, si M satisface φ, abreviado M╞ φ. Intuitivamente, M es un
modelo (abstracto) del sistema en cuestión, típicamente una estructura similar a autómata
finito y φ, típicamente extraído de una lógica temporal o modal, especifica una propiedad
deseable. El model checker luego proporciona un enfoque de botón (push-button) para probar
que el sistema modelado por M disfruta de esta propiedad. Esta automatización completa,
junto con el hecho de que los model checkers eficientes se pueden construir para lógicas
potentes, forma el atractivo del model checking.

La descripción "genérica" anterior de model checking deja algunas preguntas:

 ¿Qué es exactamente un modelo a comprobar?

 ¿Qué tipo de fórmulas se utilizan?
 ¿Cuál es la interpretación precisa de la satisfacción, ╞?

Presentamos un mapa aproximado de las diversas respuestas a estas preguntas y, en el

proceso, presentamos los enfoques principales.

Los diversos enfoques de model checking proporcionan una gran cantidad de procesos de
decisión genéricos que pueden aplicarse a escenarios que van mucho más allá de los
dominios problemáticos para los cuales se inventaron originalmente los enfoques.

La idea es traducir problemas en modelos de estructuras y fórmulas que se puedan resolver

mediante model checking.

1
MODELOS

Un model checking generalmente depende de un modelo discreto de un sistema: el

comportamiento del sistema se representa (de manera abstracta) mediante una estructura
gráfica, donde los nodos representan los estados del sistema y los arcos representan las
posibles transiciones entre los estados. Los gráficos solos son demasiado débiles para
proporcionar una descripción interesante, por lo que están anotados con información más
específica. Hay varios enfoques de uso común, nos centraremos en: las estructuras de Kripke,
donde los nodos se anotan con las llamadas proposiciones atómicas.

Estructuras de Kripke

La estructura de Kripke (KS) sobre un conjunto AP de proposiciones atómicas es una tripla

(S, R, I), donde:

S: Es un conjunto de estados.

R ⊆ S x S: Es una relación de transición.

I: S  2AP: Es una interpretación.

Intuitivamente, las proposiciones atómicas, que formalmente son solo símbolos, representan
propiedades locales básicas de los estados del sistema; I asigna a cada estado las propiedades
que disfruta. Suponemos que un conjunto de proposiciones atómicas AP siempre contiene las
proposiciones verdadero(V) y falso(F) y que, para cualquier estado s, es V ∈ I(s) y F ∉ I(s).
Una estructura de Kripke se denomina total si R es una relación total, es decir, si para todos
los s ∈ S hay un t ∈ S tal que (s; t) ∈ R, de lo contrario, se llama parcial. Para fines del model
checking, S y AP usualmente son finitos.

La Figura 1 muestra una estructura Kripke de ejemplo cuyas proposiciones toman la forma,
var = num; la estructura representa los estados que surgen mientras que los componentes del
programa, x e y, intercambian dos recursos de un lado a otro.

LÓGICAS

La interpretación, I, en un sistema de transición de Kripke define las propiedades locales de

los estados. A menudo también nos interesan las propiedades globales relacionadas con el
comportamiento de transición. Por ejemplo, podríamos estar interesados en las propiedades
de alcanzabilidad, como "¿Podemos alcanzar desde el estado inicial un estado donde se
sostiene la proposición atómica P?" Las lógicas temporales son formalismos lógicos
diseñados para expresar tales propiedades.

2
Las lógicas temporales vienen en dos variantes:

 Tiempo lineal
 Tiempo de ramificación.

Las lógicas de tiempo lineal se ocupan de las propiedades de las rutas. Se dice que un estado
en un sistema de transición satisface una propiedad de tiempo lineal si todas las rutas que
emanan de este estado satisfacen la propiedad. En un sistema de transición etiquetado, por
ejemplo, dos estados que generan el mismo lenguaje satisfacen las mismas propiedades de
tiempo lineal.

Las lógicas de tiempo de ramificación, por otro lado, describen propiedades que dependen de
la estructura de ramificación del modelo. Dos estados que generan el mismo lenguaje pero
utilizando diferentes estructuras de ramificación a menudo se pueden distinguir por una
fórmula de tiempo de ramificación.

Como ejemplo, considere los dos sistemas de transición etiquetados en la Fig. 3, que modelan
dos máquinas expendedoras diferentes que ofrecen té y café.

Ambas máquinas sirven café o té después de insertar una moneda, pero desde el punto de
vista del cliente se debe evitar la máquina correcta, porque esta decide internamente si se
sirve café o té. La máquina izquierda, por el contrario, deja esta decisión al cliente. Ambas
máquinas tienen el mismo conjunto de cálculos (rutas máximas): {(coin, coffee); (coin, tea)}
Por lo tanto, una lógica de tiempo lineal no podrá distinguir las dos máquinas. Sin embargo,
en una lógica de tiempo de ramificación, la propiedad "una acción de café es posible después
de cualquier acción de la moneda.", se puede expresar, lo que diferencia las dos máquinas.

La elección de utilizar una lógica de tiempo lineal o de ramificación depende de las

propiedades que se analizarán. Debido a su mayor selectividad, las lógicas de tiempo de
ramificación suelen ser mejores para analizar sistemas reactivos. Se prefieren las lógicas de
tiempo lineal cuando solo las propiedades de ruta son interesantes, como cuando se analizan
las propiedades de un gráfico de flujo de datos de programas imperativos.

3
Lógicas de tiempo lineal (LTL)

La lógica de tiempo lineal proposicional (PLTL) es la lógica de tiempo lineal prototípica

básica. A menudo se presenta en una forma para ser interpretada sobre las estructuras de
Kripke. Sus fórmulas se construyen de la siguiente manera, donde p abarca un conjunto AP
de proposiciones atómicas:

 p ∈ AP Proposición atómica
 ¬φyφ∧ψ Negación y Conjunción
 X(φ) NeXt
 U(φ, ψ) Until
 F(φ) Finally
 G(φ) Globally

Las fórmulas LTL se interpretan a lo largo de las rutas en una estructura Kripke K = (S, R, I)
sobre AP.

Un camino finito es una secuencia finita, no vacía:

π = (π0,…, πn-1) de estados π0,…, πn-1 ∈ S tal que (πi, πi+1) ∈ R para todo 0 ≤ i < n - 1.

La longitud del camino n se denota con |π|.

Un camino infinito es una secuencia infinita:

π = (π0, π1, π2,…) de estados en S tal que (πi, πi+1) ∈ R para todo i ≥ 0

La longitud de una ruta infinita es ∞.

Para 0 ≤ i < |π|, πi denota el estado i-esimo en la ruta π, e πi es (πi; πi + 1,…), la cola del
camino que comienza en πi. En particular, π0 = π.

Un camino en una estructura Kripke se llama máximo si no se puede extender. En particular,

cada camino infinito es máximo.

En la Fig. 4, presentamos una definición inductiva de cuando una trayectoria, π, en una

estructura de Kripke K = (S, R, I) satisface una fórmula de LTL, φ. Intuitivamente, π satisface
una proposición atómica, p, si su primer estado lo hace.

4
Las proposiciones atómicas representan propiedades locales. ¬ Y ∨ se interpretan de la
manera obvia; se pueden introducir conectivos booleanos adicionales como abreviaturas de la
forma habitual, por ejemplo, φ1 ^ φ2 se puede introducir como ¬ (¬ φ1 ∨ ¬ φ2).

Operador Next

La fórmula X (φ) significa que φ es verdadera en el siguiente estado, π1, después del inicial,
es decir, en π0.

Operador Until

La fórmula U(φ, ψ) (“φ” hasta “ψ”) requiere que ψ se haga verdadera en alguna situación
posterior y que φ sea verdadera en todas las situaciones visitadas anteriormente.

Operador Finally

La fórmula F(φ) se mantiene, si φ ocurre eventualmente, es decir, φ se mantiene en algún

estado de la ruta.

Operador Globally

5
La fórmula G(φ) se mantiene, si G(φ) se cumple globalmente, es decir, en cada estado a lo
largo de la ruta.

Until Fuerte y Débil

U(φ, ψ) este operador a veces se llama "Until fuerte" porque requiere que ψ se haga
verdadera finalmente. Esto es diferente para una variante de la modalidad Until, llamada
"Until débil", porque la fórmula es válida cuando φ es verdadera para siempre. Until Fuerte y
Débil se pueden definir entre sí utilizando F y G:

También son duales (aproximados):

Además, F puede definirse fácilmente en términos de U, y G en términos de WU:

Y F y G son duales:

Mientras que las estructuras básicas de una lógica de tiempo lineal son caminos (rutas), la
pregunta del model checking generalmente se presenta para una estructura Kripke dada. La
pregunta entonces es determinar, para cada estado, si todas las rutas que emanan del estado
satisfacen cierta fórmula.

Formula de Estado Formula de Ruta Formula LTL

(Con f y g fórmulas de ruta) (Con f formula de ruta)

6
PROPIEDADES DE LOS SISTEMAS DE TRANSICIÓN EN LTL

Las fórmulas LTL expresan propiedades de rutas en árboles de cómputo.

Propiedades de alacanzabilidad y seguridad

Un estado se llama alcanzable si hay una ruta de cálculo desde un estado inicial que conduce
a este estado.

La alacanzabilidad es una de las propiedades más importantes de los sistemas de transición en

relación con las propiedades de seguridad. El sistema es seguro si uno no puede alcanzar un
estado en el que se mantiene inseguro.

F inseguro

Entonces, la seguridad del sistema se puede expresar como la no posibilidad de acceso a un

estado que no es seguro, es decir, la propiedad

G ¬ inseguro

Ejemplo: Dada una máquina expendedora

Un comportamiento inseguro sería servir cerveza a un profesor, que puede expresarse

mediante la fórmula

disp = cerveza ∧ cliente = prof

Así, la propiedad de seguridad correspondiente es:

G (disp ≠ cerveza o cliente ≠ prof)

Otra seguridad: siempre hay café o cerveza en el depósito. Se puede expresar mediante la
siguiente fórmula:

G (st_cofee ∨ st_cerveza)

Exclusión mutua

Propiedad de los sistemas concurrentes. Surge cuando dos o más procesos no pueden ingresar
a la misma sección crítica de un sistema concurrente simultáneamente.

Suponiendo dos procesos P1, P2, y la fórmula criticoi, donde i = 1; 2 denota que Pi está en la
sección crítica.

La fórmula de exclusión mutua es:

G ¬ (crítico1 ∧ crítico2)

Para el ejemplo de la máquina expendedora:

“El café y la cerveza no pueden estar en el dispenser simultáneamente”

7
 G ¬ (disp = café ∧ disp = cerveza)

Podemos expresar que un profesor y un estudiante no pueden ser clientes al mismo tiempo:

G ¬ (cliente = estudiante ∧ cliente = prof)

Deadlock

Un programa concurrente se encuentra en una situación de deadlock, cuando no se alcanza un

estado de terminal, y ninguna parte del programa puede continuar.

Se dice que un sistema de transición o estructura de Kripke está libre de deadlocks si ningún
cómputo lleva a un deadlock.

Suponiendo que el conjunto de estados terminales está representado por una fórmula
temporal terminal, podemos expresar la libertad de deadlock mediante la fórmula

G (N ┴ → terminal)

Esta fórmula debe ser cierta en todos los caminos. De hecho, es fácil ver que la fórmula N ┴
significa "no hay un estado siguiente", es decir, no es posible una transición.

Podemos expresar la alcanzabilidad de un estado de deadlock como la existencia de un estado

con la propiedad dual

G (N ┴ ∧ ¬ terminal)

Terminación y finitud

Un sistema de transición o estructura de Kripke se llama de terminación, si cada cómputo

lleva a un estado terminal. La terminación de una estructura Kripke es equivalente a la finitud
de todas las rutas de cálculo. Pero una ruta de cálculo es finita si y solo si contiene un estado
de deadlock. Por lo tanto, la siguiente fórmula expresa que el árbol de cálculo es finito:

FN┴

(Siempre que esta fórmula se mantenga en todos los caminos).

Justicia

El sistema debe pasar de vez en cuando a través de un estado que satisfaga alguna propiedad.

Esto se denomina restricción de Justicia y los cálculos que satisfacen las restricciones de
Justicia se denominan justos.

"El dispenser contiene una bebida infinitamente a menudo"

Si la propiedad de Justicia se expresa mediante una fórmula φ, significa que A se mantiene

infinitamente a menudo en todos los caminos.

GFφ

8
Sensibilidad (Responsabilidad - Responsiveness)

Si cada solicitud es finalmente reconocida (ack):

A (solicitud → N F ack)

Si también queremos que esa solicitud siga siendo válida hasta que se reconozca, la
capacidad de respuesta se puede expresar mediante la fórmula:

A (solicitud → (solicitud ∪ ack))

También podemos exigir que la fórmula de solicitud y la fórmula de reconocimiento sean

mutuamente excluyentes:

A (solicitud → ((solicitud ∧ ¬ ack) ∪ (¬ solicitud ∧ ack)))

Alternancia

Sea π = s0; s1; s2;... un camino. Afirmamos que la fórmula:

P es cierto en los estados pares s0; s2; s4;... y falso en los estados impares s1; s3; s5 en este
camino.

Significa que π0 ╞ P, entonces P es cierto en los estados pares.

LÓGICA DE ÁRBOL DE CÁLCULO (CTL)

La lógica de árbol de computación (CTL) es una lógica temporal basada en lógica

proposicional con una noción discreta de tiempo y solo modalidades futuras. Es una lógica
temporal ramificada que es lo suficientemente expresiva para la formulación de un conjunto
importante de propiedades del sistema. También, es una lógica para la cual existen algoritmos
de model checking más simples y eficientes.

Lamport discute dos lógicas:

 Una lógica simple de tiempo lineal (LTL), y

 Una lógica simple de tiempo de ramificación (CTL).

Cada lógica podría expresar ciertas propiedades que no podrían expresarse en la otra.

La lógica simple de tiempo de ramificación no puede expresar ciertas propiedades de equidad

natural que pueden expresarse fácilmente en la lógica de tiempo lineal.

9
La lógica de tiempo lineal no puede expresar la posibilidad de que ocurra un evento en el
futuro a lo largo de alguna ruta de cálculo.

Emerson y Halpern proporcionaron un marco uniforme para investigar esta cuestión.

Formularon el problema en términos de una única lógica llamada CTL*, que combina
operadores de tiempo lineal y tiempo de ramificación. La relación entre LTL, CTL y CTL* se
presenta en la siguiente figura:

Lógica temporal de ramificación

La semántica de este tipo de lógica temporal se basa en una noción ramificada del tiempo, un
árbol infinito de estados.

Tiempo de bifurcación: En cada punto en el tiempo puede haber varios futuros posibles
diferentes. Cada punto puede así dividirse en varios futuros posibles.

La semántica de una lógica temporal de bifurcación se define en términos de un árbol de

estados dirigido e infinito en lugar de una secuencia infinita. Cada recorrido del árbol, que
comienza en su raíz, representa una única ruta.

 El árbol mismo representa así todos los caminos posibles.

El árbol arraigado en el estado s representa todos los posibles cálculos infinitos en el sistema
de transición que comienzan en s (la raíz).

10
CTL tiene una sintaxis de dos etapas donde las fórmulas en CTL se clasifican en

 Fórmulas de estado, y
 Fórmulas de ruta.

Las fórmulas de estado son afirmaciones sobre las proposiciones atómicas en los estados y su
estructura ramificada.

Las fórmulas de ruta expresan las propiedades temporales de las rutas. Se construyen
mediante los operadores Next-Step y Until. No se pueden combinar con conectivos booleanos
y no se permite la anidación de modalidades temporales.

Permite la expresión de propiedades de algunos o todos los cálculos que comienzan en un

estado. Se denotan los:

 Cuantificador de ruta existencial (denotado con ∃ -Exist)

 Cuantificador de trayectoria universal (denotado con ∀ -All).

La propiedad ∀ F φ denota que existe un cálculo a lo largo del cual se mantiene F φ.

Los cuantificadores de trayectoria universal y existencial pueden ser anidados:

∀ ∃ F Start

Significa: Para cada cálculo siempre es posible volver al estado inicial.

Exist: Se denota E φ y significa que existe un camino que cumple φ.

All: Se denota A φ y significa que todos los caminos cumplen φ

Los operadores temporales F, G, U y WU tienen el mismo significado que en LTL y son

operadores de ruta:

11
Las fórmulas de estado CTL sobre el conjunto AP de proposición atómica se forman de
acuerdo con la siguiente gramática:

Donde a ∈ AP y φ es una fórmula de ruta.

La fórmula de la ruta CTL se forma de acuerdo con la siguiente gramática

φ :: = X φ | φ1 ∪ φ2 (“:: =” significa “Se define como”)

Donde φ, φ1 y φ2 son fórmulas de estado.

Declaraciones sobre estados:

 a ∈ AP Proposición atómica.
 ¬φyφ∧ψ Negación y Conjunción.
 ∃φ Existe un camino que cumple φ.
 ∀φ Todos los caminos cumplen φ.

Declaraciones sobre rutas:

 Xφ El siguiente estado cumple φ.

 φ∪ψ φ se mantiene hasta que se alcanza un estado ψ.

Globally, Finally y Weak Until se pueden definir en términos de operadores Next y Until,
como se mostró antes.

12
Reglas de formación

Reglas de formación para fórmulas de estado:

 Si p ∈ AP, entonces p es una fórmula de estado.

 Si f, g son fórmulas de estado, entonces ¬ f, f ∧ g, f ∨ g son fórmulas de estado.
 Si f es una fórmula de ruta, entonces E f y A f son fórmulas de estado.

Reglas de formación para fórmulas de ruta:

 Si f es una fórmula de estado entonces f es una fórmula de ruta.

 Si f, g son fórmulas de ruta, entonces ¬ f, f ∧ g, f ∨ g, X f, F f, G f, f U g son fórmulas
de ruta.

Las fórmulas de ruta se pueden convertir en fórmulas de estado prefijándolas con el

cuantificador de ruta E o con el cuantificador de ruta A.

Los operadores temporales deben estar precedidos inmediatamente por E o A para obtener
una fórmula de estado legal.

13
Semántica de fórmulas de estado CTL

Definido por una relación tal que s ╞ φ si y solo si la fórmula φ se mantiene en el estado s.

s ╞ a sii a ∈ L (s)

s ╞ ¬ φ sii ¬ (s ╞ φ)

s ╞ φ ∧ ψ sii (s ╞ φ) ∧ (s ╞ ψ)

s ╞ E φ sii π ╞ φ para alguna ruta π que comienza en s.

s ╞ A φ sii π ╞ φ para todas las rutas π que comienzan en s.

Semántica de fórmulas de ruta de CTL

Define una relación ╞ tal que π ╞ φ si y solo si la ruta π satisface φ.

π ╞ N φ sii π[1] ╞ φ

π ╞ φ ∪ ψ sii (∃ j > 0. π[j] ╞ ψ ∧ (∀ 0 ≤ k ≤ j. π[k] ╞ φ ))

Donde π [i] denota el estado si en la ruta π.

Expresividad

El poder expresivo relativo es incomparable.

Justicia

 A (FG p): Es una fórmula de LTL que no se puede expresar en CTL.

Alcance

 AG (EF p): Es una fórmula CTL que no se puede expresar en LTL.

La disyunción de los dos anteriores es una fórmula CTL* que no se puede expresar ni en
CTL ni en LTL.

Vitalidad

 E (GF p) Esa fórmula no se puede expresar en LTL

CTL*

CTL y LTL tienen una expresividad incomparable. Por lo que CTL* es una extensión de
CTL, (Emerson and Halpern). CTL* combina las características de ambas lógicas, y por lo
tanto es más expresivo que cualquiera de ellas. Es una extensión de CTL ya que permite que
los cuantificadores de ruta, E y A, se aniden arbitrariamente con operadores temporales
lineales.

14
La sintaxis de CTL* distingue entre fórmulas de estado y de ruta.

 Las fórmulas de ruta CTL* se definen como fórmulas LTL,

 Las fórmulas de estado CTL* pueden usarse como átomicas.

Relación entre LTL, CTL y CTL*:

Sintaxis

Las fórmulas de estado de CTL * se forman de acuerdo con:

Donde a ∈ AP y φ es una fórmula de ruta.

En CTL*:

∀ φ = ¬ ∃¬ φ Esto no se mantiene en CTL!

Las fórmulas de ruta en CTL* se forman de acuerdo con la gramática:

Donde φ es una fórmula de estado, y φ, φ1 y φ2 son fórmulas de ruta.

En la siguiente figura se muestra CTL* y su sintaxis de construcción:

15
Semántica

Semántica de fórmulas de estado CTL

CTL (SMV) se obtiene de CTL* forzando a los operadores temporales a ser precedidos por
cuantificadores de ruta:

 Si f, g son fórmulas de estado, entonces X f, F f, G f, f U g, son fórmulas de ruta.

La semántica de CTL se define por una relación de satisfacción (indicada por ╞) entre un
modelo M (estructura de Kripke), uno de sus estados s, o una ruta π, y una fórmula φ.

 M, s ╞ f f se cumple en el estado s en la estructura Kripke M.

 M, π ╞ g f se mantiene a lo largo del camino en la estructura Kripke M.

s ╞ a sii a ∈ L (s)

s ╞ ¬ φ sii ¬ (s ╞ φ)

s ╞ φ ∧ ψ sii (s ╞ φ) ∧ (s ╞ ψ)

s ╞ ∃ φ sii π ╞ φ para alguna ruta π que comienza en s.

π ╞ φ sii π[0] ╞ φ

π ╞ φ1 ∧ φ2 sii π╞ φ1 ∧ π╞ φ2

π ╞ ¬ φ sii π[1…] ╞ φ

π ╞ X φ sii (π ╞ φ)

π ╞ φ1 ∪ φ1 sii ∃ j ≥ 0. (π[j…] ╞ φ2 ∧ (∀ 0 ≤ k < j. π[k…] ╞ φ1 ))

16
Propiedades generales de los sistemas concurrentes

Bajo ciertas condiciones:

 Alcanzabilidad: se puede llegar a una situación particular.

 Seguridad: nunca se alcanzará una situación particular.
 Vitalidad: si hay una entrada, siempre habrá una salida.
 Justicia: se dará o no una situación particular, tiempos infinitos.

Estas propiedades no son nada en absoluto, las propiedades de alcanzabilidad y vitalidad son
formas de expresar la justicia. La negación de alcanzabilidad es una propiedad de seguridad.

Las fórmulas CTL más utilizadas

Alcanzabilidad

EF Restart.

Es posible alcanzar el estado de reinicio.

Seguridad

AG ¬ Boom

No es posible alcanzar el estado Boom.

Vitalidad

AG[Req → AF Ack]

Todos los requisitos serán reconocidos.

Justicia

AGAF DeviceEnabled

La propiedad DeviceEnabled se cumple infinitas veces en cada rastreo.

17
MODEL CHECKING SIMBOLICO

Un Diagrama de decisión binaria ordenada (OBDD), aplicado a un gráfico de transición de

estados, es un árbol de decisión ordenada donde se combinan todos los subárboles isomorfos
(gráficamente distintos pero estructuralmente iguales) y se eliminan todos los nodos con hijos
isomorfos con el fin de tener un árbol ordenado y lo más eficiente posible.

Dado un orden de parámetros, el OBDD es único y el tamaño depende fundamentalmente del

orden de las variables.

Algoritmo de Model Checking Simbólico

Cómo representar gráficos de transición de estado con diagramas de decisión binarios

ordenados:

 Asuma que el comportamiento del sistema está determinado por n variables de estado
booleanas v1, v2,..., vn.
 La relación de transición T se dará como una fórmula booleana en términos de las
variables de estado: T = (v1, v2, ...,vn , v’1, v’2, …, v’n)

Donde v1, v2,..., vn representa el estado actual y v’1, v’2,..., v’n representa el siguiente
estado. Ahora T se puede convertir a un OBDD.

Ejemplo

Fórmula booleana para cada relación de transición:

A diferencia del árbol de alcanzabilidad completo en donde a partir de la raíz y las

transiciones de estado se llegaba a todas las secuencias de ejecución que resultaba en una
explosión de transiciones y estados. Con este método se cae en una expresión booleana que
resulta más simple para analizar, modelar y almacenar.

18