Charla CIWS "Techniques to solve computationally hard problems in automata theory "

Richard Mayr, University of Edinburgh
18 Agosto, 2014 - 14:30
Auditorio DCC, tercer piso
Centro de Investigación de la Web Semántica (CIWS)




We consider nondeterministic finite automata (NFA) and nondeterministic Buchi automata (NBA), which describe regular languages and omega-regular languages, respectively. Central problems for these are computationally hard (PSPACE-complete), e.g., checking language inclusion, equivalence and universality, as well as finding automata of minimal size for a given language.


In spite of the high worst-case complexity, recent algorithms and software-tools can solve many instances of nontrivial size.  Here we give an overview over these techniques. They include antichain techniques exploiting logical subsumption, the construction of congruence bases, and automata minimization methods based on transition pruning and state-space quotienting w.r.t. generalized simulation preorders. In particular, multipebble simulations and the more practical lookahead simulations can in polynomial time compute very good under-approximations of the PSPACE-complete relations of (trace-)language inclusion. A collection of current papers and tools is available at


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.



Comunicaciones DCC