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
References in zbMATH (referenced in 4 articles )
Showing results 1 to 4 of 4.
- Konur, Savas; Gheorghe, Marian; Dragomir, Ciprian; Ipate, Florentin; Krasnogor, Natalio: Conventional verification for unconventional computing: a genetic XOR gate example (2014)
- Rohr, Christian: Simulative model checking of steady state and time-unbounded temporal operators (2013)
- Heiner, Monika; Herajy, Mostafa; Liu, Fei; Rohr, Christian; Schwarick, Martin: Snoopy -- a unifying Petri net tool (2012)
- Ballarini, Paolo; Guerriero, Maria Luisa: Query-based verification of qualitative trends and oscillations in biochemical systems (2010)