¿Qué es la justicia fuerte y la justicia débil en los métodos formales?

Las propiedades de equidad son propiedades de vitalidad que garantizan un comportamiento “justo”. Consideremos el siguiente ejemplo:
Hay un canal (confiable) que conecta un emisor y un receptor. Ahora, queremos garantizar que cuando el remitente envía un mensaje, el receptor lo recibirá, es decir, obtendrá su contenido. Esto se mantendrá cuando asumimos una imparcialidad débil al recibir el mensaje. ¿Por qué?
La imparcialidad débil dice que cuando una acción se habilita (continuamente), la acción se ejecutará (eventualmente). Cuando el remitente envía el mensaje y el mensaje llega al otro extremo del canal, el receptor puede recibir el mensaje (es decir, la acción está habilitada). El receptor podría decidir hacer otra cosa, mientras que la acción aún estará habilitada sin que el receptor lea su contenido. Asumir una imparcialidad débil al recibir el mensaje implica que el receptor puede hacer otra cosa, pero que en algún momento recibirá el mensaje.
En términos de lógica temporal, esto es: FG habilitado (A) -> F A
A veces se usa esta fórmula: FG habilitado (A) -> GF A

Si hay algún punto desde el cual se habilita la acción, se aplicará.

Ahora, la justicia justa implica justicia débil, pero al revés no funciona.
La imparcialidad fuerte relaja la suposición de que la acción necesita ser continuamente habilitada para ser aplicada. En cambio, requiere que esté habilitado infinitamente (posible con intervalos donde no está habilitado).

Considerando el ejemplo anterior, supongamos ahora que el canal no es confiable, es decir, a veces pierde mensajes. Luego, el remitente envía el mensaje, y puede llegar o no al final del canal. Como el remitente no sabe si el mensaje se perdió, continúa enviando la misma copia de ese mensaje (por ejemplo, hasta recibir el acuse de recibo). Ahora, mientras el receptor está haciendo otras cosas, en algunos momentos el mensaje puede estar listo para ser leído, o puede borrarse, pero mientras se envíe el mensaje, habrá infinitos estados en los que el receptor podría leer su contenido. . Luego, suponiendo una fuerte imparcialidad, dice que si la acción de leer el contenido del mensaje está infinitamente habilitada, se hará.

En términos de lógica temporal, esto es: GF habilitado (A) -> F A
A veces se usa esta fórmula: GF habilitado (A) -> GF A

Tenga en cuenta que para una imparcialidad débil hemos escrito FG para la primera parte, mientras que para una imparcialidad fuerte hemos escrito G F.
FG dice que hay un punto en el futuro desde el cual la acción siempre estará habilitada, y GF dice que la acción se habilitará un número infinito de veces (pero no necesariamente continuamente).

Referencias: Introducción a TLA

More Interesting

¿Qué es la matemática profanada y dónde se usa?

¿Es log n lo mismo que O (nlogn)?

Dada la potencia computacional suficiente, ¿serían los objetivos de la mecánica del continuo tan complicados de lograr? Es decir, ¿sería matemáticamente más sencillo modelar sistemas de forma discreta que continua?

¿Cómo hago para hacer investigación de pregrado en CS?

¿Cuáles son algunas aplicaciones del mundo real de min-cut en la teoría de grafos?

Soy un desarrollador, pero me falta mi habilidad matemática. Con un BSc en CS y un MSc en IS, ¿qué debo saber y cómo puedo identificar dónde necesito ayuda?

¿Los libros de texto de lógica formal en idiomas que no usan el alfabeto latino todavía representan proposiciones con P y no con P?

¿En qué secuencia se debe aprender la estructura de datos, el algoritmo y las matemáticas discretas?

¿En qué subáreas de matemáticas debería centrarme para mejorar mis algoritmos en informática?

He reprobado mucho un título de CS, pero la gran emoción de diseñar un algoritmo innovador todavía está en mí, ¿qué debo hacer?

Me equivoqué completamente en mi examen de Matemática discreta. ¿Todavía podré ir a la escuela de posgrado?

¿Cuáles son algunas historias menos conocidas sobre Alan Turing?

¿Cuáles son algunos de los mejores libros sobre Matemática discreta para informática?

Para un número binario [matemático] n [/ matemático], ¿cuál es la probabilidad de que los dígitos contengan 1 consecutivos? Por ejemplo, un número binario de 3 dígitos tiene 8 posibilidades, y 110, 011 y 111 son los 3 escenarios donde hay 1s consecutivos.

¿Por qué el lenguaje de las palabras a * b * es decidible?