Evènement pour le groupe Modélisation et Verification


Date 2010-01-14  11:30-12:45
TitreL'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.  
LieuSalle 076, LaBRI, Rez-de-chaussée 
OrateurPeter Niebert 
Emailpeter.niebert@lif.univ-mrs.fr 
UrlLIF, Marseille 



Aucun document lié à cet événement.

Retour
Retour à l'index