Properties Files

Properties files are specified in Continuous Stochastic Logic, a format allowing for both state formulas and path formulas. PRISM provides documentation which is both easy to understand, and extensive. It is recommended to reference that page here.

The types of properties STAMINA supports

Because the STAMINA algorithm estimates state reachability using cumulative path probability, it lends itself well to most types of CSL properties. In most of the testing examples we use, the properties tested were bounded path probability formulas, i.e., "what is the probability that state formula Φ holds for all states for a path from time 0 s to t s?" If we reference our example model file from the previous page, an example of a property like this would be as follows:

P=? [true U[0,1000] (SpeciesA > 10 & SpeciesB < 30) ]

This property asks "what is probability that from time 0 to 1000 s that the system is in a state which satisfies SpeciesA > 10 and SpeciesB < 30?"