BRÁZDIL, Tomáš, Stefan KIEFER, Antonín KUČERA and 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, 2015, p. 44-55. ISBN 978-1-4799-8875-4. Available from: https://dx.doi.org/10.1109/LICS.2015.15.
Other formats:   BibTeX LaTeX RIS
Basic information
Original name Long-Run Average Behaviour of Probabilistic Vector Addition Systems
Authors BRÁZDIL, Tomáš (203 Czech Republic, belonging to the institution), Stefan KIEFER (276 Germany), Antonín KUČERA (203 Czech Republic, guarantor, belonging to the institution) and Petr NOVOTNÝ (203 Czech Republic, belonging to the institution).
Edition Neuveden, 30th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2015, Kyoto, Japan, July 6-10, 2015. p. 44-55, 12 pp. 2015.
Publisher IEEE
Other information
Original language English
Type of outcome Proceedings paper
Field of Study 10201 Computer sciences, information science, bioinformatics
Country of publisher United States of America
Confidentiality degree is not subject to a state or trade secret
Publication form printed version "print"
RIV identification code RIV/00216224:14330/15:00081425
Organization unit Faculty of Informatics
ISBN 978-1-4799-8875-4
ISSN 1043-6871
Doi http://dx.doi.org/10.1109/LICS.2015.15
UT WoS 000380427100007
Keywords in English Probabilistic Vector Addition Systems; Markov Chains
Tags core_A, firank_1, formela-conference
Tags International impact, Reviewed
Changed by Changed by: RNDr. Pavel Šmerk, Ph.D., učo 3880. Changed: 28/4/2016 15:35.
Abstract
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.
Links
GA15-17564S, research and development projectName: Teorie her jako prostředek pro formální analýzu a verifikaci počítačových systémů
Investor: Czech Science Foundation
MUNI/A/1159/2014, interní kód MUName: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace IV.
Investor: Masaryk University, Category A
PrintDisplayed: 6/5/2024 07:33