Christophe Chareton

I am a qualifieded doctor from Université de Toulouse in Toulouse (France).

Topics of interest

PhD Thesis

I defended my PhD thesis on June 20th 2014. (Abstract in french) (Abstract in english) (Slides) (Manuscript)




Can be found here.


A Formal Treatment of Agents, Goals and Operations using Alternating-Time Temporal Logic

The aim of this talk is to present a formal framework for actor- and goal-oriented requirements engineering modelling. To do so, we define Khi, a core modelling language, as well as its semantics in terms of a strategy logic we call SLsc. Actors, concrete active entities, are defined by their capabilities. They also pursue behavioural goals that are realised by operations. Then a relation of assignment, between (coalitions of) actors and roles (sets of operation specifications) is defined. We highlight the importance of this relation by exhibiting three "assignment problems" and we define criteria for their correctness. They are modalities about the effective ability of (coalitions of) actors to play their assigned roles. The assignment problems reduce to the satisfaction of Slsc formulas in a structure derived from the capabilities of actors. Thanks to the properties of SLsc, we end up with a decidable procedure for the assignment problems. We illustrate our approach using a toy example featuring a satellite-based Earth observation mission.(Slides)

Vers une sémantique des jeux pour un langage d’ingénierie des exigences par buts et agents

Cet exposé propose des structures d’interprétation pour le langage KHI, un langage de modélisation pour l’ingénierie des exigences, qui formalise notamment les notions d’agents, de buts et d’opérations. Deux notions d’agents s’y confrontent : les acteurs, qui sont les agents présents et décrits par leurs capacités d’action sur le système, et les rôles, qui décrivent le comportement attendu des agents pour la réalisation des buts. Les rôles sont ensuite assignés à des acteurs ou des coalitions d’acteurs. La capacité effective des coalitions à jouer les rôles qui leur sont assignés fournit donc un critère de correction du modèle, on appelle le problème relatif problème de l’assignation. KHI a une sémantique formelle dans un fragment de la logique temporelle multiagents ATL*, nommé ATLKHI . Nous décrivons les modèles sémantiques qui permettent d’interpréter ATLKHI et de réduire le problème de l’assignation à un problème de model-checking.(Slides)

Updatable Strategy Logic

This presentation is about temporal multi-agent logics. Several of these formalisms have been already presented (ATL-ATL*, ATLsc, SL). They enable to express the capacities of agents in a system to ensure the satisfaction of temporal properties. Particularly, SL and ATLsc enable several agents to interact in a context mixing the different strategies they play in a semantical game. We generalize this possibility by proposing a new formalism, Updating Strategy Logic (USL). In USL, an agent can also refine its own strategy. The gain in expressive power rises the notion of ``sustainable capacities'' for agents. USL is built from SL. It mainly brings to SL the two following modifications: semantically, the successor of a given state is not uniquely determined by the data of one choice from each agent. Syntactically, we introduce in the language an operator, called an ``unbinder'', which explicitely deletes the binding of a strategy to an agent. We show that USL is strictly more expressive than SL. We also give the results of model-checking for USL and its memoryless version. They are the same as those of formalisms with implicit unbinders, such as SL and ATLsc.(Slides)