By collecting statistics over runtime executions of a program we can
answer complex queries, such as ``what is the average number of packet
retransmissions'' in a communication protocol, or "how often does process
P_1 enter the critical section while process P_2 waits" in a mutual
exclusion algorithm. We present an extension to linear-time temporal logic
that combines the temporal specification with the collection of
statistical data. By translating formulas of this language to alternating
automata we obtain a simple and efficient query evaluation algorithm. We
illustrate our approach with examples and experimental results.
bibtex
pdf
postscript
|