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

Parameter Synthesis for Probabilistic Timed Reachability

Tuesday, January 13 2009 at 11:00AM
Salle de Conférence (Pavillon des Jardins)
Joost-Pieter Katoen (Software Modeling and Verification Group (MOVES), RWTH Aachen)

In this talk, we propose a technique to synthesize parametric rate values in continuous-time Markov chains that ensure the validity of time-bounded reachability properties. Rate expressions over variables indicate the average speed of state changes and are expressed using the polynomials over reals. The key contribution is an algorithm that approximates the set of parameter values for which the stochastic real-time system guarantees the validity of bounded reachability properties. This algorithm is based on discretizing parameter ranges together with a refinement technique. We will describe the algorithm, analyze its time complexity, and show its applicability by deriving parameter constraints for a real-time storage system with probabilistic error checking facilities.

(This is joint work with Tingting Han and Alexandre Mereacre.)

About LSV