Inria
Inria.fr
Inria Channel
Séminaire : CONTRAINTES
Hybrid Automata Stochastic Logic: expressive statistical verification of stochastic models
Entrée libre.
Horaire : 14 h 00
- Date : 11/04/2011
- Lieu : Inria Rocquencourt, Bâtiment 8
- Intervenants : Paolo Ballarini
- Organisateurs : CONTRAINTES
We introduce the Hybrid Automata Stochastic Logic (HASL), a new temporal logic formalism for the verification of discrete event stochastic processes (DESP). HASL employs Linear Hybrid Automata (LHA) as machineries to select prefixes of relevant execution paths of a DESP. The advantage with LHA is that rather elaborate information can be collected "on-the-fly" during path selection, providing the user with a powerful means to express sophisticated measures. A formula of HASL consists of an LHA (A) and an expression (Z) referring to moments of "path random variables". A (simulation-based) statistical engine is employed to obtain a confidence-interval estimate of the expected value of Z. In essence HASL provides a unifying verification framework where sophisticated temporal reasoning is naturally blended with elaborate reward-based analysis. In this talk I will illustrate the HASL approach and a discuss about its expressivity. I will also present preliminary empirical evidence obtained through COSMOS, a prototype software tool for HASL verification.
Mots-clés : Séminaire Paris - Rocquencourt CONTRAINTES
