Contributions to the verification and control of timed and probabilistic models: Mémoire d'habilitation à diriger des recherches

Nathalie Bertrand 1
1 SUMO - SUpervision of large MOdular and distributed systems
Inria Rennes – Bretagne Atlantique , IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL
Abstract : The importance of model checking was acknowledged by a Turing award in 2007, and formal methods in general have proved extremely useful in the validation of hardware and software systems. These techniques are based on mathematical abstractions, and require models both of the system, and of the requirements it has to meet. In order to faithfully represent real-life systems, models should incorporate several features including timing contraints, probabilities, unknown parameters and imperfect information. This habilitation document reports on my contributions to formal methods for complex systems that combine several of these aspects. More specifically, the following problems are tackled: approximate determinization of timed automata, model checking and control for stochastic timed automata, synthesis for partially observable probabilistic systems, and parameterized verification of probabilistic systems.
Mots-clés : verification
Type de document :
HDR
Formal Languages and Automata Theory [cs.FL]. Rennes 1, 2015
Liste complète des métadonnées

Littérature citée [125 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/tel-01243612
Contributeur : Nathalie Bertrand <>
Soumis le : mercredi 16 décembre 2015 - 23:45:51
Dernière modification le : mercredi 16 mai 2018 - 11:24:07
Document(s) archivé(s) le : samedi 29 avril 2017 - 14:12:26

Fichier

Identifiants

  • HAL Id : tel-01243612, version 1

Citation

Nathalie Bertrand. Contributions to the verification and control of timed and probabilistic models: Mémoire d'habilitation à diriger des recherches. Formal Languages and Automata Theory [cs.FL]. Rennes 1, 2015. 〈tel-01243612〉

Partager

Métriques

Consultations de la notice

655

Téléchargements de fichiers

172