Almost-certain eventualities and abstract probabilities in quantitative temporal logic

Annabelle McIver, Carroll Morgan

Research output: Contribution to journalArticlepeer-review

1 Citation (Scopus)


'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 [17] 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.

Original languageEnglish
Pages (from-to)15-43
Number of pages29
JournalElectronic Notes in Theoretical Computer Science
Publication statusPublished - Jan 2001


Dive into the research topics of 'Almost-certain eventualities and abstract probabilities in quantitative temporal logic'. Together they form a unique fingerprint.

Cite this