خلاصه‌ای از این ارائه به شرح زیر است:

Responsiveness -the requirement that every request to a system be eventually handled- is one of the fundamental liveness properties of a reactive system and lies at the heart of all methods for specifying and verifying liveness. Average response time is a quantitative measure for the responsiveness requirement used commonly in performance evaluation. The static computation of average response time has proved remarkably elusive even for finite-state models of reactive systems. We present, for the first time, a robust formalism that allows the specification and computation of quantitative temporal properties including average response time. The formalism is based on nested weighted automata, which can serve as monitors for measuring the response time of a reactive system. We show that the average response time can be computed in exponential space for nondeterministic finite-state models of reactive systems and in polynomial time for probabilistic finite-state models. This work is joint with Krishnendu Chatterjee and Jan Otop.

اگر دانشجوی دانشگاه شریف نیستید، جهت انجام هماهنگی‌های لازم برای حضور در ارائه، لازم است که مشخصات زیر را وارد نمایید.