BEGIN:VCALENDAR
PRODID:-//eluceo/ical//2.0/EN
VERSION:2.0
CALSCALE:GREGORIAN
BEGIN:VEVENT
UID:www.tcs.tifr.res.in/event/232
DTSTAMP:20230914T125915Z
SUMMARY:Observing Markov Chains by Timed Automata
DESCRIPTION:Speaker: Joost-Pieter Katoen\nRWTH Aachen University\nLS2: Soft
ware Modeling and Verification\nD-52056 Aachen\nGermany\n\nAbstract: \nMar
kov chains are omnipresent. They are used as semantical backbone of Markov
ian queueing networks\, stochastic Petri nets\, stochastic process algebra
s\, and calculi for systems biology. Abundant applications in performance\
, reliability and dependability analysis use Markov chains. The specificat
ion of measures-of-interest is however quite limited\, and dedicated algor
ithms are typically developed for every new measure.\n\nIn this talk\, we
will survey model checking techniques for Markov chains. On the one hand\,
temporal logics allow to express most measures of interest as well as mea
sures that go beyond the classical one. On the other hand\, a single model
-checking algorithm suffices to deal with all measures that can be express
ed.\n\nWe will describe the basic model-checking algorithms\, covering bot
h discrete-time and continuous-time Markov chains\, and report on recent p
rogress on using timed automata as requirements (rather than temporal logi
c).\n
URL:https://www.tcs.tifr.res.in/web/events/232
DTSTART;TZID=Asia/Kolkata:20111216T113000
DTEND;TZID=Asia/Kolkata:20111216T123000
LOCATION:A-212 (STCS Seminar Room)
END:VEVENT
END:VCALENDAR