This thesis goal is to provide Alchemist with a module able to run approximate stochastic model checking. Roughly, those steps will be required:

• Deep understanding of the Approximate Stochastic Model Checking
• Deep understanding of Alchemist's model and engine
• Definition of the concept of "parameter" for a generic simulation
• Definition of the concept of "observable status"
• Creation of a (possibly multithreaded, possibly distributed) executor for multiple simulations

Mirko Viroli (Contact)

Mirko Viroli (Supervisor)

Danilo Pianini (Co-supervisors)