We present an extension to linear-time temporal logic (LTL) that combines the
temporal specification 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
definition of the temporal operators, we introduce algebraic alternating
automata as an automata-based intermediate representation. Algebraic
alternating automata are an extension of alternating automata 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 efficient query evaluation algorithm. The
approach is illustrated with examples and experimental results.
pdf
postscript
|