# LSV Seminar

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.

## Past Seminars

### The stochastic logic CSL TA and its efficient model-checking

- Date
- Tuesday, January 22 2019 at 11:00AM
- Place
- Pavillon des Jardins
- Speaker
- Susanna Donatelli (University of Torino, Italy and invited Prof. at LSV)

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.