TLA+
Durante la sesión de hoy vimos una breve introducción a una de las aplicaciones más útiles de la Lógica Modal: la Lógica Temporal de Acciones.
Vimos algunos ejemplos en la herramienta TLA+ y cómo se puede usar a manera de model-checker.
Material
Durante la sesión utilicé la herramienta TLA+.
El código utilizado se puede encontrar en el siguiente repositorio: jpyamamoto/m_formales.