'Almost-certain eventualities' are liveness properties that hold with probability 1. 'Abstract probabilities' are probabilities in transition systems about which we know only that they are neither 0 nor 1. Vardi  showed that almost-certain properties in linear temporal logic depend only on abstract probabilities, rather than on the probabilities' 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. We consider briefly the complexity of the specialised logic.
|Number of pages||29|
|Journal||Electronic Notes in Theoretical Computer Science|
|Publication status||Published - Jan 2001|