Job objectives
From LRDE
This is a property of type Text.
J
https://www.lrde.epita.fr/~gtochon/stage/fiche_poste_stage_apprentissage_resnet_teledetection.pdf +
L'objectif de ce projet est de s'intéresser, non pas à la logique LTL,
mais à des logiques un peu plus expressives : LDL (linear dynamic
logique) et la partie linéaire de PSL (property specification
language). Dans les deux cas, la logique est augmentée avec des
expressions ω-régulières. Par ailleurs, on souhaite produire des
ω-automates qui ne soient pas nécessairement des automates de Büchi ;
par exemple certaines applications préfèrent travailler avec des
automates à parité déterministes.
On souhaite développer les algorithmes pour effectuer ces traductions,
et les implémenter dans la bibliothèque Spot. Aujourd'hui, Spot est
une bibliothèque C++ mature pour la manipulation d'ω-automates et de
formules de logique, on y trouve des algorithmes de traductions de LTL
en ω-automates réputés, ainsi qu'un support partiel de la logique PSL. +
L'objectif de ce projet est d'étudier dans quelle mesure les
algorithmes de manipulation d'ω-automates peuvent être accélérés à
l'aide de GPU. +
Dans Spot, on souhaite être capable d'effectuer des transformations de
conditions d'acceptation, on souhaite généraliser les algorithmes qui
ont été inventés pour des conditions d'acceptations particulières de
façon à traiter des conditions d'acceptation plus larges. C'est le but
de ce projet de recherche. Parmi les algorithmes dont la
généralisation nous intéresse le plus, citons : les transformations
entre divers types de conditions d'acceptation, les simplifications
d'ω-automates avec condition d'acceptation quelconque, la
déterminisation d'ω-automates avec condition d'acceptation la plus
générique possible, le test du vide d'ω-automates construits à la
volée, etc. +
L'objectif de ce stage est de concevoir, en s'inspirant de l'interface
existante, une nouvelle interface plus moderne et foncionnelle basée sur
Qt. L'utilisation de Qt permettra notamment d'obtenir un « look & feel » natif
sur toutes les plateformes (OS X, Linux etc.). D'autre part, les solutions
d'interfaçage entre Lisp et Qt sont aujourd'hui de meilleure qualité que
celles pour Gtk.
Déroulement du stage :
* apprentissage des bases de Qt [*]
* découverte du langage Lisp et de la bibliothèque Climb
* choix du système d'interfaçage Lisp / Qt
* réalisation de la nouvelle interface à fonctionnalités équivalentes à l'ancienne,
* en fonction du temps et au libre choix du stagiaire: toute amélioration de l'interface elle-même, de son intégration avec le reste de la bibliothèque, etc. +