Vérification des systèmes probabilistes
|
|
Le Project
Dans ce projet : vérification des systèmes probabilistes (Verification
of Probabilistic Systems : VPS) nous nous
intéressons à utiliser les méthodes formelles pour vérifier les systèmes
probabilistes.
Membres
Outils
CISMO
:
|
|
CISMO est un vérificateur de modèle dédié aux processus
markoviens étiquetés (Labelled Markov Processes : LMP) c'est à dire qui fonctionne sur des
systèmes dont l'espace d'états est continu.
|
|
|
LMPGenerator est un générateur aléatoire
de systèmes probabilistes infinis.
|
RL-Div :
|
|
RL-Div est un outil qui estime la
divergence relative entre deux systèmes probabilistes (LMPs)
et qui est basé sur l'apprentissage par renforcement (Reinforcement
Learning).
|
Publications
J. Desharnais, F. Laviolette,
D. Precup et S. Zhioua. Learning the Difference
between Partial ly
Observable Dynamical Systems.
European
Conference on Machine Learning and Principles and Practice of Knowledge
Discovery in Databases
(ECML PKDD), Slovenia, (2), 2009, 664-677.
J. Desharnais, F. Laviolette, K. Darsini Moturu, and S. Zhioua. Trace
Equivalence Characterization through
Reinforcement Learning (Draft).
19th Canadian Conference on Artificial
Intelligence. June 7-9, 2006, Quebec,
Canada.
J. Desharnais, F. Laviolette,
and S. Zhioua. Testing Probabilistic Equivalence through Reinforcement Learning
(Draft). Submitted
to the 26th Conference on Foundations
of Software Technology and Theoretical
Computer Science. December 13-15, 2006, India.
Mémoires et thèse
Sami Zhioua, Stochastic systems
divergence through Reinforcement
Learning. Ph.D. Thesis, 2008.
Krishna Priya Darsini Moturu. Application of Reinforcement
Learning Algorithms to Software Verification.
Mémoire de maîtrise, 2006.
Simon Paquette. Évaluation symbolique de systèmes
probabilistes à espaces d'états continus. Mémoire de maîtrise, 2005.
Thouria Nafa. La
vérification formelle de systèmes réactifs probabilistes finis. Mémoire
de maîtrise, 2005.
Nicolas Richard. La vérification formelle de systèmes
probabilistes continus. Mémoire de maîtrise, 2003.
|