This is the repository for the Approximate Probabilistic Model Checker.
APMC: Approximate Probabilistic Model Checker is a distributed model checker for fully probabilistic systems that uses a client/server computation model to distribute path generation and formula verification on a cluster of workstations. The APMC approach uses an efficient Monte-Carlo method to approximate satisfaction probabilities of monotone properties over fully probabilistic transitions systems. Properties to be checked are expressed in LTL: Linear Temporal Logic.
Many people contributed to the development of APMC :
Richard Lassaigne, Thomas Hérault, Frédéric Magniette, Hélène Baraud, Guillaume Guirado, Michael Cadilhac, Alexandre Borghi and many others.
The team leader was and still is Sylvain Peyronnet (now at ix-labs).