Lógica temporal de tiempo alterno

Tipo de lógica temporal

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 cómputo (CTL) a múltiples jugadores. ^[1] La ATL describe naturalmente los cálculos de sistemas multiagente y juegos concurrentes . ^[2] La cuantificación en ATL se realiza sobre rutas de programas que son posibles resultados de los juegos. ^[3] La 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.

Ejemplos

Se pueden escribir fórmulas lógicas en ATL tales que expresen 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 estén haciendo los demás agentes del sistema. ${\displaystyle \langle \langle \{a,b\}\rangle \rangle Fp}$

Extensiones y variantes

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

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

En ATL no es posible expresar propiedades sobre objetivos individuales. Por eso, en 2010, Chatterjee , Henzinger y Piterman introdujeron la lógica de estrategias, una lógica de primer orden en la que las estrategias son ciudadanos de primer orden. ^[7] La ​​lógica de estrategias abarca tanto a ATL como a ATL*.

Véase también

• Lógica temporal lineal

Referencias

1. Alur, Rajeev ; Henzinger, Thomas A. ; Kupferman, Orna (1997). "Lógica temporal de tiempo alterno". Actas del 38.° Simposio Anual sobre Fundamentos de la Ciencia de la Computación . IEEE Computer Society. págs. 100–109. doi :10.1109/SFCS.1997.646098. ISBN 0-8186-8197-7.
2. van Drimmelen, Govert (2003). "Satisfacción en lógica temporal de tiempo alterno". Actas del 18.º Simposio anual IEEE sobre lógica en informática . IEEE Computer Society. doi :10.1109/LICS.2003.1210060. ISBN 0-7695-1884-2.
3. Alur, Rajeev; Henzinger, Thomas A.; Kupferman, Orna (2002). "Lógica temporal de tiempo alterno". Revista de la ACM . 49 (5): 672–713. doi :10.1145/585265.585270. S2CID  15984608.
4. Belardinelli, Francesco; Lomuscio, Alessio; Murano, Aniello; Rubin, Sasha (2018). "Lógica temporal de tiempo alterno en trazas finitas": 77–83. {{cite journal}}: Requiere citar revista |journal=( ayuda )
5. van der Hoek, Wiebe; Wooldridge, Michael (1 de octubre de 2003). "Cooperación, conocimiento y tiempo: lógica epistémica temporal de tiempo alterno y sus aplicaciones". Studia Logica . 75 (1): 125–157. doi :10.1023/A:1026185103185. ISSN  1572-8730. S2CID  10913405.
6. Schobbens, Pierre-Yves (1 de abril de 2004). "Lógica de tiempo alterno con recuperación imperfecta". Notas electrónicas en informática teórica . LCMAS 2003, Lógica y comunicación en sistemas multiagente. 85 (2): 82–93. doi : 10.1016/S1571-0661(05)82604-0 . ISSN  1571-0661.
7. Chatterjee, Krishnendu ; Henzinger, Thomas A.; Piterman, Nir (1 de junio de 2010). "Strategy logic" (PDF) . Información y computación . Número especial: 18.ª Conferencia internacional sobre teoría de la concurrencia (CONCUR 2007). 208 (6): 677–693. doi :10.1016/j.ic.2009.07.004. ISSN  0890-5401.