Project information
Formální verifikace stochastických systémů s reálným časem
(Formální verifikace stochastických systémů s reáln)
- Project Identification
- GPP202/12/P612
- Project Period
- 1/2012 - 12/2014
- Investor / Pogramme / Project type
-
Czech Science Foundation
- Postdoctoral projects
- MU Faculty or unit
- Faculty of Informatics
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.
Publications
Total number of publications: 10
2014
-
Dealing with Zero Density Using Piecewise Phase-Type Approximation
Computer Performance Engineering, year: 2014
-
Markov Decision Processes with Multiple Long-Run Average Objectives
Logical Methods in Computer Science, year: 2014, volume: 10, edition: 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), year: 2014
2013
-
On time-average limits in deterministic and stochastic Petri nets
ACM/SPEC International Conference on Performance Engineering, ICPE'13, year: 2013
-
Solvency Markov Decision Processes with Interest
IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2013), year: 2013
-
Trading Performance for Stability in Markov Decision Processes
Proceedings of 28th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2013), year: 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, year: 2012
-
Minimizing Expected Termination Time in One-Counter Markov Decision Processes
Proceedings of 39th International Colloquium on Automata, Languages and Programming (ICALP 2012), year: 2012
-
Sequence Chart Studio
2012 12th International Conference on Application of Concurrency to System Design, year: 2012
-
Verification of Open Interactive Markov Chains
IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2012), year: 2012