@article{Finkbeiner2005,
title = {Collecting Statistics Over Runtime Executions},
author = {Bernd Finkbeiner and Sriram Sankaranarayanan and Henny B. Sipma},
journal = {Formal Methods in System Design},
publisher = {Springer Netherlands},
issn = {0925-9856 (Print) 1572-8102 (Online)},
url = {http://www.springerlink.com/content/f2354782v9x41407/},
abstract = {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.},
number = {3},
pages = {253--274},
volume = {27},
doi = {10.1007/s10703-005-3399-3},
year = {2005},
keywords = {program profiling - runtime verification - specification languages - runtime monitoring - temporal logic},
month = {November},
subject_collection = {Engineering},
}