MC2(PLTLc) is a Monte Carlo Model Checker for properties written in Probabilistic Linear-time Temporal Logic with numerical constraints (PLTLc). The model checker takes as input a set of traces in the form of a simulation output file. It also takes as input a query file containing a list of PLTLc properties, and returns for each property the probability that the set of traces satisfies the property. MC2(PLTLc) can also calculate the probabilistic domains of free variables within a property; thus it is easy to calculate the distribution of features, such as times at which peaks occur. MC2(PLTLc) can operate with stochastic/deterministic simulation output, deterministic parameter scan output or even wet-lab data. MC2(PLTLc) was developed at the Bioinformatics Research Centre in the University of Glasgow.

Keywords for this software

Anything in here will be replaced on browsers that support the canvas element