Quantitative monitor automata - Chatterjee, Krishnendu; Henzinger, Thomas A; Otop, Jan; SAS: Static Analysis Symposium; Rigorous Systems Engineering; The Wittgenstein Prize; Quantitative Graph Games: Theory and Applications; Efficient Algorithms for Computer Aided Verification (Edinburgh, United Kingdom : Springer, 2016)
In this paper we review various automata-theoretic formalisms for expressing quantitative properties. We start with finite-state Boolean automata that express the traditional regular properties. We then consider weighted ω-automata that can measure the average density of events, which finite-state Boolean automata cannot. However, even weighted ω-automata cannot express basic performance properties like average response time. We finally consider two formalisms of weighted ω-automata with monitors, where the monitors are either (a) counters or (b) weighted automata themselves. We present a translation result to establish that these two formalisms are equivalent. Weighted ω-automata with monitors generalize weighted ω-automata, and can express average response time property. They present a natural, robust, and expressive framework for quantitative specifications, with important decidable properties.
published
yes
Keywords: conference paper