Agent Interval Temporal Logic

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.