Project information
Teorie her jako prostředek pro formální analýzu a verifikaci počítačových systémů
- Project Identification
- GA15-17564S
- Project Period
- 1/2015 - 12/2017
- Investor / Pogramme / Project type
-
Czech Science Foundation
- Standard Projects
- MU Faculty or unit
- Faculty of Informatics
Projekt je orientován na rozvoj herně-teoretických metod pro formální analýzu a verifikaci interaktivních počítačových systémů. Chování takových systémů lze popsat v termínech teorie her jako hru dvou hráčů, systému a prostředí, kteří mají antagonistické cíle --- systém se snaží o splnění zadané verifikační podmínky, zatímco prostředí se snaží o opak. Tímto způsobem je možné problémy související s bezpečností, korektností a výkonem daného systému vyjádřit pomocí aparátu teorie her a využít příslušný teoretický aparát k jejich řešení.
Publications
Total number of publications: 17
2017
-
Mean-Payoff Optimization in Continuous-Time Markov Chains with Parametric Alarms
Quantitative Evaluation of Systems, year: 2017
-
Policy learning in continuous-time Markov decision processes using Gaussian Processes
Performance Evaluation, year: 2017, volume: 116, edition: 1, DOI
-
Symbiotic 4: Beyond Reachability (Competition Contribution)
Tools and Algorithms for the Construction and Analysis of Systems: 23rd International Conference, year: 2017
-
Synthesis of Optimal Resilient Control Strategies
Automated Technology for Verification and Analysis, year: 2017
-
Temporal logic control for stochastic linear systems using abstraction refinement of probabilistic games
Nonlinear Analysis: Hybrid Systems, year: 2017, volume: 23, edition: February 2017, DOI
-
Trading performance for stability in Markov decision processes
Journal of Computer and System Sciences, year: 2017, volume: 84, edition: 2017, DOI
2016
-
Efficient Timeout Synthesis in Fixed-Delay CTMC Using Policy Iteration
2016 IEEE 24th International Symposium on Modeling, Analysis and Simulation of Computer and Telecommunication Systems, year: 2016
-
MoChiBA: Probabilistic {LTL} Model Checking Using Limit-Deterministic Büchi Automata
Automated Technology for Verification and Analysis - 14th International Symposium, ATVA 2016, year: 2016
-
Policy Learning for Time-Bounded Reachability in Continuous-Time Markov Decision Processes via Doubly-Stochastic Gradient Ascent
Proceedings of QEST 2016, year: 2016
-
Regular Strategies and Strategy Improvement: Efficient Tools for Solving Large Patrolling Problems
Proceedings of the 2016 International Conference on Autonomous Agents & Multiagent Systems, year: 2016