BEGIN:VCALENDAR
PRODID:-//eluceo/ical//2.0/EN
VERSION:2.0
CALSCALE:GREGORIAN
BEGIN:VEVENT
UID:www.tcs.tifr.res.in/event/621
DTSTAMP:20230914T125931Z
SUMMARY:Statistical Model Checking for Unbounded Temporal Properties
DESCRIPTION:Speaker: Przemyslaw Daca (Institute of Science and Technology\n
 Am Campus 1\nA - 3400 Klosterneuburg\nAustria)\n\nAbstract: \nAbstract: In
  this talk\, I present a new algorithm for the statistical model checking 
 of Markov chains with respect to unbounded temporal properties\, such as r
 eachability and full linear temporal logic. The main idea is that we monit
 or each simulation run on the fly\, in order to detect quickly if a bottom
  strongly connected component is entered with high probability\, in which 
 case the simulation run can be terminated early. As a result\, our simulat
 ion runs are often much shorter than required by termination bounds that a
 re computed a priori for a desired level of confidence and size of the sta
 te space. In comparison to previous algorithms for statistical model check
 ing\, for a given level of confidence\, our method is not only faster in m
 any cases but also requires less information about the system\, namely\, o
 nly the minimum transition probability that occurs in the Markov chain. In
  addition\, our method can be generalised to unbounded quantitative proper
 ties such as mean-payoff bounds.\n
URL:https://www.tcs.tifr.res.in/web/events/621
DTSTART;TZID=Asia/Kolkata:20150901T153000
DTEND;TZID=Asia/Kolkata:20150901T163000
LOCATION:A-212 (STCS Seminar Room)
END:VEVENT
END:VCALENDAR