Zero-reachability in probabilistic multi-counter automata

D 2014

Zero-reachability in probabilistic multi-counter automata

BRÁZDIL, Tomáš, Stefan KIEFER, Antonín KUČERA, Petr NOVOTNÝ, Joost-Pieter KATOEN et. al.

Základní údaje

Originální název

Zero-reachability in probabilistic multi-counter automata

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í), Petr NOVOTNÝ (203 Česká republika, domácí) a Joost-Pieter KATOEN (528 Nizozemské království)

Vydání

New York, 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), od s. nestránkováno, 10 s. 2014

Nakladatel

ACM

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í

elektronická verze "online"

Odkazy

URL

Kód RIV

RIV/00216224:14330/14:00074099

Organizační jednotka

Fakulta informatiky

ISBN

978-1-4503-2886-9

DOI

http://dx.doi.org/10.1145/2603088.2603161

UT WoS

000693915100021

Klíčová slova anglicky

markov chains; petri nets; reachability; multicounter automata

Štítky

best1, core_A, firank_1, formela-conference

Příznaky

Mezinárodní význam, Recenzováno

Změněno: 16. 11. 2014 14:20, doc. RNDr. Petr Novotný, Ph.D.

Anotace

V originále

We study the qualitative and quantitative zero-reachability problem in probabilistic multi-counter systems. We identify the undecidable variants of the problems, and then we concentrate on the remaining two cases. In the first case, when we are interested in the probability of all runs that visit zero in some counter, we show that the qualitative zero-reachability is decidable in time which is polynomial in the size of a given pMC and doubly exponential in the number of counters. Further, we show that the probability of all zero-reaching runs can be effectively approximated up to an arbitrarily small given error epsilon > 0 in time which is polynomial in log(epsilon), exponential in the size of a given pMC, and doubly exponential in the number of counters. In the second case, we are interested in the probability of all runs that visit zero in some counter different from the last counter. Here we show that the qualitative zero-reachability is decidable and SquareRootSum-hard, and the probability of all zero-reaching runs can be effectively approximated up to an arbitrarily small given error epsilon > 0 (these result applies to pMC satisfying a suitable technical condition that can be verified in polynomial time). The proof techniques invented in the second case allow to construct counterexamples for some classical results about ergodicity in stochastic Petri nets.

Návaznosti

GPP202/12/P612, projekt VaV

Název: Formální verifikace stochastických systémů s reálným časem (Akronym: Formální verifikace stochastických systémů s reáln)

Investor: Grantová agentura ČR, Formální verifikace stochastických systémů s reálným časem

MUNI/A/0765/2013, interní kód MU

Název: Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity (Akronym: SKOMU)

Investor: Masarykova univerzita, Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity, DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty

MUNI/A/0855/2013, interní kód MU

Název: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace III. (Akronym: FI MAV III.)

Investor: Masarykova univerzita, Rozsáhlé výpočetní systémy: modely, aplikace a verifikace III., DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty

Citovat

BRÁZDIL, Tomáš, Stefan KIEFER, Antonín KUČERA, Petr NOVOTNÝ a Joost-Pieter KATOEN. Zero-reachability in probabilistic multi-counter automata. Online. In Thomas Henzinger and Dale Miller. 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). New York: ACM, 2014, s. nestránkováno, 10 s. ISBN 978-1-4503-2886-9. Dostupné z: https://dx.doi.org/10.1145/2603088.2603161.

@inproceedings{1206161,
   author = {Brázdil, Tomáš and Kiefer, Stefan and Kučera, Antonín and Novotný, Petr and Katoen, JoostandPieter},
   address = {New York},
   booktitle = {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)},
   doi = {http://dx.doi.org/10.1145/2603088.2603161},
   editor = {Thomas Henzinger and Dale Miller},
   keywords = {markov chains; petri nets; reachability; multicounter automata},
   howpublished = {elektronická verze "online"},
   language = {eng},
   location = {New York},
   isbn = {978-1-4503-2886-9},
   pages = {nestránkováno},
   publisher = {ACM},
   title = {Zero-reachability in probabilistic multi-counter automata},
   url = {http://arxiv.org/abs/1401.6840},
   year = {2014}
}

TY  - JOUR
ID  - 1206161
AU  - Brázdil, Tomáš - Kiefer, Stefan - Kučera, Antonín - Novotný, Petr - Katoen, Joost-Pieter
PY  - 2014
TI  - Zero-reachability in probabilistic multi-counter automata
PB  - ACM
CY  - New York
SN  - 9781450328869
KW  - markov chains
KW  - petri nets
KW  - reachability
KW  - multicounter automata
UR  - http://arxiv.org/abs/1401.6840
N2  - We study the qualitative and quantitative zero-reachability problem in probabilistic multi-counter systems. We identify the undecidable variants of the problems, and then we concentrate on the remaining two cases. In the first case, when we are interested in the probability of all runs that visit zero in some counter, we show that the qualitative zero-reachability is decidable in time which is polynomial in the size of a given pMC and doubly exponential in the number of counters. Further, we show that the probability of all zero-reaching runs can be effectively approximated up to an arbitrarily small given error epsilon > 0 in time which is polynomial in log(epsilon), exponential in the size of a given pMC, and doubly exponential in the number of counters. In the second case, we are interested in the probability of all runs that visit zero in some counter different from the last counter. Here we show that the qualitative zero-reachability is decidable and SquareRootSum-hard, and the probability of all zero-reaching runs can be effectively approximated up to an arbitrarily small given error epsilon > 0 (these result applies to pMC satisfying a suitable technical condition that can be verified in polynomial time). The proof techniques invented in the second case allow to construct counterexamples for some classical results about ergodicity in stochastic Petri nets.
ER  -

BRÁZDIL, Tomáš, Stefan KIEFER, Antonín KUČERA, Petr NOVOTNÝ a Joost-Pieter KATOEN. Zero-reachability in probabilistic multi-counter automata. Online. In Thomas Henzinger and Dale Miller. \textit{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)}. New York: ACM, 2014, s.~nestránkováno, 10 s. ISBN~978-1-4503-2886-9. Dostupné z: https://dx.doi.org/10.1145/2603088.2603161.

Podrobný výpis o publikaci