|title:||Model checking random graphs|
|topics:||Algorithms and Data Structures , Logics and semantics|
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?