Exposé

• Titre : Performance analysis of stochastic models through Hybrid Automata Specifications
• Intervenant : Paolo Ballarini (CentraleSupelec)

Résumé : The Hybrid Automata Specification Language (HASL) is a powerful formalism for expressing performance measures of discrete-state stochastic models. Its essence consists in employing a hybrid  automaton as a means for selecting   trajectories that fulfil  specific "dynamic" characteristics. For example trajectories that contains a certain pattern of  events whose occurrence fulfil specific timing constraints, or trajectories that match specific dynamic profiles, e.g. presence/absence of peaks of given height, etc.  A confidence-interval estimattion procedure is then used to  estimate the average value of specific statistics computed with respect to the selected trajectories. In this presentation I will give an overview of the HASL approach and demonstrate its effectiveness by looking at a couple of case studies. 


Keywords: Performance analysis, discrete-state stochastic models, statistical model-checking, temporal logic reasoning.