|
An Expressive Language for Statistical Verification of Stochastic Models| old_uid | 9467 |
|---|
| title | An Expressive Language for Statistical Verification of Stochastic Models |
|---|
| start_date | 2010/12/17 |
|---|
| schedule | 15h-15h30 |
|---|
| online | no |
|---|
| location_info | batiment d’Alembert, Amphithéâtre Fonteneau |
|---|
| details | joint work with P. Ballarini, M. Duflot, S. Haddad and N. Pekergin |
|---|
| summary | Being inspired by existing stochastic logic, such as, the Continuous Stochastic Logic CSL and its following action-state asCSL and timed automata CSLTA evolutions, SHAL extends them in two respects: firstly it targets a much broader class of stochastic models (i.e. DESP rather than Markov chains); secondly it increases the expressiveness of verification by allowing to capture sophisticated dynamics expressed in terms of multivariate conditions. A formula of SHAL consists of a Linear Hybrid Automaton (LHA) and an expression. The LHA selects prefixes of relevant execution paths of a DESP and collects information along the paths. The result of the formula verification is the evaluation of an expression of the considered path random variable. A statistical engine is then employed for the confidence-interval estimation of the expected value of the expression associated to an LHA. We illustrate the SHAL approach by means of some examples and experimental results obtained through a prototype software tool for SHAL verification. |
|---|
| responsibles | Baerecke |
|---|
| |
|