Theorie

Veel belangrijke onderwerpen in de informatica, zoals de juistheid van software, de efficiëntie van algoritmen en de modellering van gecompliceerde systemen, zijn afhankelijk van een goede theoretische onderbouwing. In de Theoriegroep bestuderen we deze fundamentele bouwstenen en ontwikkelen we verificatiemethoden om systeemcorrectheid, nieuwe (kwantum)algoritmen en fundamentele modellen van concurrentie- en infinite-state systemen aan te tonen.

Algoritmen

We ontwikkelen combinatorische algoritmen, bijvoorbeeld voor gebruik in verschillende soorten spellen, met een speciale nadruk op algoritmen die in de biologie kunnen worden toegepast. We werken ook aan schaalbare algoritmen voor het analyseren van netwerksystemen in de echte wereld. Voorbeelden hiervan zijn rekenkundige benaderingen voor het berekenen van afstandsmetingen zoals de diameter, maar ook het efficiënt tellen van karakteristieke grafiekpatronen.

Bio-geïnspireerd computergebruik

We onderzoeken reactiesystemen, een nieuw rekenmodel dat voortkomt uit de biochemische reacties die plaatsvinden in levende cellen en informatieverwerking in de natuur. Andere formele modellen geïnspireerd door moleculaire reacties binnen cellen zijn membraan- en weefselsystemen. Hiervoor ontwikkelen we een causaliteitssemantiek volgens een op Petri-net gebaseerde benadering. Een andere niet-traditionele benadering van computing is DNA-computing. Deze is gebaseerd op de hardware van de moleculaire biologie. We gebruiken algebraïsche en combinatorische technieken om deze computationele processen te modelleren en te analyseren, zoals het herschikken van genen.

Gelijktijdige systemen

In moderne informatiesystemen zijn vaak een groot aantal verschillende componenten tegelijkertijd actief. Dit fenomeen - bekend als gelijktijdigheid - ligt niet alleen ten grondslag aan het functioneren van computersystemen, maar aan elk systeem waarin vele processen tegelijkertijd plaatsvinden. Het leidt tot een grote verscheidenheid aan gecompliceerde interacties die het algehele functioneren van het systeem beïnvloeden. Het doel van ons onderzoek naar gelijktijdige systemen is om deze interacties te begrijpen en te modelleren en het effect ervan te beschrijven. We onderzoeken Petri-netten en andere modellen van gelijktijdige en gedistribueerde systemen, zoals teamautomaten. Onze focus ligt op semantische aspecten, synthese en formele analyse- en verificatietechnieken. Dit onderzoek profiteert van onze expertise en het lopende theoretische onderzoek op het gebied van wiskundige structuren, logica, formele talen en automata. We passen onze inzichten toe op en worden gemotiveerd door biologische systemen, hardware (asynchrone circuits) en bedrijfsprotocollen (bijv. groupware en financiële markten). In samenwerking met het CWI onderzoeken we de ontwikkeling, implementatie en toepassingen van Reo, een exogeen coördinatiemodel voor de bouw van coördinerende connectoren in gedistribueerde, mobiele en dynamisch herconfigureerbare component-gebaseerde systemen.

Quantum Lab

Quantumcomputing is een nieuw paradigma voor de berekening, dat met de komende generatie van beperkte, maar niettemin krachtige quantumapparaten de impact in de echte wereld nadert. We bestuderen en ontwikkelen nieuwe algoritmen voor algemene kwantumcomputers, gespecialiseerde algoritmen voor machines op korte termijn, en hybride algoritmische methoden die klassieke en kwantumberekening combineren. In het bijzonder richten we ons op de ontwikkeling van kwantumalgoritmische funderingen voor heuristisch computergebruik en machinaal leren. Samen met het initiatief Applied Quantum Algorithms (aQa) in Leiden bestuderen we ook de toepassing van onze methoden op real-world problemen, en de integratie van theorie, experiment en real-world toepassing.

Systems Modelling Lab (SML)

Wiskundige modellen van softwaresystemen maken karakteriseringen, abstracties, simulaties en analyses van complexe software mogelijk tijdens de ontwikkeling ervan. Het gebruik van wiskundige technieken op het gebied van algebra, coalgebra, automatiseringstheorie, logica, typetheorie en categorietheorie maakt formele specificatie en analyse mogelijk, die bijdragen aan het juiste ontwerp en de juiste implementatie van een softwaresysteem. We ontwikkelen nieuwe wiskundige technieken die nodig zijn voor het omgaan met de huidige en toekomstige kenmerken van softwaresystemen. Verder ontwikkelen we rigoureuze modellen en krachtige algoritmen voor het redeneren over moderne objectgeoriënteerde programma's, gelijktijdige en probabilistische systemen, coördinatietalen en softwaregedefinieerde netwerken. We onderzoeken ook de toepassing van de modellerings- en redeneringstechnieken op andere systemen die buiten de computerwetenschap ontstaan.

System Verification Lab (SVL)

De juistheid van computersystemen is van groot belang voor onze samenleving, omdat deze steeds meer afhankelijk wordt van de voordelen van de informatica. We bestuderen een scala aan benaderingen voor het formeel modelleren en verifiëren van computersystemen om kostbare bugs op te sporen en correcte implementaties te realiseren. Met behulp van symbolische redeneringstechnieken van kunstmatige intelligentie maken we de volautomatische verificatie van grotere systemen mogelijk door middel van een methode die modelchecken wordt genoemd. In samenwerking met het Concurrent Systems Lab ontwikkelen we reductietechnieken met hetzelfde doel. En in samenwerking met het Quantum en Algoritmes Lab ontwikkelen we nieuwe kwantum- en parallelle algoritmen om de kracht van de volgende generatie computersystemen te benutten voor verificatie. De toegevoegde rekenkracht is ook nodig om het gedrag van stochastische processen te analyseren, zoals de processen die ten grondslag liggen aan de risicoanalyse van de infrastructuur van het elektriciteitsnet. In samenwerking met de industrie vormt dit een ander toepassingsgebied voor ons onderzoek.