Titre: Vérification de scénarios de jeux vidéos Encadrants: F. Herbreteau, A. Rollet et L. Simon Résumé: Ce stage se place dans le cadre d'un projet commun entre différents acteurs du jeu vidéo en Nouvelle Aquitaine, dont notamment Ubisoft, Inria, Cnam et LaBRI. Dans ce cadre, le stage proposé s'articule autour d'une collaboration entre UbiSoft et le LaBRI pour l'amélioration des techniques de générations procédurales de contenus, en cherchant l'apport des méthodes formelles pour permettre de garantir certaines propriétés à l'issu de ce type de génération. La narration est un élément clé du succès d'un jeu vidéo. Un jeu tel "Assassins Creed" repose sur un récit dans lequel de nombreux acteurs (virtuels) interagissent entre eux et avec un joueur réel. Chaque joueur virtuel exécute un programme indépendamment des autres joueurs. Il est cependant souhaitable de voir émerger de bonnes propriétés des interactions entres les différents joueurs. Par exemple, certains joueurs virtuels sont des adversaires du joueur réel quand d'autres ont pour but de l'assister. Il n'est donc pas souhaitable qu'un assistant puisse éliminer le joueur réel, ni même qu'un adversaire élimine un assistant dont le rôle est crucial à la réussite de la quête du joueur réel. On parle globalement de scénarios. D'un point de vue informatique, les joueurs virtuels sont des processus indépendants qui interagissent via des synchronisations. Ils forment donc un système dont on veut vérifier des propriétés. Depuis une trentaine d'années la vérification formelle permet de prouver des propriétés de systèmes concurrents. L'objectif de ce stage est d'appliquer les techniques de vérification formelle aux scénarios issus de jeux vidéos. Pour cela, il faut disposer d'un langage permettant d'exprimer les propriétés attendues du système. Le premier objectif de ce stage est donc la définition d'une logique qui permette de spécifier des propriétés de type "scénarios" et de les vérifier. Plusieurs logiques permettent de spécifier les propriétés des comportements d'un système. Notamment les logiques temporelles LTL [P77] et CTL [CE81], les relations d'Allen [A83] ou encore la logique d'intervalles de Halpern-Shoham [HS92]. Des liens ont été établis entre ces logiques, notamment [RB06]. Par ailleurs, les logiques d'intervalles sont en général indécidables, et des sous-logiques décidables ont pu être identifiées [MMP18]. Le stage débutera donc par une analyse des besoins de spécification, ainsi qu'un état de l'art des logiques existantes et de leur adéquation au besoin. Il se poursuivra par la proposition d'algorithmes de vérification de scénarios, et par la réalisation d'un démonstrateur probant pour les partenaires du projet. [A83] Allen, James F. (26 November 1983). "Maintaining knowledge about temporal intervals". Communications of the ACM. ACM Press: 832-843. doi:10.1145/182.358434. ISSN 0001-0782. [CE81] E.M. Clarke; E.A. Emerson (1981). "Design and synthesis of synchronisation skeletons using branching time temporal logic". Logic of Programs, Proceedings of Workshop, Lecture Notes in Computer Science, vol. 131. Springer, Berlin: 52-71. [HS92] J. Halpern, Y. Shoham, A propositional modal logic of time intervals, Journal of the ACM 38 (4) (1991) 935-962. [MMP18] Alberto Molinari, Angelo Montanari, Adriano Peron: Model checking for fragments of Halpern and Shoham's interval temporal logic based on track representatives. Inf. Comput. 259(3): 412-443 (2018) [P77] Amir Pnueli: The Temporal Logic of Programs FOCS 1977: 46-57 [RB06] Grigore Rosu, Saddek Bensalem: Allen Linear (Interval) Temporal Logic - Translation to LTL and Monitor Synthesis. CAV 2006: 263-277