Informatica & AI

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.

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.

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.

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.

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.

Semantiek, Types & Logica (STyLo)

Het werk van de STyLo groep draait om correctheid van systemen door constructie, en de verificatie en analyse van systemen. Om systemen te implementeren die voldoen aan gewenste eigenschappen door constructie, heeft men talen nodig die deze eigenschappen statisch garanderen. We richten ons op het gebruik van typesystemen, omdat deze compositorisch redeneren mogelijk maken. Inzicht in het geïnduceerde gedrag van zulke talen wordt verkregen door hun semantiek, die we ontwikkelen met hulpmiddelen uit de categorietheorie en andere gebieden van de wiskunde. Interessant is dat dezelfde gereedschappen die we gebruiken om typesystemen te construeren en te analyseren ook gebruikt kunnen worden als basis voor logische deductiesystemen. Zulke deductiesystemen liggen ten grondslag aan de verificatie en analyse van systemen, zowel in de vorm van computerondersteunde bewijzen als in automatische deductie. We kiezen ervoor om ons te richten op compositioneel en computerondersteund redeneren, omdat ze de sleutel zijn tot het omgaan met de complexiteit van het construeren en analyseren van grote systemen.

Logica en computatie zijn onlosmakelijk met elkaar verbonden als ze door de juiste lens worden bekeken. In de STyLo groep gebruiken we categorietheorie, typetheorie en taalsemantiek als zulke lenzen om ons werk te structureren en nieuwe inzichten te krijgen in hoe de onderdelen ontwikkeld kunnen worden. Het voordeel van het gebruiken en ontwikkelen van abstracte theorieën is dat ze gemakkelijk toepasbaar zijn op systemen in verschillende gebieden van bijvoorbeeld computerwetenschap, natuurkunde, biologie en scheikunde.

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.