Bachelor Scripties

Algemeen

Op deze pagina beschrijf ik wat suggesties voor bachelor scriptie projecten. Een bachelor scriptie project moet je interesseren, fascineren, en je moet het leuk vinden. Wanneer je zelf een onderwerp hebt bedacht juich ik dat toe, ook al heeft het niet direct te maken met mijn eigen onderzoek. Natuurlijk moet er wel een duidelijke relatie zijn met Informatica/Informatiekunde, en als een andere docent meer over een onderwerp weet dan zal ik je daar naar verwijzen. Afhankelijk van je belangstelling kan ik theoretische maar ook zeer practische opdrachten begeleiden.

Frits Vaandrager

Projecten

• Op dit moment hebben we goede theorie en software tools voor het leren van eindige automaten, gebaseerd op het L* algoritme van Dana Angluin. Maar in de praktijk zijn er veel protocollen met real-time gedrag zoals timeouts. Met wat trucs kunnen we daar in de praktijk toch wel modellen van leren maar dit is ad hoc. In Zweden is er onderzoek gedaan over hoe je het algoritme van Angluin kunt veralgemeniseren naar getimede automaten, een uitbreiding van eindige automaten waarmee je real-time kunt modelleren (zit ook in Uppaal). Maar de Zweedse algoritmen zijn hopeloos inefficient. Ik denk dat het mogelijk is om een efficiente uitbreiding van Angluin's algoritme te verzinnen wanneer je kijkt naar een deelklasse van getimede automaten. Dit is een overzichtelijk theoretisch project.
• Een goed overzichtsartikel van Angluin-style leeralgoritmen voor eindige automaten is recent geschreven door Steffen et al. Er staan allemaal algoritmen in met claims over de correctheid, maar die claims worden niet echt in detail uitgewerkt. Een mogelijk project zou zijn om de correctheidsbewijzen van een aantal algoritmen veel meer in detail uit te werken, bijvoorbeeld met behulp van Hoare logica. Dit is een overzichtelijk theoretisch project.
• Tijdens de cursus Processen heb je leren werken met de model checker Uppaal. Uppaal doorzoekt alle bereikbare toestanden van een model om te bepalen of een bepaalde eigenschap geldt. Het probleem is dat het aantal toestanden vaak expodeert wanneer het aantal processen te groot wordt. Om met dit probleem om te gaan is er recent een statistische versie van Uppaal uitgekomen. Het idee is dat je voor alle nondeterminische keuzes in het model kansverdelingen geeft die vertellen hoe waarschijnlijk een bepaalde keuze is. Vervolgens ga je niet alle toestanden doorzoeken maar met Monte Carlo simulaties een beperkt aantal runs doen. Gebruikmakend van statistiek kun je vervolgens laten zien dat bepaalde eigenschappen gelden (gegeven een bepaalde foutkans). Tijdens deze opdracht zou je onderzoeken of het gebruik van Uppaal SMC (voor Statistical Model Checking) meerwaarde oplevert boven standaard Uppaal door een case studie die eerder met Uppaal is gedaan over te doen in Uppaal SMC. Een geschikte case study zou bijvoorbeeld het Zeroconf protocol zijn. Wanneer je waarschijnlijkheidsleer en statistiek interessant vindt, en het leuk vindt om met Uppaal te spelen is dit een geschikt project.

Interesse?

Loop langs op mijn kamer of stuur me een mailtje.