Oct. 7 - Quantitative Verification beyond Markov: Models, Techniques and Tools


The Department of Computer Science is happy to welcome Arnd Harmanns for a faculty colloquium on October 7 at 1p. Arnd is a postdoc in the Formal Methods and Tools group at the University of Twente in the Netherlands. The abstract for his talk, which will be presented in Room 115 of the New Computer Science building, is pasted below. 

Proper consideration of quantitative aspects is crucial to formally model and analyse many complex critical systems. We need to properly represent randomised and real-time behaviour in models, and we want to compute quantitative measures like the worst-case probability of failure during system lifetime or the expected energy consumption over  time. In this talk, I will present stochastic timed automata (STA) as a suitable and flexible formal model for this purpose. 

Many well-known  Markovian and real-time models, for example MDP, GSMP and timed automata, are special cases of STA. I will give an overview of the basic model checking approach for STA and highlight recent advances in dealing with large models and bounded properties. I will demonstrate the Modest Toolset, a modular multiple-formalism, multiple-solution implementation that supports STA-based modelling and analysis, before concluding with an outlook on stochastic hybrid systems.

Everyone is welcome to attend and CSE 600 students should sign in for class credit.