Project Details
VESCAA: Verifikovatelná a efektivní syntéza kontrolerů
Project Period: 1. 3. 2023 - 31. 12. 2025
Project Type: grant
Code: GA23-06963S
Agency: Czech Science Foundation
Program: Standardní projekty
Decision making under uncertainty; controller design; safety and scalalbility; inductive synthesis; reinforcement learning, risk-aware learning;
Many modern computing systems can be seen as (semi)-autonomous agents interacting with their environment. The agent's behaviour is determined by a controller that necessarily needs to deal with uncertainties including unpredictability of the environment and the imprecision of data gathered about its current state. There exists a multitude of approaches to automated controller design, however, they all tackle the safety-scalability gap: scalability limits the complexity of the problems that can be handled and safety ensures that agent operates in a safe and interpretable way. There are two principal approaches: formal methods prioritize safety and reinforcement learning prioritizes scalability.
The project aims at developing theoretical foundation and synthesis algorithms that reduce this gap and thus improve their practical applicability. The key idea is to adapt, further develop and synergically integrate two emerging paradigms: inductive synthesis improving the scalability of correct-by-construction design techniques and risk-aware learning improving the safety guarantees.
Andriushchenko Roman, Ing. (DITS FIT BUT)
Gaďorek Petr, Ing. (OIP FIT BUT)
Hudák David, Ing. (DITS FIT BUT)
Macák Filip, Ing. (DITS FIT BUT)
Malásková Věra (DITS FIT BUT)
Mrázek Vojtěch, Ing., Ph.D. (DCSY FIT BUT)
Nesvedová Šárka (DEAN FIT BUT)
Oravcová Marcela, Ing. (DEAN FIT BUT)
Paulíková Barbora, Mgr. (DEAN FIT BUT)
Štanclová Eva (DEAN FIT BUT)
Štursová Markéta, Ing. (DEAN FIT BUT)
Ventrubová Hana (DEAN FIT BUT)
2024
- ANDRIUSHCHENKO Roman, ČEŠKA Milan, JUNGES Sebastian and MACÁK Filip. Policies Grow on Trees: Model Checking Families of MDPs. In: Proceeding of 22nd International Symposium on Automated Technology for Verification and Analysis. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Cham: Springer Verlag, 2024, p. 13. Detail
2023
- ANDRIUSHCHENKO Roman, BARTOCCI Ezio, ČEŠKA Milan, FRANCESCO Pontiggia and SARAH Sallinger. Deductive Controller Synthesis for Probabilistic Hyperproperties. In: Quantitative Evaluation of SysTems. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 14287. Cham: Springer Verlag, 2023, pp. 288-306. ISBN 978-3-031-43834-9. Detail
- ANDRIUSHCHENKO Roman, ALEXANDER Bork, ČEŠKA Milan, JUNGES Sebastian, KATOEN Joost-Pieter and MACÁK Filip. Search and Explore: Symbiotic Policy Synthesis in POMDPs. In: Computer Aided Verification. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 13966. Cham: Springer Verlag, 2023, pp. 113-135. ISBN 978-3-031-37708-2. Detail