Collecting Statistics over Runtime Executions

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 appro...

• Type: Journal
• Year: 2002
• Where: ENTCS
• Authors: Bernd Finkbeiner, Sriram Sankaranarayanan, Henny Sipma
• Keywords: Algebraic Alternating Automata, ENTCS 2002, Linear-time Temporal Logic, Mutual Exclusion Algorithm