BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//University of Liverpool Computer Science Seminar System//v2//EN
BEGIN:VEVENT
DTSTAMP:20260921T102715Z
UID:Seminar-dept-407@lxserverM.csc.liv.ac.uk
ORGANIZER:CN=Lutz Oettershagen:MAILTO:Lutz.Oettershagen@liverpool.ac.uk
DTSTART:20160426T130000
DTEND:20160426T140000
SUMMARY:School Seminar Series
DESCRIPTION:Dr. Ernst Moritz Hahn: Lazy Probabilistic Model Checking without Determinisation\n\nThe bottleneck in the quantitative analysis of Markov chains and Markov decision processes against specifications given in LTL or as some form of nondeterministic Büchi automata is the inclusion of a determinisation step of the automaton under consideration. In this talk, we show that full determinisation can be avoided: subset and breakpoint constructions suffice. We have implemented our approach — both explicit and symbolic versions — in a prototype tool. Our experiments show that our prototype can compete with mature tools like PRISM.\n\nhttps://www.csc.liv.ac.uk/research/seminars/abstract.php?id=407
LOCATION:Ashton Lecture Theater
END:VEVENT
END:VCALENDAR