BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//University of Liverpool Computer Science Seminar System//v2//EN
BEGIN:VEVENT
DTSTAMP:20260916T075605Z
UID:Seminar-dept-462@lxserverM.csc.liv.ac.uk
ORGANIZER:CN=Lutz Oettershagen:MAILTO:Lutz.Oettershagen@liverpool.ac.uk
DTSTART:20180501T160000
DTEND:20180501T170000
SUMMARY:School Seminar Series
DESCRIPTION:Prof. Thomas Brihaye: When are stochastic transition systems tameable?\n\nA decade ago, Abdulla et al introduced the elegant concept of decisiveness for denumerable Markov chains. Roughly decisiveness allows one to lift most good properties from finite Markov chains to denumerable ones, and therefore to adapt existing verification algorithms to infinite-state models. Denumerable Markov chains however do not encompass stochastic real-time systems, and general stochastic transition systems (STSs) are needed. In this talk, we discuss a framework to perform both the qualitative and the quantitative analysis of STSs. In order to do so, we first need to adapt the concept of decisiveness for general STSs. Then we define a notion of abstraction and provide some transfer properties. Then we focus on both qualitative and quantitative analysis. Beyond (repeated) reachability properties for which our technics are strongly inspired by the work on denumerable Markov chains, we use abstractions to design algorithms for the model-checking of arbitrary omega-regular properties, for subclasses of STS. Last we instantiate our framework with stochastic timed automata Some of these results were known from the literature, but our generic approach permits to view them in a unified framework. We also derive interesting new approximability results.\n\n\n\nThis talk is based on joint work with Nathalie Bertrand, Patricia Bouyer, and Pierre Carlier\n\nhttps://www.csc.liv.ac.uk/research/seminars/abstract.php?id=462
LOCATION:ELEC-202
END:VEVENT
END:VCALENDAR