The LSV seminar takes place on Tuesday at 11:00 AM. The usual location is the conference room at Pavillon des Jardins (venue). If you wish to be informed by e-mail about upcoming seminars, please contact Stéphane Le Roux and Matthias Fuegger.
The seminar is open to public and does not require any form of registration.
In this talk I will review the stochastic logic CSL TA, a logic that has been defined to model-check Continuous Time Markov Chains. CSL TA extends the well-known stochastic logic CSL by allowing path properties to be defined through a Timed Automaton (TA). The price of this extension is an increase in the cost of the model checking algorithm both in terms of memory and of solution time: the model checking of CSL requires to solve one of more CTMCs, that of CSL TA the solution of a Markov Regenerative Process. I will then discuss how we can efficiently model check CSL TA properties, in particular I will present a model-checking algorithm that adapts itself to the formula, so that the memory and computational cost for the model checking of a CSL TA formula naturally scales down to that of the standard CSL model checking algorithm, when the property specified by the TA is equivalent to a CSL one. The technique is based on the construction of the region graph of the timed automata and on a component-based technique for the computation of the steady-state probability of Markov regenerative processes. The presentation will be supported by a demo with the GreatSPN tool developed in Torino.