Charla de Friedrich Gretz (RWTH), 12-Sep-2013, 17:00

Este Jueves 12 de Septiembre, a las 17:00 en la Sala Smith, Friedrich Gretz va a dar una charla en el marco del curso "Semántica de procesos" abierta a todos. A continuación los datos de la charla:

Friedrich Gretz, Moves group, RWTH
Título: Probabilistic Guarded Command Language - a tutorial.
Resumen:In this tutorial we introduce the probabilistic Guarded Command Language (pGCL). The use of a probabilistic language will be motivated by a a set of examples. We will then introduce the notions of expectations and expectation transformers that are used to reason over pGCL programs. As it turns out these notions can intuitively be understood using a Markov Decision Process as the underlying operational semantics. In the second half we return to reasoning with expectations and introduce probabilistic invariants. We will then show how invariants can help us to prove properties of pGLC programs. Finally, we briefly introduce a tool called Prinsys that helps us to discover invariants.