Agenda
06/ago
Abstract: Consider Markov Decision Processes (MDPs) and 2-player turn-based stochastic games on countably infinite game graphs, with objectives expressible by parity conditions (including special cases like reachability, safety, Buchi and co-Buchi objectives). We give an overview of results about the determinacy (for games) and about the memory requirements of epsilon-optimal and optimal strategies, respectively (for MDPs and games). Moreover, we highlight the differences between infinite game graphs and finite game graphs, and the reasons why (epsilon-)optimal strategies need memory for certain objectives.
is a very popular proof assistant, used in a variety of academic and industrial projects, for formalizing both computer science results as well as mathematical ones.
About the speaker: Richard Mayr received a Msc in computer science from TU-Munich, Germany, (1994) and a PhD in computer science from TU-Munich (1998). He received scholarships from the DAAD and the DFG in support of his research at the University of Edinburgh, UK, (1999) and the University of Paris 7, France, (2000), and completed his Habilitation for Informatics at the University of Freiburg, Germany, in 2002. He was assistant professor at the University of Freiburg (2001-2004) and at North Carolina State University, USA, (2004-2007). In 2008 he was appointed to the post of Lecturer at the School of Informatics (LFCS) at the University of Edinburgh, UK. His research interests include automated verification, automata and temporal logic, model-checking and semantic equivalence checking, formal verification of real-time and probabilistic systems, infinite-state Markov chains and stochastic games.
Venue: Sala Javier Pinto, Edificio San Agustin, 4to piso, PUC, Campus San Joaquín
