Temporal logik kommer i två varianter: linjär-tid temporal logik antar implicit universell kvantifiering över d l vägar som genereras av systemrörelser; förgreningstid temporal logik tillåter explicit existentiell och universell kvantifiering över alla vägar. Vi introducerar en tredje, mer allmän variation av temporal logik: alternerande tid temporal logik erbjuder selektiv kvantifiering över de vägar som är möjliga resultat av spel, såsom spelet där systemet och miljön växlar. Medan linjär-tid och förgrenings-tidslogik är naturliga specifikationsspråk för slutna system, är alternerande tidslogik naturliga specifikationsspråk för öppna system. Till exempel kan vi genom att föregå den temporala operatören "eventuellt" med en selektiv vägkvantifiering specificera att systemet i spelet mellan systemet och miljön har en strategi för att nå en viss stat. Även problemen med mottaglighet, realiserbarhet och kontrollbarhet kan formuleras som modell-kontroll problem för alternerande tid formler. Beroende på om vi medger godtycklig häckning av selektiva vägkvantifierare och temporaloperatörer, får vi de två tidsförskjutningslogikerna ATL och ATL*. Vi tolkar formlerna ATL och ATL* med avseende på två modeller av komposition för öppna system, synkrona och asynkrona. För synkrona system är den expressiva kraften hos ATL utöver CTL utan kostnad: den modellkontrollerande komplexiteten hos synkrona ATL är linjär i systemets storlek och längden på formeln. Den symboliska modellkontrollalgoritmen för CTL sträcker sig med få ändringar till synkront ATL, och med lite arbete, även till asynkront ATL, vars modellkontroll komplexitet är kvadratisk. Detta gör ATL till en självklar kandidat för automatisk verifiering av öppna system. När det gäller ATL* är problemet med modellkontroll nära relaterat till syntesproblemet för linjära tidsformler och kräver dubbelt exponentiellt lång tid för både synkrona och asynkrona system.
Det visades att syftet med sociala lagar kan uttryckas som en alternativtidslogik (ATL) REF-formel, och det sociala rättsproblemet omvandlas till ett ATL-modellkontrollproblem.
Alternating-time temporal logic
{'venue': 'Proceedings 38th Annual Symposium on Foundations of Computer Science', 'journal': 'Proceedings 38th Annual Symposium on Foundations of Computer Science', 'mag_field_of_study': ['Computer Science']}