Long-Run Average Behaviour of Probabilistic Vector Addition
Systems

D 2015

Long-Run Average Behaviour of Probabilistic Vector Addition Systems

BRÁZDIL, Tomáš, Stefan KIEFER, Antonín KUČERA a Petr NOVOTNÝ

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

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

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ěněno: 28. 4. 2016 15:35, RNDr. Pavel Šmerk, Ph.D.

Anotace

V originále

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 VaV

Ná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 MU

Ná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

Citovat

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, 2015, s. 44-55. ISBN 978-1-4799-8875-4. Dostupné z: https://dx.doi.org/10.1109/LICS.2015.15.

@inproceedings{1323104,
   author = {Brázdil, Tomáš and Kiefer, Stefan and Kučera, Antonín and Novotný, Petr},
   address = {Neuveden},
   booktitle = {30th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2015, Kyoto, Japan, July 6-10, 2015.},
   doi = {http://dx.doi.org/10.1109/LICS.2015.15},
   editor = {Neuveden},
   keywords = {Probabilistic Vector Addition Systems; Markov Chains},
   howpublished = {tištěná verze "print"},
   language = {eng},
   location = {Neuveden},
   isbn = {978-1-4799-8875-4},
   pages = {44-55},
   publisher = {IEEE},
   title = {Long-Run Average Behaviour of Probabilistic Vector Addition Systems},
   year = {2015}
}

TY  - JOUR
ID  - 1323104
AU  - Brázdil, Tomáš - Kiefer, Stefan - Kučera, Antonín - Novotný, Petr
PY  - 2015
TI  - Long-Run Average Behaviour of Probabilistic Vector Addition Systems
PB  - IEEE
CY  - Neuveden
SN  - 9781479988754
KW  - Probabilistic Vector Addition Systems
KW  - Markov Chains
N2  - 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.
ER  -

BRÁZDIL, Tomáš, Stefan KIEFER, Antonín KUČERA a Petr NOVOTNÝ. Long-Run Average Behaviour of Probabilistic Vector Addition Systems. In Neuveden. \textit{30th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2015, Kyoto, Japan, July 6-10, 2015.}. Neuveden: IEEE, 2015, s.~44-55. ISBN~978-1-4799-8875-4. Dostupné z: https://dx.doi.org/10.1109/LICS.2015.15.

Podrobný výpis o publikaci