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

Professeurs :

Josée Desharnais

 

François Laviolette

 

 

Étudiants en Doctorat  :

Sami Zhioua

 

 

Master Students :

Marcelo Alves Ribeiro

 

Krishna P. D. Moturu

 

Simon Paquette

 

Thouria Nafa

 

Nicolas Richard

 

 

Étudiants au Bac :

Frédérick Lemay

 

Amélie Turgeon

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.