Guillermo Alberto Perez associate professor

Research Guillermo Alberto Perez

Research team

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.

Synthesis of reactive systems from formal specifications and examples. 01/01/2024 - 31/12/2027

Abstract

The goal of synthesis is to automatically generate a program from a high-level specification of *what* it has to do, rather than *how* it must do it. Synthesis is difficult to realise for general purpose programming languages, and researchers have targeted application-specific domains, such as reactive systems. Reactive systems are programs in continuous interaction with their environment, and must react in a timely fashion to its inputs by producing some control actions. Their automatic synthesis is an ambitious challenge: the uncontrollable nature of the environment makes synthesis methods algorithmically demanding. However, important progresses have been made in the last decade, during which efficient synthesis tools have been developed. This algorithmic prowess has not been followed by a methodological shift in reactive system design. SynthEx identifies an important reason: synthesis methods do not offer easy solutions to control the quality of the synthesis systems. To get high-quality programs, current approaches need precise specifications which include both high-level critical properties and low-level implementational details. Writing such precise specifications is difficult even for experts. SynthEx proposes a new methodology where only the high-level critical properties must be provided, together with some examples of execution scenarios. Its goal is to provide theoretical foundations supporting this new methodology and experimentally assess it.

Researcher(s)

Research team(s)

Project type(s)

  • Research Project

Nexor - Cyber-Physical Systems for the Industry 4.0 era 01/01/2021 - 31/12/2026

Abstract

The fourth industrial revolution (Industry 4.0 as it is commonly referred to) is driven by extreme digitalization, enabled by tremendous computing capacity, smart collaborating machines and wireless computer networks. In the last six years, Nexor — a multi-disciplinary research consortium blending expertise from four Antwerp research labs — has built up a solid track record therein. We are currently strengthening the consortium in order to establish our position in the European eco-system. This project proposal specifies our 2021 - 2026 roadmap, with the explicit aim to empower industrial partners to tackle their industry 4.0 challenges. We follow a demand driven approach, convincing industrial partners to pick up our innovative research ideas, either by means of joint research projects (TRL 5—7) or via technology licenses.

Researcher(s)

Research team(s)

Project website

Project type(s)

  • Research Project

Dotation for the structural collaboration with Flanders Make. 01/01/2021 - 31/12/2024

Abstract

Flanders Make's mission is to strengthen the international competitiveness of the Flemish manufacturing industry on the long term through industry-driven, precompetitive, excellent research in the field of mechatronics, product development methods and advanced production technologies and by maximizing valorisation in these areas.

Researcher(s)

Research team(s)

Project type(s)

  • Research Project

DESCARTES - infectious DisEaSe eConomics and Ai with guaRanTEeS. 01/01/2021 - 31/12/2024

Abstract

In this proposal we focus on challenges regarding infectious diseases such as measles elimination and optimal influenza vaccination and draw motivation from fundamental questions with respect to healthcare prioritisation. Advancements in the fields of epidemic modelling, health economics and multi-agent learning paired with formally-verified guarantees can improve the effectiveness and reliability of the complex decision-making mechanisms needed to answer such questions. This complexity is situated in different aspects: the computational complexity, model structure and the interactions between multiple agents, in combination with multi-criteria objectives. Our consortium establishes a unique combination of leading expertise, which as a team not only will advance each of these fields, but also develops a new, internationally unique, multidisciplinary research line.

Researcher(s)

Research team(s)

Project type(s)

  • Research Project

Deterministic and inexpensive realizations of advanced control (DIRAC-SBO). 01/09/2020 - 28/02/2025

Abstract

The mechatronic machine building and manufacturing industry is currently facing various control challenges that simple PID controllers and alike fail to address: systems are increasingly complex, need to comply to constraints, need to account for economic objectives and effectively cope with valuable preview information. Model Predictive Control (MPC) is the only advanced control approach able to address all these challenges, and this thanks to its model-based and optimization-based nature. Yet MPC's optimization-based nature currently impedes wide adoption in industrial mechatronic systems: current MPC implementations are expensive in terms of computational and memory resources, computation time is non-deterministic and hence MPC algorithms cannot be certified to operate at a given sampling rate, MPC development and deployment is not straightforward and comes with a high engineering cost because proper tools are missing. The project "Deterministic and Inexpensive Realizations of Advanced Control" (DIRAC) aims for a breakthrough of MPC in the mechatronic/machine building/manufacturing industry by resolving all impeding elements through accomplishments that revolve around the three keywords in its title:  - Deterministic: Novel MPC algorithms and approaches will be developed that can run reliably at a given sampling rate as well as methods to verify their worst-case computation times and control performance.  - Inexpensive: Implementations will be created that approximate "full-blown" (=online nonlinear optimization with high fidelity models) MPC and hence can run on inexpensive computational hardware with a quantifiable impact on control performance that is computed upfront.  A modular MPC toolbox will be developed facilitating the development, tuning and validation of advanced control at manageable engineering cost. - Realizations: We will demonstrate the MPC toolbox and potential of MPC on industrially relevant demonstrators and validation cases in order to break the status-quo in control practices, foster take-up and inspire Flemish industry.  The overarching tangible reusable generic result of this project is a toolbox that simplifies design of nonlinear MPC controllers and brings methodological advances in solvers, approximations and validation techniques to the fingertips of control practitioners.

Researcher(s)

Research team(s)

Project type(s)

  • Research Project

SAILor: Safe Artificial Intelligence and Learning for Verification. 01/01/2020 - 31/12/2023

Abstract

Reactive synthesis is the act of automatically implementing a reactive system from a given formal specification so as to guarantee correctness by construction. It is especially useful when the desired system is safety critical, e.g. embedded controllers used in cars and ai lanes. Unfortunately, reactive synthesis is computationally hard and current synthesis tools are still not efficient enough to be used in practically relevant applications. Furthermore, systems obtained in this fashion tend to be overly pessimistic: since they must be correct regardless of what their environment does, they consider the environment to be fully antagonistic. This abstraction of reality is often too conservative. Recently, there has been a boom in the number of efficient artificial intelligence techniques applied to problems which are (theoretically) hard or even undecidable, while usually no formal correctness guarantees are given. These shortcomings raise the following question: Can we leverage machine learning techniques to implement better, more efficient synthesis tools? We propose to answer this question in two steps. First, we will study learning algorithms with formal correctness guarantees as well as the assumptions under which these guarantees are valid. Second, we will implement those algorithms and compare them against each other and the state-of-the-art synthesis tools based on automata and logic.

Researcher(s)

Research team(s)

Project type(s)

  • Research Project

CAST: Counter-Automata Algorithms for Software Verification Tools. 01/10/2019 - 30/09/2023

Abstract

Formal verification of reactive systems is an increasingly important research area of computer science. Modern systems now include features which make their design difficult and verifying their correctness very demanding. Companies such as Facebook and Amazon have teams dedicated to formally verifying their systems while, in academia, works on verification have already been lauded with two Turing awards in the last twenty years. As systems become more complex, more intricate models are required in order to capture their behaviour. Counter automata result from adding integer-valued counters to the widely studied model of finite automata. The formal verification community has found several uses for different classes of counter automata. This project aims at (i) contributing to the theory of automatic software verification --- in particular, model checking various classes of one-counter automata, (ii) translating those model-checking algorithms into semi-decision procedures implementable in existing interactive software verification tools, and (iii) guiding the development of the theory based on the limitations and capabilities of such tools.

Researcher(s)

Research team(s)

Project type(s)

  • Research Project