Université de Liège Réseau des Bibliothèques

BICTEL/e - ULg
Serveur institutionnel des thèses de doctorat



Nouvelles thèses
dans BICTEL/e - ULg
  • Decock, Alice - Etude des produits de dissociation de H2O dans un échantillon de comètes d'origines variées
  • Brotcorne, Fany - Behavioral ecology of commensal long-tailed macaque (Macaca fascicularis) populations in Bali, Indonesia: impact of anthropic factors
  • Mishra, Bamdev - A Riemannian approach to large-scale constrained least-squares with symmetries
Présentation Recherche thèse Dépôt thèse Accès
gestionnaires
 
Page de résumé pour ULgetd-11242007-175646

Auteur : Legay, Axel
E-mail de l'auteur : alegay@ulg.ac.be
URN : ULgetd-11242007-175646
Langue : Anglais/English
Titre : Generic Techniques for the verification of infinite-state systems
Intitulé du diplôme : Doctorat en sciences (orientation informatique)
Département : FSA - Département d'électricité, électronique et informatique
Jury :
Nom : Titre :
ABDULLA, Parosh Membre du jury/Committee Member
BOIGELOT, Bernard Membre du jury/Committee Member
LAKHNECH, Yassine Membre du jury/Committee Member
RIGO, Michel Membre du jury/Committee Member
GRIBOMONT, Pascal Président du jury/Committee Chair
WOLPER, Pierre Promoteur/Director
Mots-clés :
  • model checking
  • iteration
  • infinite-state systems
  • automata
  • transducers
  • verification
Date de soutenance : 2007-12-10
Type d'accès : Restreint/Intranet
Résumé :

Within the context of the verification of infinite-state systems,

'Regular model checking' is the name of a family of techniques in

which states are represented by words or trees, sets of states by

finite automata on these objects, and transitions by finite automata

operating on pairs of state encodings, i.e. finite-state

transducers. In this context, the problem of computing the set of

reachable states of a system can be reduced to the one of computing

the iterative closure of the finite-state transducer representing its

transition relation. This thesis provides several techniques to

computing the transitive closure of a finite-state transducer. One of

the motivations of the thesis is to show the feasibility and

usefulness of this approach through a combination of the necessary

theoretical developments, implementation, and experimentation. For

systems whose states are encoded by words, the iteration technique

proceeds by comparing a finite sequence of successive powers of the

transducer, detecting an 'increment' that is added to move from one

power to the next, and extrapolating the sequence by allowing

arbitrary repetitions of this increment. For systems whose states are

represented by trees, the iteration technique proceeds by computing

the powers of the transducer and progressively collapsing their states

according to an equivalence relation until a fixed point is reached.

The proposed iteration techniques can just as well be exploited to

compute the closure of a given set of states by repeated applications

of the transducer, which has proven to be a very effective way of

using the technique. Various examples have been handled completely

within the automata-theoretic setting.

Another applications of the techniques are the verification of linear

temporal properties as well as the computation of the convex hull of a

finite set of integer vectors.

Autre version : http://www.montefiore.ulg.ac.be/~legay/papers/thesis.ps
Fichiers :
Nom du fichier Taille Temps de chargement évalué (HH:MI:SS)
Modem 56K ADSL
[Restreint/Intranet] thesis.ps 3.51 Mb 00:08:21 00:00:18
Fichiers accessibles par l'Internet [Public/Internet] ou que par l'Intranet [Restreint/Intranet].

Bien que le maximum ait été fait pour que les droits des ayants-droits soient respectés, si un de ceux-ci constatait qu'une oeuvre sur laquelle il a des droits a été utilisée dans BICTEL/e ULg sans son autorisation explicite, il est invité à prendre contact le plus rapidement possible avec la Direction du Réseau des Bibliothèques.


Parcourir BICTEL/e par Auteur|Département | Rechercher dans BICTEL/e


© Réseau des Bibliothèques de l'ULg, Grande traverse, 12 B37 4000 LIEGE