BEGIN:VCALENDAR
VERSION:2.0
CALSCALE:GREGORIAN
METHOD:PUBLISH
X-WR-CALNAME:
X-WR-TIMEZONE:Europe/Paris
BEGIN:VTIMEZONE
TZID:Europe/Paris
X-LIC-LOCATION:Europe/Paris
BEGIN:DAYLIGHT
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
TZNAME:CEST
DTSTART:19700329T020000
RRULE:FREQ=YEARLY;BYMONTH=3;BYDAY=-1SU
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
TZNAME:CET
DTSTART:19701025T030000
RRULE:FREQ=YEARLY;BYMONTH=10;BYDAY=-1SU
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
SUMMARY:
Verification of stochastic timed automata
STATUS:CONFIRMED
ATTENDEE;CN="Pierre Carlier
":
MAILTO:no@spam.com
DESCRIPTION:
In this talk\, I will present the contributions of my thesis
. We are interested in the stochastic timed automaton model
(STA)\, which is a probabilistic extension of the timed auto
maton model. The contributions of this thesis are twofold. I
will mainly focus on the first one: the qualitative and qua
ntitative model-checking problems. STA are\, in particular\,
general probabilistic systems and with such model\, one is
thus interested in questions like Â« Is a property satisfied
\, within a given model\, with probability 1 ? Â» (qualitati
ve) or Â« Can we compute an approximation of the probability
that the model satisfies a given property ? Â» (quantitativ
e). We first study those questions for general stochastic sy
stems. The notion of decisiveness\, that was already studied
in denumerable Markov chains by Abdulla et al.\, plays a ke
y role in order to get results. I will present some of our r
esults\, some being extensions of previous work on Markov ch
ains\, other being new. I will then briefly explain how we c
ould apply those results to subclasses of STA. Finally\, I w
ill have a brief word on our second contribution\, which is
the definition of an operator of composition for STA.
DTSTART;TZID=Europe/Paris:20171114T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201711141
100
UID:LSVsemLSV.201711141100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
END:VCALENDAR