Hello tout le monde.

Tout d'abord, qu'est-ce qu'un TAS (Tool-Assisted Speedrun) ?
1) C'est un speedrun. (Si si !) C'est à dire un jeu vidéo complété le plus rapidement possible. Parfois en s'imposant des contraintes artificielles comme ne pas exploiter de bug.
2) Il est assisté par des outils, notamment des émulateurs permettant de faire avancer le jeu frame par frame, de revenir en arrière sans faire appel à un quelconque mécanisme de sauvegarde du jeu.

Le but étant de produire uniquement une séquence d'appui de touches pouvant être rejoué sur le même émulateur.

Un site y est notamment dédié : http://tasvideos.org/

Voici donc un exemple que je trouve assez amusant et que j'aimerais pouvoir reproduire de manière automatique :

Il "termine" le jeu pokémon yellow (déclenche les crédits de fin) sur gameboy color en à peine plus d'une minute, dont environ une minute de dialogues.


Et donc, je pense que pour automatiser complètement cette tâche de création de TAS, le model checking me semble être une approche intéressante puisque, du point de vue informatique, l'objectif est d'amener le programme (le jeu) dans un état donné (celui qui dit "WIN" ou autre).

Si je devais coder moi-même un model checker pour cette tâche, je prendrais soin d'inclure des heuristiques de plus court chemin, et je ne m'arrêterais pas au premier état valide trouvé afin d'en chercher des plus courts. Bref, je ferais un bon vieux branch and bound avec des heuristiques et des connaissances domain-specific un peu partout.

Seulement y'a des tas de model checker dans la nature, dont certains sont sûrement infiniment plus efficace d'une manière générale que ce que je peux coder en un temps raisonnable. L'idée serait donc de lier les deux.


J'ai donc deux questions.
1) Que pensez-vous de l'approche model-checking pour cet usage ? (Sachant que j'aimerais le faire tourner sur des jeux beaucoup plus longs.) Peut-être vaudrait-il mieux partir sur une formalisation comme un problème d'optimisation et là dessus rajouter l'exploration des états du programme ?
2) Connaissez-vous des model-checker qui me permettent d'introduire des heuristiques de parcours des états (pour aller vers un chemin court en premier) et qui me permette d'entrer mes connaissances spécifiques au domaine pour encore accélérer le truc ?


Comme connaissance domain-specific, je pense notamment au fait que beaucoup d'états ne vont avoir de différent que le générateur de nombres aléatoires et que par conséquent, on peut les considérer identiques tant qu'une transition ne lit pas ces octets.


Merci d'avance.