Verification of Probabilistic
Systems
|
|
The Project
The Verification of Probabilistic
Systems (VPS) project aims
at using formal methods to verify probabilistic systems.
People
Tools
|
CISMO
:
|
|
CISMO
is a continuous state space model checker based on labeled Markov chain processes (LMP).
|
|
|
|
LMPGenerator is a random
generator for infinite probabilistic systems.
|
|
RL-Div :
|
|
RL-Div is a Reinforcement
Learning based software tool
that computes the
relative divergence between probabilistic
systems (LMP).
|
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. Sc. and Ph. D. Thesis
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. Sc. Thesis, 2006.
Simon Paquette. Symbolic Evaluation of
Probabilistic Systems with
Continous State Spaces.
M. Sc. Thesis, 2005.
Thouria Nafa. Formal Verification of Finite Reactive Probabilistic Systems.
M. Sc. Thesis, 2005.
Nicolas Richard. Formal Verification of Continous Probabilistic Systems. M. Sc. Thesis, 2003.
|
