BRÁZDIL, Tomáš, Stefan KIEFER, Antonín KUČERA a Petr NOVOTNÝ. Long-Run Average Behaviour of Probabilistic Vector Addition Systems. In Neuveden. 30th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2015, Kyoto, Japan, July 6-10, 2015. Neuveden: IEEE. s. 44-55. ISBN 978-1-4799-8875-4. doi:10.1109/LICS.2015.15. 2015.
Další formáty:   BibTeX LaTeX RIS
Základní údaje
Originální název Long-Run Average Behaviour of Probabilistic Vector Addition Systems
Autoři BRÁZDIL, Tomáš (203 Česká republika, domácí), Stefan KIEFER (276 Německo), Antonín KUČERA (203 Česká republika, garant, domácí) a Petr NOVOTNÝ (203 Česká republika, domácí).
Vydání Neuveden, 30th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2015, Kyoto, Japan, July 6-10, 2015. od s. 44-55, 12 s. 2015.
Nakladatel IEEE
Další údaje
Originální jazyk angličtina
Typ výsledku Stať ve sborníku
Obor 10201 Computer sciences, information science, bioinformatics
Stát vydavatele Spojené státy
Utajení není předmětem státního či obchodního tajemství
Forma vydání tištěná verze "print"
Kód RIV RIV/00216224:14330/15:00081425
Organizační jednotka Fakulta informatiky
ISBN 978-1-4799-8875-4
ISSN 1043-6871
Doi http://dx.doi.org/10.1109/LICS.2015.15
UT WoS 000380427100007
Klíčová slova anglicky Probabilistic Vector Addition Systems; Markov Chains
Štítky core_A, firank_1, formela-conference
Příznaky Mezinárodní význam, Recenzováno
Změnil Změnil: RNDr. Pavel Šmerk, Ph.D., učo 3880. Změněno: 28. 4. 2016 15:35.
Anotace
We study the pattern frequency vector for runs in probabilistic Vector Addition Systems with States (pVASS). Intuitively, each configuration of a given pVASS is assigned one of finitely many \emph{patterns}, and every run can thus be seen as an infinite sequence of these patterns. The pattern frequency vector assigns to each run the limit of pattern frequencies computed for longer and longer prefixes of the run. If the limit does not exist, then the vector is undefined. We show that for one-counter pVASS, the pattern frequency vector is defined and takes one of finitely many values for almost all runs. Further, these values and their associated probabilities can be approximated up to an arbitrarily small relative error in polynomial time. For stable two-counter pVASS, we show the same result, but we do not provide any upper complexity bound. As a byproduct of our study, we discover counterexamples falsifying some classical results about stochastic Petri nets published in the 80s.
Návaznosti
GA15-17564S, projekt VaVNázev: Teorie her jako prostředek pro formální analýzu a verifikaci počítačových systémů
Investor: Grantová agentura ČR, Teorie her jako prostředek pro formální analýzu a verifikaci počítačových systémů
MUNI/A/1159/2014, interní kód MUNázev: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace IV.
Investor: Masarykova univerzita, Rozsáhlé výpočetní systémy: modely, aplikace a verifikace IV., DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty
VytisknoutZobrazeno: 18. 4. 2024 12:26