Lógica temporal de tiempo alterno

En informática , la lógica temporal de tiempo alterno , o ATL , es una lógica temporal de tiempo ramificado que extiende la lógica de árbol de computación (CTL) a múltiples jugadores. ^{[ 1 ]} ATL describe de forma natural los cálculos de sistemas multiagente y juegos concurrentes . ^{[ 2 ]} La cuantificación en ATL se realiza sobre rutas de programa que son posibles resultados de los juegos. ^{[ 3 ]} ATL utiliza fórmulas de tiempo alterno para construir verificadores de modelos con el fin de abordar problemas como la receptividad, la realizabilidad y la controlabilidad.

En ATL se pueden escribir fórmulas lógicas como por ejemplo:${\displaystyle \langle \langle \{a,b\}\rangle \rangle Fp}$que expresa el hecho de que los agentes a y b tienen una estrategia para asegurar que la propiedad p se mantenga en el futuro, independientemente de lo que hagan los demás agentes del sistema.

ATL* es una extensión de ATL, al igual que CTL* extiende CTL. ATL* permite escribir objetivos temporales más complejos, por ejemplo${\displaystyle \langle \langle \{a,b\}\rangle \rangle (Fp\land Gq)}$. Belardinelli et al. proponen una variante de ATL en trazas finitas. ^{[ 4 ]} ATL se ha extendido con contexto, para almacenar las estrategias actuales jugadas por los agentes. ATL* se extiende con lógica de estrategia.

ATL se ha generalizado para incluir características epistémicas. En 2003, van der Hoek y Woodridge propusieron ATEL: la lógica ATL aumentada con un operador epistémico de la lógica epistémica . ^{[ 5 ]} En 2004, Pierre-Yves Schobbens propuso variantes de ATL con recuerdo imperfecto. ^{[ 6 ]}

No se pueden expresar propiedades sobre objetivos individuales en ATL. Por eso, en 2010, Chatterjee , Henzinger y Piterman introdujeron la lógica de estrategia, una lógica de primer orden en la que las estrategias son ciudadanos de primer orden. ^{[ 7 ]} La lógica de estrategia engloba tanto a ATL como a ATL*.

• Lógica temporal lineal