Guillermo Alberto Perez hoofddocent

Onderzoek Guillermo Alberto Perez

Onderzoeksgroep

Expertise

Development and study of automatic verification techniques. The latter include the theory and practice of model checking, automatic synthesis of reactive controllers, and the theory of learning with guarantees, amongst others.

Synthese van reactieve systemen uit formele specificaties en voorbeelden. 01/01/2024 - 31/12/2027

Abstract

Het doel van synthese is om automatisch een programma van een hoog niveau te genereren specificatie van *wat* het moet doen, in plaats van *hoe* het het moet doen. Synthese is moeilijk te realiseren voor algemene programmeertalen, en onderzoekers hebben zich gericht op toepassingsspecifieke domeinen, zoals reactief systemen. Reactieve systemen zijn programma's die continu met elkaar in wisselwerking staan met hun omgeving, en moeten tijdig reageren door enkele besturingsacties te produceren. Hun automaat synthese is uitdagend: de oncontroleerbare aard van de omgeving maakt synthesemethoden algoritmisch veeleisend. Echter, belangrijke vorderingen zijn gemaakt in het afgelopen decennium, waarin er zijn efficiënte synthesetools ontwikkeld. Dit is niet gevolgd door een methodologische verschuiving in reactief systeemontwerp. SynthEx identificeert een belangrijke reden: synthesemethoden bieden geen gemakkelijke oplossingen om de kwaliteit van de synthese systemen. Om programma's van hoge kwaliteit te krijgen, hebben de huidige benaderingen nodig nauwkeurige specificaties die zowel kritieke eigenschappen op hoog niveau omvatten als implementatiedetails op laag niveau. SynthEx stelt een nieuwe methodologie voor waarbij alleen de kritische eigenschappen op hoog niveau moeten worden verstrekt, samen met enkele voorbeelden van uitvoeringsscenario's. Het doel is om een theoretische basis te leggen deze nieuwe methodologie te ondersteunen en experimenteel te beoordelen.

Onderzoeker(s)

Onderzoeksgroep(en)

Project type(s)

  • Onderzoeksproject

Nexor - Cyber-fysische systemen ten bate van de vierde industriële revolutie 01/01/2021 - 31/12/2026

Abstract

De vierde industriële revolutie (Industrie 4.0 zoals het vaak wordt genoemd) wordt aangedreven door extreme digitalisatie, mogelijk gemaakt door een enorme rekenkracht, gestuurd door slimme machines en draadloze netwerken. In de laatste zes jaar heeft Nexor — een multidisciplinair samenwerkingsverband tussen vier Antwerpse onderzoekslaboratoria — daar een solide portfolio opgebouwd. Momenteel versterken we het consortium om ons toe te laten door te groeien tot een gevestigde waarde in het Europese landschap. Het voorliggende projectvoorstel beschrijft onze plannen voor 2021 - 2026, met de expliciete bedoeling om industriële partners in staat te stellen hun Industrie 4.0 uitdagingen aan te pakken. We volgen daarbij een vraaggedreven aanpak, om toekomstige partners te overtuigen onze innovatieve ideeën op te pikken. We mikken daarbij onder andere op gezamenlijke onderzoeksprojecten (TRL5—7) en licentieovereenkomsten.

Onderzoeker(s)

Onderzoeksgroep(en)

Project website

Project type(s)

  • Onderzoeksproject

Dotatie i.k.v. structurele samenwerking met Flanders Make. 01/01/2021 - 31/12/2024

Abstract

Flanders Make heeft als missie het versterken van de internationale competitiviteit van de Vlaamse maakindustrie op lange termijn door industriegedreven, precompetitief, uitmuntend onderzoek uit te voeren op het gebied van mechatronica, productontwikkelingsmethodes en geavanceerde productietechnologieën en door valorisatie in deze domeinen te maximaliseren.

Onderzoeker(s)

Onderzoeksgroep(en)

Project type(s)

  • Onderzoeksproject

DESCARTES - infectieziekten economie en artificiële intelligentie met garanties. 01/01/2021 - 31/12/2024

Abstract

We richten ons op uitdagingen met betrekking tot infectieziekten, zoals het indijken van de COVID-19 pandemie, de eliminatie van mazelen en optimale influenzavaccinatie, mede gemotiveerd door fundamentele vragen rond de priorisering van gezondheidszorg. De beoogde ontwikkelingen op het vlak van epidemiologische modellen, gezondheidseconomie en AI-leeralgoritmen, in combinatie met formeel geverifieerde eigenschappen, zullen de effectiviteit en betrouwbaarheid verbeteren van de complexe besluitvorming die zulke vragen vereisen. De complexiteit situeert zich op verschillende vlakken: het computationele, de modelstructuren en de interacties tussen agenten, in combinatie met meerdere te optimaliseren objectieven. Ons consortium brengt een unieke combinatie van expertise samen, die als team niet enkel elk van deze onderzoeksdomeinen versterkt, maar ook een nieuwe, internationaal unieke, multidisciplinaire onderzoekslijn uitzet.

