The LSV seminar takes place on Tuesday at 11:00 AM. The usual location is the conference room at Pavillon des Jardins (venue). If you wish to be informed by e-mail about upcoming seminars, please contact Stéphane Le Roux and Matthias Fuegger.
The seminar is open to public and does not require any form of registration.
Regular graphs (generated by deterministic graph grammars) form a simple and natural generalisation of pushdown automata. In this talk we use such graphs to define infinite state Markov chains. We establish some model checking results for a probabilistic temporal logic (pCTL). These results were already known for probabilistic pushdown automata, but we advocate that regular graphs enable a simpler exposition.
This is joint work with Nathalie Bertrand (INRIA Rennes).