TY - JOUR
T1 - Almost-certain eventualities and abstract probabilities in the quantitative temporal logic qTL
AU - McIver, Annabelle
AU - Morgan, Carroll
PY - 2003/2/9
Y1 - 2003/2/9
N2 - '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 http://web.comlab.ox.ac.uk/oucl/research/areas/probs/bibliography.html; logic J, IGPL 7(6) (1999) 779, http://www3.oup.co.uk/igp1/Volume_07/Issue_06, http://web.comlab.ox.ac.uk/oucl/research/areas/probs/bibliography.html), 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.
AB - '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 http://web.comlab.ox.ac.uk/oucl/research/areas/probs/bibliography.html; logic J, IGPL 7(6) (1999) 779, http://www3.oup.co.uk/igp1/Volume_07/Issue_06, http://web.comlab.ox.ac.uk/oucl/research/areas/probs/bibliography.html), 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.
UR - http://www.scopus.com/inward/record.url?scp=0037427177&partnerID=8YFLogxK
U2 - 10.1016/S0304-3975(02)00612-6
DO - 10.1016/S0304-3975(02)00612-6
M3 - Article
AN - SCOPUS:0037427177
SN - 0304-3975
VL - 293
SP - 507
EP - 534
JO - Theoretical Computer Science
JF - Theoretical Computer Science
IS - 3
ER -