Charla Arnd Hartmanns (Universität des Saarlandes)

Este miércoles 19 de noviembre, a las 14:00 en la Sala Smith, Arnd Hartmanns dictará una charla en el marco del grupo. A continuación los datos de la charla:

Arnd Hartmanns, Universität des Saarlandes, Dependable Systems and Software Group
Título: Reachability and Reward Checking for Stochastic Timed Automata.
Abstract:Stochastic timed automata are an expressive formal model for hard and soft real-time systems. They support choices and delays that can be deterministic, nondeterministic or stochastic. Stochastic choices and delays can be based on arbitrary discrete and continuous distributions. In this talk, I present an analysis approach for stochastic timed automata based on abstraction and probabilistic model checking. It delivers upper/lower bounds on maximum/minimum reachability probabilities and expected cumulative reward values. Building on theory originally developed for stochastic hybrid systems, it is the first fully automated model checking technique for stochastic timed automata. Based on an implementation as part of the Modest Toolset and using four varied examples, I will give an idea of its applicability, its efficiency, and current limitations.