Charla Sean Sedwards (INRIA Rennes)

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

Sean Sedwards, INRIA Rennes, ESTASYS team
Título: Lightweight Verification of Markov Decision Processes.
Abstract: Markov decision processes are a useful formalism to express and optimise concurrency. They may be verified numerically in polynomial time with respect to the size of their state space, however this increases exponentially with the number of state variables. Existing approximative verification techniques are typically memory intensive and do not address the standard verification problems.
I will present recent results that provide the elements of memory-efficient ("lightweight") Monte Carlo verification of Markov decision processes. The idea is based on an O(1) memory representation of history-dependent schedulers, using a hash function and a pseudo-random number generator. This allows schedulers to be chosen at random and constructed on-the-fly, facilitating scalable verification and the efficient use of massively parallel computational architectures.

See you there!