VESCAA: Verifikovatelná a efektivní syntéza kontrolerů

Název anglicky

VESCAA: Verifiable and Efficient Synthesis of Agent Controllers

Typ

grant

Klíčová slova

Řízení agentů v nejistém prostředí; automatizovaný návrh systémů; bezpečnost a škálovatelnost; induktivní syntéza; zpětnovazebné učení; risk-aware učení;

Abstrakt

Mnohé počítačové systémy mohou být chápány jako (semi-)autonomní agenti, kteří interagují se svým prostředím. Chování těchto agentů je řízeno pomocí tzv. kontrolerů, které musí nezbytně brát do úvahy různé formy neurčitosti pramenící zejména z nepredikovatelného chování prostředí a z nepřesnosti dat, které sbírají o svém stavu. Existuje několik přístupů pro automatizovaný návrh kontrolerů, ale jejich reálné nasazení je limitované buď omezenou škálovatelností nebo zárukami, které mohou poskytnout na bezpečnost výsledných kontrolerů: formální metody se typicky soustředí na bezpečnost zatímco metody strojové učení na škálovatelnost.

Cílem tohoto projektu je vývoj teoretických základů a syntetizačních algoritmů, které dovolí redukovat tyto limity a tak zásadně zlepšit aplikovatelnost automatizovaného návrhu kontrolerů. Hlavní vizí projektu je adaptovat, dále vyvinout a synergicky integrovat nově vznikající paradigmata: induktivní syntézu, která vylepšuje škálovatelnost formálních metod a risk-aware učení, které vylepšuje garance bezpečnosti výsledných kontrolerů.

Řešitelé

Češka Milan, doc. RNDr., Ph.D. (UITS FIT VUT) , hlavní řešitel
Andriushchenko Roman, Ing. (UITS FIT VUT)
Gaďorek Petr, Ing. (DFIT-OIP)
Hudák David, Ing. (UITS FIT VUT)
Macák Filip, Ing. (UITS FIT VUT)
Malásková Věra (UITS FIT VUT)
Mrázek Vojtěch, Ing., Ph.D. (UPSY FIT VUT)
Nesvedová Šárka (Děkanát FIT VUT)
Oravcová Marcela, Ing. (Děkanát FIT VUT)
Paulíková Barbora, Mgr. (Děkanát FIT VUT)
Štanclová Eva (Děkanát FIT VUT)
Štursová Markéta, Ing. (Děkanát FIT VUT)
Ventrubová Hana (Děkanát FIT VUT)

Podpora

Publikace

2025

ANDRIUSHCHENKO Roman, ČEŠKA Milan, JUNGES Sebastian, KATOEN Joost-Pieter a MACÁK Filip. An Oracle-Guided Approach to Constrained Policy Synthesis Under Uncertainty. Journal of Artificial Intelligence Research, roč. 2025, č. 82, s. 433-469. ISSN 1076-9757. Detail
ANDRIUSHCHENKO Roman, ČEŠKA Milan, FRANCESCO Pontiggia, MACÁK Filip a MICHELE Chiari. Decentralized Planning Using Probabilistic Hyperproperties. In: Proc. of the 24th International Conference on Autonomous Agents and Multiagent Systems. 2025. Detail
ANDRIUSHCHENKO Roman, ČEŠKA Milan, JUNGES Sebastian a 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, 2025, s. 51-75. ISBN 978-3-031-78749-2. Detail

2024

ANDRIUSHCHENKO Roman, ARND Hartmanns, ČEŠKA Milan, JUNGES Sebastian a KŘETÍNSKÝ Jan a kol. Tools at the Frontiers of Quantitative Verification: QComp 2023 Competition Report. In: International TOOLympics Challenge. Lecture Notes in Computer Science. Cham: Springer Nature Switzerland AG, 2024, s. 90-146. ISBN 978-3-031-67694-9. Detail

2023

ANDRIUSHCHENKO Roman, BARTOCCI Ezio, ČEŠKA Milan, FRANCESCO Pontiggia a 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), roč. 14287. Cham: Springer Verlag, 2023, s. 288-306. ISBN 978-3-031-43834-9. Detail
ANDRIUSHCHENKO Roman, ALEXANDER Bork, ČEŠKA Milan, JUNGES Sebastian, KATOEN Joost-Pieter a 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), roč. 13966. Cham: Springer Verlag, 2023, s. 113-135. ISBN 978-3-031-37708-2. Detail