Onderzoeker(s)

Onderzoeksgroep(en)

Project type(s)

  • Onderzoeksproject

Deterministische en goedkope realisaties van geavanceerde controle (DIRAC-SBO). 01/09/2020 - 28/02/2025

Abstract

De mechatronische machinebouw en productie-industrie wordt momenteel geconfronteerd met verschillende regeltechniekuitdagingen die eenvoudige PID-regelaars en dergelijke niet aankunnen: systemen worden steeds complexer, moeten voldoen aan beperkingen, moeten rekening houden met economische doelstellingen en moeten effectief omgaan met waardevolle informatie. Model Predictive Control (MPC) is de enige geavanceerde besturingsaanpak die al deze uitdagingen kan aanpakken, en dit dankzij het modelmatige en op optimalisatie gebaseerde karakter. Toch belemmert de op optimalisatie gebaseerde aard van MPC momenteel een brede toepassing in industriële mechatronische systemen: de huidige MPC-implementaties zijn duur in termen van reken- en geheugenbronnen, de rekentijd is niet-deterministisch en daarom kunnen MPC-algoritmen niet worden gecertificeerd om met een bepaalde bemonsteringssnelheid te werken, de ontwikkeling en toepassing van MPC is niet eenvoudig en brengt hoge techniekkosten met zich mee omdat de juiste hulpmiddelen ontbreken. Het project "Deterministische en goedkope Realisaties van Geavanceerde Controle" (DIRAC) streeft naar een doorbraak van MPC in de mechatronische/machinebouw/fabricage industrie door het oplossen van alle belemmerende elementen door middel van prestaties die draaien om de drie trefwoorden in de titel:  - Deterministisch: Er zullen nieuwe MPC-algoritmen en -benaderingen worden ontwikkeld die betrouwbaar kunnen werken bij een bepaalde bemonsteringssnelheid, evenals methoden om hun slechtst denkbare rekentijden en controleprestaties te verifiëren.  - Goedkoop: Er zullen implementaties worden gecreëerd die "full-blown" (=onlineaire niet-lineaire optimalisatie met high fidelity modellen) MPC benaderen en dus kunnen draaien op goedkope computer hardware met een kwantificeerbare impact op de controleprestaties die vooraf wordt berekend.  Er zal een modulaire MPC toolbox worden ontwikkeld die de ontwikkeling, tuning en validatie van geavanceerde controle mogelijk maakt tegen beheersbare technische kosten. - Realisaties: We zullen de MPC toolbox en het potentieel van MPC demonstreren op industrieel relevante demonstratoren en validatiegevallen om de status-quo in de controlepraktijk te doorbreken, de acceptatie te bevorderen en de Vlaamse industrie te inspireren.  Het overkoepelende tastbare, herbruikbare generieke resultaat van dit project is een toolbox die het ontwerp van niet-lineaire MPC-controllers vereenvoudigt en methodologische vooruitgang in solvers, benaderingen en validatietechnieken aan de vingertoppen van controlebeoefenaars brengt.

Onderzoeker(s)

Onderzoeksgroep(en)

Project type(s)

  • Onderzoeksproject

SAILor: Veilige Kunstmatige Intelligentie en Leren voor Verificatie. 01/01/2020 - 31/12/2023

Abstract

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.

Onderzoeker(s)

Onderzoeksgroep(en)

Project type(s)

  • Onderzoeksproject

CAST: Tellerautomatenalgoritmes voor Softwareverificatietools. 01/10/2019 - 30/09/2023

Abstract

Formele verificatie van reactieve systemen is een steeds belangrijker onderzoeksgebied van informatica. Moderne systemen bevatten nu functies die hun ontwerp moeilijk maken en die ervoor zorgen dat het controleren van hun juistheid zeer veeleisend is. Bedrijven zoals Facebook en Amazon hebben teams die zich toeleggen op het formeel verifiëren van hun systemen, terwijl in de academische wereld de het werk op het gebied van verificatie in de afgelopen twintig jaar zijn geprezen met twee Turing-awards. Naarmate systemen complexer worden, zijn er meer ingewikkelde modellen nodig om hun gedrag vast te leggen. Tellerautomaten resulteren uit het toevoegen van geheel-getal waarde tellers aan het algemeen bestudeerde model van eindige automaten. De formele verificatiegemeenschap heeft verschillende toepassingen gevonden voor verschillende klassen van tellerautomaten. Dit project heeft tot doel (i) bij te dragen aan de theorie van automatische software verificatie --- model-checking van eentellerautomaten (ii) algoritmes voor model-checking te vertalen naar semi-beslissingsprocedures die implementeerbaar zijn in bestaande interactieve software verificatiehulpmiddelen en (iii) het sturen van de ontwikkeling van de theorie op basis van de beperkingen en mogelijkheden van dergelijke hulpmiddelen.

Onderzoeker(s)

Onderzoeksgroep(en)

Project type(s)

  • Onderzoeksproject