SAILor: Veilige Kunstmatige Intelligentie en Leren voor Verificatie.

Reactieve synthese is de handeling van het automatisch implementeren van een reactief systeem uit een gegeven formele specificatie om zo de juistheid door constructie te garanderen. Het is vooral nuttig wanneer het gewenste systeem veiligheidskritisch is, b.v. ingebedde controllers die worden gebruikt in auto's en vliegtuigen. Helaas is reactieve synthese rekenkundig moeilijk en zijn de huidige synthesetools nog niet efficiënt genoeg om in praktisch relevante toepassingen te worden gebruikt. Bovendien zijn systemen die op deze manier zijn verkregen over het algemeen pessimistisch: omdat ze correct moeten zijn, ongeacht wat hun omgeving doet, beschouwen ze de omgeving als volledig antagonistisch. Deze abstractie van de werkelijkheid is vaak te conservatief. Onlangs is het aantal efficiënte kunstmatige intelligentie-technieken sterk toegenomen en zij worden toegepast op problemen die (theoretisch) moeilijk of zelfs onbeslisbaar zijn terwijl er gewoonlijk geen formele correctheidsgaranties worden gegeven. Deze tekortkomingen brengen de volgende vraag met zich mee: kunnen we gebruikmaken van machinale leertechnieken om betere, efficiëntere synthesetools te implementeren? We stellen voor om deze vraag in twee stappen te beantwoorden: we zullen leeralgoritmen bestuderen met formele correctheidsgaranties en de algoritmen implementeren en met elkaar en met de ultramoderne synthesetools vergelijken.

Trefwoorden:SOFTWAREVERIFICATIE

Disciplines:Machine learning en besluitvorming, Analyse van algoritmen en complexiteit, Computationele logica en formele talen