PhD defense
Ghassan Oreiby
Title of thesis
Temporal Logics for timed control
Members of the Jury
Time and Location
The Defense will take place on
December 8, 2008 at 2pm in salle Renaudeau, Bâtiment Laplace, ENS de Cachan (
Map).
Abstract
The temporal logic ATL has been introduced in the late 90's. More powerful than CTL, using ATL we can express more precise properties that can quantify over strategies of different players in a game context.
In this thesis, we have studied the complexity of model-checking ATL over different kind of games structures and we have shown that the complexity depends on the relying structure. We studied as well the expressivness power of the logic with respect to the operator 'weak until'.
We extended concurrent games with discrete time (or costs), in a way that in the new model, every transition holds a duration.
We developped as well a more general model that envolves clocks the same way as in timed automata, with this richer framework we can express more properties using an exteded version of ATL called TATL that can express timing properties of games. We introduced as well a new logic that extends Timed ATL and called TALTL which can states timed properties and infinite behaviour while remaining decidable.
Keywords: formal verification, ATL, timed games, model-checking, concurrent games, temporal logics.