[Grunske08]
- probabilisticProperty::= "The system shall have a behavior where" patternStateFormula.
- patternStateFormula::= "with a probability" probabilityBound "it is the case that" occurenceStateFormula| orderStateFormula.
- occurenceStateFormula::= transientStateProbability | steadyStateProbability | probabilisticInvariance | probabilisticExistence.
- orderStateFormula::= probabilisticUntil | probabilisticPrecedence | probabilisticResponse | probabilisticConstResponse.
- transientStateProbability::= stateFormula "holds after exactly" time "time units.".
- steadyStateProbability::= stateFormula "holds in the long run.".
- probabilisticInvariance::= stateFormula "holds continuously" timeBound ".".
- probabilisticExistence::= stateFormula "will eventually hold" timeBound ".".
- probabilisticUntil::= stateFormula2 "holds" timeBound "after" stateFormula1 "has held continuously before".
- probabilisticPrecedence::= stateFormula2 "holds before" stateFormula1 "can hold" timeBound ".".
- probabilisticResponse::= "if" stateFormula1 "holds, then as a response" stateFormula2 "becomes true" timeBound ".".
- probabilisticConstResponse::= "if" stateFormula1 "holds, then as a response" stateFormula3 "becomes true" timeBound "without" stateFormula2"holding in between.".
- timeBound::= noTimeBound | upperTimeBound | lowerTimeBound | timeInterval.
- noTimeBound::= "".
- upperTimeBound::= "within" time "time units".
- lowerTimeBound::= "after" time "time units".
- timeInterval::= "between" time "and" time "time units".
- time::=Positive & Real.
- probabilityBound::= lowerProbBound | lowerOrEqualProbBound | higherProbBound| higherOrEqualProbBound.
- lowerProbBound::= "lower than" probability.
- lowerOrEqualProbBound::= "lower or equal than" probability.
- higherProbBound::= "greater than" probability.
- higherOrEqualProbBound::= "greater or equal than" probability.
- probability::=[0..1].
- SimpleStateProperty::=given.
- stateFormula::= SimpleStateProperty.
- stateFormula1::= SimpleStateProperty.
- stateFormula2::= SimpleStateProperty.
- stateFormula3::= SimpleStateProperty.