Alternating-time Temporal Logic-英文文献.pdf

y Alternatingtime Temp oral Logic z x Ra jeev Alur Thomas A Henzinger Orna Kupferman Abstract Temp oral logic comes in two varieties lineartime temp oral logic assumes implicit universal quantication over all paths that are generated by system moves branchingtime temp oral logic allows explicit existential and universal quantication over all paths We intro duce a third more general variety of temp oral logic alternatingtime temporal logic oers selective quantication over those paths that are p ossible outcomes of games such as the game in which the system and the environment alternate moves While lineartime and branchingtime logics are natural sp ecication languages for closed systems alternatingtime logics are natural sp ecication languages for op en systems For example by preceding the temp oral op erator eventually with a selective path quantier we can sp ecify that in the game b etween the system and the environment the system has a strategy to reach a certain state Also the problems of receptiveness realizability and controllability can b e formulated as mo delchecking problems for alternatingtime formulas Dep ending on whether we admit arbitrary nesting of selective path quantiers and temp oral op erators we obtain the two alternatingtime temp oral logics ATL and ATL We interpret the for mulas of ATL and ATL over alternating transition systems While in ordinary transition systems each transition corresp onds to a p ossible step of the system in alternating transition systems each transition corresp onds to a p ossible move in the game b etween the system and the environment Fa