logo EDITE Ala Eddine BEN SALEM
Identité
Ala Eddine BEN SALEM
État académique
Thèse soutenue le 2014-09-25
Sujet: Model checking adapté aux spécifications et propriétés à vérifier
Direction de thèse:
Encadrement de thèse:
Laboratoire:
Voisinage
Ellipse bleue: doctorant, ellipse jaune: docteur, rectangle vert: permanent, rectangle jaune: HDR. Trait vert: encadrant de thèse, trait bleu: directeur de thèse, pointillé: jury d'évaluation à mi-parcours ou jury de thèse.
Productions scientifiques
edite:1332792370221
Generalized Büchi Automata versus Testing Automata for Model Checking
2nd workshop on Scalable and Usable Model Checking for Petri Nets and other models of Concurrency (SUMo 2011), Newcastle, UK 2011
oai:hal.archives-ouvertes.fr:hal-00855991
Model Checking using Generalized Testing Automata
Geldenhuys and Hansen showed that a kind of ω-automata known as Testing Automata (TA) can, in the case of stuttering-insensitive properties, outperform the Büchi automata traditionally used in the automata-theoretic approach to model checking. In previous work, we compared TA against Transition-based Generalized Büchi Automata (TGBA), and concluded that TA were more interesting when counterexamples were expected, otherwise TGBA were more efficient. In this work we introduce a new kind of automata, dubbed Transition-based Generalized Testing Automata (TGTA), that combine ideas from TA and TGBA. Implementation and experimentation of TGTA show that they outperform other approaches in most of the cases.
Transactions on Petri Nets and Other Models of Concurrencyarticle in peer-reviewed journal 2012
Soutenance
Thèse: Improving the Model Checkin of stutter-Invariant LTL Properties
Soutenance: 2014-09-25
Rapporteurs: Radu MATEESCU    Stefan SCHWOON