Moje meno: Michal Adámek
Moja e-mailová adresa: michal.adamek1@gmail.com
Meno vedúceho ročníkového projektu: RNDr. Michal Forišek PhD.
E-mailová adresa vedúceho ročníkového projektu: forisek@dcs.fmph.uniba.sk
Názov ročníkového projektu: Implementácia algoritmu na zistenie dosiahnuteľnosti nuly v stochastickom systéme s počítadlami
Špecifikácia ročníkového projektu:
Stochastický systém s počítadlami rozmeru d, kde d ≥ 1, sa skladá z konečne-stavovej kontrolnej jednotky a d neohraničených počítadiel, ktoré môžu uchovávať nezáporné celé čísla. Konfigurácia stochastického systému s počítadlami pv je daná súčasným kontrolným stavom p a vektorom súčasných hodnôt počítadiel v. Prechod v stochastickom systéme s počítadlami je určený konečnou množinou pravidiel tvaru (p, α, q), kde p je súčasný kontrolný stav, q je ďalší kontrolný stav a α je d-rozmerný vektor zmien hodnôt počítadiel rozsahu nad {-1, 0, 1}d. Každé pravidlo má priradenú kladnú celočíselnú váhu. Pravidlo (p, α, q) je povolené v konfigurácií pv ak žiadna zložka vektora v + α nie je záporná. Použíté pravidlo (p, α, q) v konfigurácií pv vytvára stochastický prechod pvq(v + α) s pravdepodobnosťou x, ktorá je rovná podielu váhy tohto pravidla a súčtu váh všetkých pravidiel povolených v pv. Konfigurácie a stochastické prechody medzi nimi tvoria Markovov reťazec. Cieľ ročníkového projektu je implementovať algoritmus na zistenie, či hodnota niektorého počítadla bude 0 v niektorej konfigurácií v Markovovom reťazci, a zistiť ako dlho algoritmus počíta s náhodne vytvorenými stochastickými systémami s počítadlami.
Odkaz na článok s algoritmom na zistenie dosiahnuteľnosti nuly v stochastickom systéme s počítadlami: Zero-Reachability in Probabilistic Multi-Counter Automata
Časový harmonogram ročníkového projektu:
Zimný semester:
- naprogramovať algoritmus na zistenie pokrytelnosti jednej konfigurácie z inej konfigurácie v systéme s počítadlami
Letný semester:
- naprogramovať algoritmus na zistenie dosiahnutelnosti nuly v stochastickom systéme s počítadlami
Vyhodnotenie ročníkového projektu:
Implementoval som algoritmus na zistenie dosiahnuteľnosti nuly v stochastickom systéme s počítadlami v programovacom jazyku Java. Program má vykonávať algoritmus na 60 náhodne vytvorených systémoch. Program pri testovaní počítal dlho už na systéme rozmeru 2, a nevykonal algoritmus na všetkých vytvorených systémoch, pretože skončil kvôli problému s pamäťou.
Literatúra:
  1. BRÁZDIL, Tomáš, Stefan KIEFER, Antonín KUČERA, Petr NOVOTNÝ a Joost-Pieter KATOEN. Zero-reachability in probabilistic multi-counter automata. In: 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) - CSL-LICS ’14 [online]. New York, New York, USA: ACM Press, 2014, 2014, s. 1-10 [cit. 2018-01-10]. DOI: 10.1145/2603088.2603161. ISBN 9781450328869. Dostupné z: http://dl.acm.org/citation.cfm?doid=2603088.2603161
  2. BOZZELLI, Laura a Pierre GANTY. Complexity Analysis of the Backward Coverability Algorithm for VASS. DELZANNO, Giorgio a Igor POTAPOV, ed. Reachability Problems [online]. Berlin, Heidelberg: Springer Berlin Heidelberg, 2011, 2011, s. 96-109 [cit. 2018-01-10]. Lecture Notes in Computer Science. DOI: 10.1007/978-3-642-24288-5_10. ISBN 978-3-642-24287-8. Dostupné z: http://link.springer.com/10.1007/978-3-642-24288-5_10

Pseudokód algoritmu na zistenie dosiahnuteľnosti nuly v stochastickom systéme s počítadlami
Pseudokód algoritmu na zistenie pokrytelnosti jednej konfigurácie z inej konfigurácie v systéme s počítadlami
Zdrojový kód algoritmu na zistenie dosiahnuteľnosti nuly v stochastickom systéme s počítadlami