Parameter Synthesis in Continuous-Time Stochastic Systems /
Markovove reťazce spojitého času (eng. continuous-time Markov chains, CTMC) sú atraktívny formalizmus na špecifikáciu a verifikáciu stochastických systémov, kde sa diskrétne udalosti odohrávajú v spojitom čase. Trieda CTMC je vhodná na testovanie výkonnosti týchto systémov pretože má Markovovu vlast...
Uloženo v:
| Hlavní autor: | |
|---|---|
| Další autoři: | |
| Typ dokumentu: | VŠ práce nebo rukopis |
| Jazyk: | Angličtina |
| Vydáno: |
2018
|
| Témata: | |
| On-line přístup: | http://is.muni.cz/th/zaes9/ |
| Shrnutí: | Markovove reťazce spojitého času (eng. continuous-time Markov chains, CTMC) sú atraktívny formalizmus na špecifikáciu a verifikáciu stochastických systémov, kde sa diskrétne udalosti odohrávajú v spojitom čase. Trieda CTMC je vhodná na testovanie výkonnosti týchto systémov pretože má Markovovu vlastnosť. Tá zjednodušuje analýzu, ale limituje modelovaciu silu, pretože implikuje, že všetky udalosti majú exponenciálne rozdelenie. Markovove reťazce spojitého času s budíkmi (eng. continuous-time Markov chains with alarms, ACTMC) umožňujú naviac modelovať budíkové udalosti. Tie môžu mať ľubovoľné rozdelenie času zvonenia za podmienky, že v každom momente je aktívny maximálne jeden budík. Uvažujeme parametrické ACTMC, kde (spojité) parametre budíkových rozdelení nie sú fixne dané a môžu byť syntetizované. Toto je veľmi užitočné napríklad na automatickú syntézu časových limitov v sieťových protokoloch. Predstavujeme dve množiny algoritmov na riešenie epsilon-optimálnej syntézy parametrov v pa Continuous-time Markov chains (CTMCs) is an attractive formalism for specification of stochastic systems where discrete events occur in continuous time. The class of CTMCs is suitable for performance evaluation thanks to the Markov property, which simplifies the analysis but limits the modeling power as it requires exponential distribution for all events. Continuous-time Markov chains with alarms (ACTMCs) additionally allow for alarm events that have generally distributed delays, given that at most one alarm is active at any time. We consider parametric ACTMCs where the (continuous) parameters of alarm-delay distributions are not given explicitly and can be subjects of parameter synthesis. This is very useful in practice, e.g., to automatically synthesize timeouts in network protocols. We present two sets of algorithms solving the epsilon-optimal parameter synthesis problem for parametric ACTMCs with total accumulated reward or long-run average optimization objectives. All algorithms |
|---|---|
| Popis jednotky: | Vedoucí práce: Antonín Kučera |
| Fyzický popis: | ix, 143 stran |