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