|
Evènement pour le groupe Modélisation et Verification
Date | 2010-01-14 11:30-12:45 |
Titre | L'approche SAT pour lpour automates temporisés avec étapes parallèles |
Résumé | Plusieurs travaux ont exploré la possibilité d'améliorer les algorithmes d'exploration d'états symboliques (zones) pour automates temporisés par une sémantique d'ordres partiels. A priori, ces sémantiques sont contre-intuitives, parce que le temps, représenté par des nombres réels, est un ordre total.
D'un autre coté, pour des systèmes non-temporisés, on connaît des réductions SAT qui utilisent une sémantique avec transitions parallèles : la possibilité d'exécuter plusieurs transitions indépendantes en parallèle raccourcit des séquences témoin et permet ainsi d'aller plus loin avec la vérification bornée.
Dans notre travail, nous combinons les deux améliorations, ordres partiels pour automates temporisés et transitions parallèles pour une meilleure réduction SAT. Il se pose alors la question de ce que sont des « transitions parallèles » pour un automate temporisé. Autre que la réponse intuitive « en parallèle est en même temps » nous explorons deux autres sémantiques avec des notions plus relâchées pour les transitions parallèles. Il s'avère que les trois sémantiques ont des performances incomparables, selon les exemples considérés.
À l'occasion, je présente aussi le vérificateur POEM, qui est la plate forme expérimentale avec laquelle nous avons réalisé le prototype et les expériences.
|
Lieu | Salle 076, LaBRI, Rez-de-chaussée |
Orateur | Peter Niebert |
Email | peter.niebert@lif.univ-mrs.fr |
Url | LIF, Marseille |
Aucun document lié à cet événement. RetourRetour à l'index
| |