Abstract:
Alternating-Time Temporal Logic (ATL), introduced by Alur, Henzinger and
Kupferman, is a logic involving coalitions of agents performing actions which cause
a state change in a turn-based time system. There have been game theoretic ex-
tensions on ATL, and they are very good at specifying systems of multiple agents
cooperating or competing in a game-like situation. Unfortunately neither ATL nor
its extensions are able to capture the idea of gradual change, or duration of actions
or events. The concurrent game model of ATL operates like a turn based game,
with sets of agents taking their turn, and then the environment changing based
on their actions, before they take their next turn. The fact that some actions
take longer than others, or that sometimes a state changes gradually, rather than
immediately, is not representable in ATL. As an example, take a train entering
a tunnel. Before the train enters the tunnel, it is outside the tunnel, after it has
entered the tunnel, it is inside the tunnel, but for the few seconds it takes the
train to enter the tunnel, it is neither inside nor outside the tunnel. ATL cannot
represent this basic intuitive truth.
A family of logics called Interval Logic (IL) use finite state sequences called
“intervals”, which allow it to describe a more continuous model of time, rather
than a discrete state based one such as ATL. This allows it to capture the idea of
gradual change, of a train entering a tunnel, and the fact that actions and events
have various durations. Most of the IL formulations do however not have any way
of distinguishing multiple agents acting at the same time.
Both of these logics - ATL and IL - are useful for specific things, but combining
them might produce new applications which are not possible when only using the
one or the other. In this dissertation we present one such possible combination,
called Agent Interval Temporal Logic (AITL). AITL combines the notion of agents,
coalitions and strategies from ATL with the interval based model of time from IL,
thus creating a new logic which might have some powerful applications in a wide
range of areas in which gradual change and multiple agents acting at the same
time can both be accommodated.
