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)
Dacík Tomáš, 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, doc. Ing., Ph.D. (UPSY)
Nesvedová Šárka (DFIT-EO)
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)
Publikační výsledky

2025

  • ANDRIUSHCHENKO, R.; ČEŠKA, M.; CHAKRABORTY, D.; JUNGES, S.; KRETINSKY, J.; MACÁK, F. Symbiotic Local Search for Small Decision Tree Policies in MDPs. In Proceedings of the Forty-first Conference on Uncertainty in Artificial Intelligence. Proceedings of Machine Learning Research. ML Research Press, 2025. p. 132-142. Detail
  • ANDRIUSHCHENKO, R.; ČEŠKA, M.; JUNGES, S.; MACÁK, F. Small Decision Trees for MDPs with Deductive Synthesis. In Computer Aided Verification. Springer Cham, 2025. p. 169-192. ISBN: 978-3-031-98678-9. Detail
  • ANDRIUSHCHENKO, R.; ČEŠKA, M.; MACÁK, F.; FRANCESCO, P.; MICHELE, C. Decentralized Planning Using Probabilistic Hyperproperties. In Proc. of the 24th International Conference on Autonomous Agents and Multiagent Systems. Detroit: 2025. p. 1688-1697. ISBN: 979-8-4007-1426-9. Detail
  • ANDRIUSHCHENKO, R.; ČEŠKA, M.; MACÁK, F.; JUNGES, S. Policies Grow on Trees: Model Checking Families of MDPs. In Proceeding of 22nd International Symposium on Automated Technology for Verification and Analysis. Cham: Springer Verlag, 2025. p. 51-75. ISBN: 978-3-031-78749-2. Detail
  • GALESLOOT, M.; ANDRIUSHCHENKO, R.; ČEŠKA, M.; JUNGES, S.; JANSEN, N. Robust Finite-Memory Policy Gradients for Hidden-Model POMDPs. In Proceedings of the Thirty-Fourth International Joint Conference on Artificial Intelligence. International Joint Conferences on Artificial Intelligence Organization, 2025. p. 8518-8526. ISBN: 978-1-956792-06-5. Detail
  • MACÁK, F.; ANDRIUSHCHENKO, R.; ČEŠKA, M.; JUNGES, S.; KATOEN, J. An Oracle-Guided Approach to Constrained Policy Synthesis Under Uncertainty. The journal of artificial intelligence research, 2025, vol. 2025, iss. 82, p. 433-469. 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