| Summary: | <p>&apos;Almost-certain eventualities&apos; are liveness properties that hold with probability 1. &apos;Abstract probabilities&apos; are probabilities in transition systems about which we know only that they are neither 0 nor 1.</p> <p>Vardi [17] showed that almost-certain properties in linear temporal logic depend only on abstract probabilities, rather than on the probabilities&apos; precise values; we discuss the extent to which a similar result holds in quantitative temporal logic [9,10], and we show how to specialise the logic to those cases. The aim is to provide a simpler calculus than the full logic, one that is in a certain sense complete for proving almost-certain eventualities from abstract-probabilistic assumptions.</p> <p>We consider briefly the complexity of the specialised logic.</p>
|
|---|