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:
The stochastic logic CSL TA and its efficient model-checking
STATUS:CONFIRMED
ATTENDEE;CN="Susanna Donatelli
":
MAILTO:no@spam.com
DESCRIPTION:
In this talk I will review the stochastic logic CSL TA\, a
logic that has been defined to model-check Continuous Time M
arkov Chains. CSL TA extends the well-known stochastic logic
CSL by allowing path properties to be defined through a Tim
ed Automaton (TA). The price of this extension is an increas
e in the cost of the model checking algorithm both in terms
of memory and of solution time: the model checking of CSL re
quires to solve one of more CTMCs\, that of CSL TA the solut
ion of a Markov Regenerative Process. I will then discuss ho
w we can efficiently model check CSL TA properties\, in part
icular I will present a model-checking algorithm that adapts
itself to the formula\, so that the memory and computationa
l cost for the model checking of a CSL TA formula naturally
scales down to that of the standard CSL model checking algor
ithm\, when the property specified by the TA is equivalent t
o a CSL one. The technique is based on the construction of t
he region graph of the timed automata and on a component-bas
ed technique for the computation of the steady-state probabi
lity of Markov regenerative processes. The presentation will
be supported by a demo with the GreatSPN tool developed in
Torino.
DTSTART;TZID=Europe/Paris:20190122T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201901221
100
UID:LSVsemLSV.201901221100@lsv.ens-cachan.fr
LOCATION:Pavillon des Jardins
END:VEVENT
END:VCALENDAR