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, 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.)