Almost-certain eventualities and abstract probabilities in the quantitative temporal logic qTL

Annabelle McIver, Carroll Morgan*

*Corresponding author for this work

Research output: Contribution to journalArticlepeer-review

2 Citations (Scopus)


'Almost-certain eventualities' are liveness properties that hold with probability 1. 'Abstract probabilities' in transition systems are those known only to be bounded away from zero and one. Vardi (Proceedings of the 26th IEEE Symposium on Foundations of Computer Science, Portland, 1985, p. 327) 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 the quantitative temporal logic qTL derived from the quantitative modal μ-calculus qMμ (Proceedings the Formal Methods Pacific '97, Springer, Singapore, 1997, also available; logic J, IGPL 7(6) (1999) 779,,, and we show how to specialise the logic to these 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 conclude by considering the complexity of the specialised logic.

Original languageEnglish
Pages (from-to)507-534
Number of pages28
JournalTheoretical Computer Science
Issue number3
Publication statusPublished - 9 Feb 2003


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

Cite this