Lógica de árbol computacional justa

La lógica de árbol computacional justa es la lógica de árbol computacional convencional estudiada con restricciones de equidad explícitas.

Esto declara condiciones tales como que todos los procesos se ejecutan infinitamente. Si consideramos que los procesos son P _i , entonces la condición se convierte en:

${\displaystyle \bigwedge GFP_{i}}$

En este caso, si un proceso solicita un recurso infinitamente a menudo (R), se le debería permitir obtener el recurso (C) infinitamente a menudo:

${\displaystyle \bigwedge (GFR\longrightarrow GFC)}$

Consideremos un modelo de Kripke con un conjunto de estados F. Un camino${\displaystyle \pi =s_{o},s_{1}\dots }$Se considera un camino justo si y solo si el camino incluye a todos los miembros de F infinitas veces. La verificación de modelos CTL justa restringe las verificaciones solo a caminos justos. Hay dos tipos de cuantificadores justos:

1. M _f , s _i |= A${\displaystyle \phi }$si y solo si${\displaystyle \phi }$se mantiene en todos los caminos justos.

2. M _f , s _i |= E${\displaystyle \phi }$si y solo si${\displaystyle \phi }$se mantiene en uno o más caminos justos.

Un estado justo es aquel del que se origina al menos un camino justo. Esto se traduce en M _f , s |= EGtrue.

Un componente fuertemente conectado (CFC) de un grafo dirigido es un subgrafo fuertemente conectado maximal: todos los nodos son alcanzables entre sí. Un CFC equitativo es aquel que tiene una arista que apunta a al menos un nodo para cada una de las condiciones de equidad.

Para comprobar si existe un EG justo para cualquier fórmula,

1. Calcula lo que se denomina la denotación de la fórmula φ : el conjunto de estados tales que M, s |= φ .
2. Restringir el modelo a la denotación.
3. Encuentra el SCC justo.
4. Obtén la unión de los 3 (arriba).
5. Calcula los estados que pueden formar parte de la unión.

La caracterización del punto fijo de Exist Globally viene dada por: [EGφ] = ν Z .([φ] ∩ [EXZ ]), que es básicamente el límite aplicado según el teorema de Kleene . Para caminos justos, se convierte en [Ef Gφ] = ν Z .([φ] ∩ _{Fi ∈FT} [EX[E(ZU(Z ∧ Fi ))]), lo que significa que la fórmula se cumple en el estado actual y en los estados siguientes y en los siguientes a los siguientes hasta que se cumplan todos los miembros de las condiciones justas. Esto significa que la condición es equivalente a una especie de punto de aceptación donde la condición de aceptación es el conjunto completo de condiciones justas.

• Emerson, EA; Halpern, JY (1985). "Procedimientos de decisión y expresividad en la lógica temporal del tiempo ramificado" . Journal of Computer and System Sciences . 30 (1): 1– 24. doi : 10.1016/0022-0000(85)90001-7 .
• Clarke, EM ; Emerson, EA y Sistla, AP (1986). "Verificación automática de sistemas concurrentes de estados finitos mediante especificaciones de lógica temporal" . ACM Transactions on Programming Languages ​​and Systems . 8 (2): 244– 263. doi : 10.1145/5397.5399 . S2CID 52853200 .