Detail projektu

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

Období řešení: 1. 3. 2023 – 31. 12. 2025

Typ projektu: grant

Kód: GA23-06963S

Agentura: Grantová agentura České republiky

Program: Standardní projekty

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) – hlavní řešitel
Andriushchenko Roman, Ing. (UITS)
Gaďorek Petr, Ing. (DFIT-OIP)
Hudák David, Ing. (UITS)
Macák Filip, Ing. (UITS)
Malásková Věra (UITS)
Mrázek Vojtěch, Ing., Ph.D. (UPSY)
Nesvedová Šárka (DFIT-PO)
Oravcová Marcela, Ing. (DFIT-EO)
Paulíková Barbora, Mgr. (DFIT-PO)
Štanclová Eva (DFIT-EO)
Štursová Markéta, Ing. (DFIT-EO)
Ventrubová Hana (DFIT-EO)
Publikace

2025

  • ANDRIUSHCHENKO, R.; ČEŠKA, M.; MACÁK, F.; JUNGES, S. Policies Grow on Trees: Model Checking Families of MDPs. 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. p. 51-75. ISBN: 978-3-031-78749-2. Detail
  • MACÁK, F.; ANDRIUSHCHENKO, R.; ČEŠKA, M.; FRANCESCO, P.; MICHELE, C. Decentralized Planning Using Probabilistic Hyperproperties. Proc. of the 24th International Conference on Autonomous Agents and Multiagent Systems. 2025. Detail
  • MACÁK, F.; ANDRIUSHCHENKO, R.; ČEŠKA, M.; JUNGES, S.; KATOEN, J. An Oracle-Guided Approach to Constrained Policy Synthesis Under Uncertainty. JOURNAL OF ARTIFICIAL INTELLIGENCE RESEARCH, 2025, vol. 2025, no. 82, p. 433-469. ISSN: 1076-9757. Detail

2024

  • ČEŠKA, M.; ANDRIUSHCHENKO, R.; ARND, H.; JUNGES, S.; KŘETÍNSKÝ, J. 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. p. 90-146. ISBN: 978-3-031-67694-9. Detail

2023

  • ANDRIUSHCHENKO, R.; ALEXANDER, B.; ČEŠKA, M.; JUNGES, S.; KATOEN, J.; MACÁK, F. 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). Cham: Springer Verlag, 2023. p. 113-135. ISBN: 978-3-031-37708-2. Detail
  • ANDRIUSHCHENKO, R.; BARTOCCI, E.; ČEŠKA, M.; FRANCESCO, P.; SARAH, S. 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). Cham: Springer Verlag, 2023. p. 288-306. ISBN: 978-3-031-43834-9. Detail
Nahoru