title: Model checking random graphs
topics: Algorithms and Data Structures , Logics and semantics
committee: Mariƫlle Stoelinga ,
Hajo Broersma


Model checking is a well-known technique to verify if a certain property holds for a given labeled transition system or finite state machine.

This BSc project is about model checking properties over random graphs: what happens if we generate (according to some procedure) a graph at random and then verify our property. What is the probability that this property hold? Certain properties will hold with probability 1; can we characterize these? And: how are these question affected by the generation procedure?