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.
In Runtime Verification, CAV'02 workshop.