Tidslogik för alternerande tid
Inom datavetenskap är alternating-time temporal logic , eller ATL , en temporal logik för förgrening av tid som utökar beräkningsträdlogik (CTL) till flera spelare. ATL beskriver naturligtvis beräkningar av multi-agent system och multiplayer videospel . Kvantifiering i ATL går över programvägar som är möjliga resultat av spel. ATL använder formler med alternerande tid för att konstruera modellkontroller för att lösa problem som mottaglighet, realiserbarhet och kontrollerbarhet.
Exempel
I ATL kan vi skriva logiska formler som som uttrycker det faktum att agenterna a och b ha en strategi för att säkerställa att egenskapen p behåller i framtiden, oavsett vad de andra agenterna i systemet utför.
Tillägg och varianter
ATL* är förlängningen av ATL, eftersom CTL* utökar CTL. ATL* tillåter att skriva mer komplexa tidsmässiga mål, till exempel . Belardinelli et al. föreslår en variant av ATL på finita spår. ATL har utökats med sammanhang för att lagra de nuvarande strategierna som spelas av agenterna. ATL* utökas med strategilogik.
ATL har generaliserats till att inkludera epistemiska drag. 2003 föreslog van der Hoek och Woodridge ATEL: logiken ATL utökad med en epistemisk operator från epistemisk logik . 2004 föreslog Pierre-Yves Schobbens varianter av ATL med ofullkomlig återkallelse.
I ATL kan vi inte uttrycka egenskaper om individuella mål. Det är därför som Chatterjee , Henzinger och Piterman 2010 introducerade strategilogik, en första ordningens logik där strategier är första ordningens medborgare. Strategilogik subsumerar både ATL och ATL*.