Parameter Synthesis in Continuous-Time Stochastic Systems - Korenčiak, Ľuboš (2018)
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