Modélisation formelle d'exigences et logiques temporelles multi-agents
Thèse soutenue le 20 juin 2014 à l'Institut Supérieur de l'Aéronautique et de l'Espace ( ISAE Toulouse, France).
exigences
agents
rôles
multi-stratégies
rafffinement de stratégies
Ces travaux concernent la modélisation formelle d'exigences et les interactions entre agents. Nous y développons un langage de modélisation pour les exigences d'un système à élaborer, Khi. Nous y proposons également une logique temporelle multi-agents, USL.
    A notre connaissance, il n'y a pas de formalisation dans ce domaine qui traite à la fois le temps et les actions des agents. C'est ce que nous proposons avec Khi. Il emprunte à la méthode Kaos ses moyens pour décrire formellement des exigences comportementales et en dériver des spécifications d'opérations pour un système. Il emprunte également à Tropos-i* un appareil conceptuel qui nous permet d'exprimer la question de la capacité effective des agents à assurer la satisfaction des spécifications qui leurs sont assignées. Nous appelons cette question le « problème de l'assignation ». Le langage Khi propose ainsi une synthèse originale qui permet de formaliser dans un langage unique à la fois les exigences comportementales d'un système à élaborer et les capacités d'actions des agents dans ce système. Par ailleurs, Khi offre un cadre conceptuel qui permet d'exprimer le problème de l'assignation. Il y est décrit comme le problème de la satisfaction d'un certain nombre de critères de correction par un modèle.
    Pour donner un formalisme aux concepts de Khi et un moyen de résolution du problème de l'assignation, nous introduisons également une logique temporelle multi-agents, USL. Elle s'inspire des travaux dans le domaine, en particulier ATLsc et SL. Comme ces derniers formalismes, elle utilise des contextes de stratégies pour exprimer des capacités d'agents à assurer la satisfaction de propriétés temporelles. Elle se distingue des autres formalismes existants principalement par deux aspects : d'abord elle utilise des stratégies non-déterministes. Nous les appelons des multi-stratégies. Nous pouvons ainsi exprimer des propriétés de raffinement entre les multi-stratégies. Par ailleurs, nous utilisons pour USL des exécutions du système qui ne sont pas nécessairement infinies. Nous pouvons alors formaliser les notions d'engagement contradictoire pour un agent et de capacités d'actions conflictuelles pour un ensemble d'agents. Nous montrons que l'expressivité d'USL englobe celle des formalismes pré-existants. Cette logique permet notamment de formaliser la propriété, nouvelle dans le domaine, de contrôle pérenne. Elle permet également d'introduire des prédicats de comparaisons et d'égalité entre les multi-stratégies et/ou les stratégies. Une étude des relations de dépendance entre les multi-stratégies et/ou les stratégies est par ailleurs amorcée avec USL. Nous montrons par ailleurs que la complexité des problèmes de model-checking et de satisfiabilité pour USL est équivalente à celle des formalismes pré-existants.
    Nous réduisons ensuite la satisfaction des critères de correction qui expriment le problème de l'assignation dans Khi à des instances du problème de model-checking pour une version adéquate de USL, USLKhi. Nous donnons un algorithme de résolution pour ce problème, il utilise un espace polynomial. Le développemeent de Khi et l'usage adéquat d'USL permettent donc d'exprimer, de formaliser et de résoudre le problème de l'assignation. L'ensemble des concepts et des outils présentés est par ailleurs illustré par un cas d'étude décrivant des missions d'observation spatiale.