Informace o projektu
Formální verifikace stochastických systémů s reálným časem
(Formální verifikace stochastických systémů s reáln)
- Kód projektu
- GPP202/12/P612
- Období řešení
- 1/2012 - 12/2014
- Investor / Programový rámec / typ projektu
-
Grantová agentura ČR
- Postdoktorské projekty
- Fakulta / Pracoviště MU
- Fakulta informatiky
Předmětem našeho výzkumu je formální verifikace systémů, které vykazují náhodné chování a zároveň musí splňovat různá časová omezení (stochastic real-time systems, SRTS). Náhodné aspekty systémů se obvykle modelují pomocí stochastických procesů. Systémy pracující v reálném čase jsou typicky modelovány pomocí časových automatů. Abychom byli schopni modelovat SRTS, musíme tyto formalismy vhodně spojit. Koncentrujeme se zejména na strukturální vlastnosti takových systémů a výpočetní složitost základních verifikačních problémů. Další obvyklou vlastností reálných systémů je nedeterminismus, tedy nejistota v chování bez jakékoliv statistické znalosti. Nedeterminismus se také objevuje v problémech, v nichž je třeba syntetizovat řídící jednotku systému. SRTS s nedeterminismem lze modelovat pomocí rozhodovacích procesů se spojitým časem, jejichž cílové podmínky lze vyjádřit pomocí časových automatů. V této oblasti se zabýváme zejména existencí řídící jednotky, která splňuje cílovou podmínku a zároveň ji lze algoritmicky konstruovat.
Publikace
Počet publikací: 10
2014
-
Dealing with Zero Density Using Piecewise Phase-Type Approximation
Computer Performance Engineering, rok: 2014
-
Markov Decision Processes with Multiple Long-Run Average Objectives
Logical Methods in Computer Science, rok: 2014, ročník: 10, vydání: 1, DOI
-
Zero-reachability in probabilistic multi-counter automata
Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), rok: 2014
2013
-
On time-average limits in deterministic and stochastic Petri nets
ACM/SPEC International Conference on Performance Engineering, ICPE'13, rok: 2013
-
Solvency Markov Decision Processes with Interest
IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2013), rok: 2013
-
Trading Performance for Stability in Markov Decision Processes
Proceedings of 28th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2013), rok: 2013
2012
-
LTL to Büchi Automata Translation: Fast and More Deterministic
TACAS 2012: 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, rok: 2012
-
Minimizing Expected Termination Time in One-Counter Markov Decision Processes
Proceedings of 39th International Colloquium on Automata, Languages and Programming (ICALP 2012), rok: 2012
-
Sequence Chart Studio
2012 12th International Conference on Application of Concurrency to System Design, rok: 2012
-
Verification of Open Interactive Markov Chains
IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2012), rok: 2012