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.

Basic information

Original name

Zero-reachability in probabilistic multi-counter automata

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), Petr NOVOTNÝ (203 Czech Republic, belonging to the institution) and Joost-Pieter KATOEN (528 Netherlands)

Edition

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), p. nestránkováno, 10 pp. 2014

Publisher

ACM

Other information

Language

English

Type of outcome

Stať ve sborníku

Field of Study

10201 Computer sciences, information science, bioinformatics

Country of publisher

United States of America

Confidentiality degree

není předmětem státního či obchodního tajemství

Publication form

electronic version available online

References:

URL

RIV identification code

RIV/00216224:14330/14:00074099

Organization unit

Faculty of Informatics

ISBN

978-1-4503-2886-9

DOI

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

UT WoS

000693915100021

Keywords in English

markov chains; petri nets; reachability; multicounter automata

Tags

best1, core_A, firank_1, formela-conference

Tags

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

Abstract

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.

Links

GPP202/12/P612, research and development project
Name: Formální verifikace stochastických systémů s reálným časem (Acronym: Formální verifikace stochastických systémů s reáln)
Investor: Czech Science Foundation
MUNI/A/0765/2013, interní kód MU
Name: Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity (Acronym: SKOMU)
Investor: Masaryk University, Category A
MUNI/A/0855/2013, interní kód MU
Name: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace III. (Acronym: FI MAV III.)
Investor: Masaryk University, Category A
Displayed: 10/11/2024 20:31