Collecting statistics over runtime executions

Abstract. We present an extension to linear-time temporal logic (LTL) that com-bines the temporal specication with the collection of statistical data. By collecting statistics over runtime executions of a program we can answer complex queries, such as \what is the average number of packet transmissions " in a communication protocol, or \how often does a particular process enter the critical section while another process remains waiting " in a mutual exclusion algorithm. To decouple the evaluation strategy of the queries from the denition of the temporal operators, we introduce algebraic alternating automata as an automata-based intermediate representation. Algebraic alternating automata are an extension of alternating au-tomata that produce a value instead of acceptance or rejection for each trace. Based on the translation of the formulas from the query language to algebraic alternating automata, we obtain a simple and ecient query evaluation algorithm. The approach is illustrated with examples and experimental results. 1