Probabilistic Verifier (ProVer)

ProVer is outdated. Take a look at Ymer instead.

ProVer implements the model independent verification algorithm proposed by Younes & Simmons (2002) for verifying probabilistic real-time properties of discrete event systems through the use of acceptance sampling. Properties are expressed using the continuous stochastic logic (CSL), and discrete event systems are specified using a stochastic process definition language (SPDL) inspired by PDDL. SPDL is expressive enough to allow the specification of time-homogeneous generalized semi-Markov processes (GSMPs).

ProVer is written in C++, and has been reported to compile on the following systems:

Released versions of ProVer can be downloaded here.