Room 206 (2nd floor, badged access)
22 février 2024 - 14h00
Hybrid-Automata Specification Language: from expressive stochastic model checking to parametric stochastic model checking
par Paolo Ballarini de CentraleSupélec - MCIS
Abstract: Probabilistic model checking is concerned with providing modellers with an effective means for automatically assessing with what probability a model exhibits a given behaviour formally expressed by a temporal logic specification. The ability to capture relevant behaviours depends on the expressiveness of the considered property language and in this respect the Hybrid Automata Specifications Language (HASL) has proved a powerful means which exceeds the expressiveness of classical temporal logics. HASL model checking is a simulation-based procedure: given a probabilistic model M and a HASL specification F the expected value of the quantity captured by F is estimated by sampling trajectories of the product process M x F. In this talk I am going first to give an overview of the HASL model checking approach and then discuss how, taking advantage of HASL expressiveness, we can characterise a procedure that allows for tuning the parameters of a probabilistic model so that it meets a given behaviour. Otherwise said we introduce a procedure for reverse engineering of a probabilistic model w.r.t. a temporal property, something which is also known as parametric model checking. The parametric model checking problem is as follows: given a model M that depends on a set of parameters P and a behavior of interest expressed by a specification F assess how the probability that F is satisfied by M varies over the domain of the parameters P. The formulation of parametric model checking based on HASL relies on the characterisation of satisfiability distance (i.e. how far a model's trajectory is from satisfying a specification F) and on the corresponding hybrid-automaton for measuring it. The searching of the parameter-space is obtained through the adaptation of the Approximated Bayesian Computation (ABC) method obtained by plugging in the satisfiability-distance automaton.
Candidat potentiel sur un poste à Verimag.
