---
_id: '7183'
abstract:
- lang: eng
  text: 'A probabilistic vector addition system with states (pVASS) is a finite state
    Markov process augmented with non-negative integer counters that can be incremented
    or decremented during each state transition, blocking any behaviour that would
    cause a counter to decrease below zero. The pVASS can be used as abstractions
    of probabilistic programs with many decidable properties. The use of pVASS as
    abstractions requires the presence of nondeterminism in the model. In this paper,
    we develop techniques for checking fast termination of pVASS with nondeterminism.
    That is, for every initial configuration of size n, we consider the worst expected
    number of transitions needed to reach a configuration with some counter negative
    (the expected termination time). We show that the problem whether the asymptotic
    expected termination time is linear is decidable in polynomial time for a certain
    natural class of pVASS with nondeterminism. Furthermore, we show the following
    dichotomy: if the asymptotic expected termination time is not linear, then it
    is at least quadratic, i.e., in Ω(n2).'
alternative_title:
- LNCS
article_processing_charge: No
arxiv: 1
author:
- first_name: Tomás
  full_name: Brázdil, Tomás
  last_name: Brázdil
- first_name: Krishnendu
  full_name: Chatterjee, Krishnendu
  id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
  last_name: Chatterjee
  orcid: 0000-0002-4561-241X
- first_name: Antonín
  full_name: Kucera, Antonín
  last_name: Kucera
- first_name: Petr
  full_name: Novotný, Petr
  id: 3CC3B868-F248-11E8-B48F-1D18A9856A87
  last_name: Novotný
- first_name: Dominik
  full_name: Velan, Dominik
  last_name: Velan
citation:
  ama: 'Brázdil T, Chatterjee K, Kucera A, Novotný P, Velan D. Deciding fast termination
    for probabilistic VASS with nondeterminism. In: <i>International Symposium on
    Automated Technology for Verification and Analysis</i>. Vol 11781. Springer Nature;
    2019:462-478. doi:<a href="https://doi.org/10.1007/978-3-030-31784-3_27">10.1007/978-3-030-31784-3_27</a>'
  apa: 'Brázdil, T., Chatterjee, K., Kucera, A., Novotný, P., &#38; Velan, D. (2019).
    Deciding fast termination for probabilistic VASS with nondeterminism. In <i>International
    Symposium on Automated Technology for Verification and Analysis</i> (Vol. 11781,
    pp. 462–478). Taipei, Taiwan: Springer Nature. <a href="https://doi.org/10.1007/978-3-030-31784-3_27">https://doi.org/10.1007/978-3-030-31784-3_27</a>'
  chicago: Brázdil, Tomás, Krishnendu Chatterjee, Antonín Kucera, Petr Novotný, and
    Dominik Velan. “Deciding Fast Termination for Probabilistic VASS with Nondeterminism.”
    In <i>International Symposium on Automated Technology for Verification and Analysis</i>,
    11781:462–78. Springer Nature, 2019. <a href="https://doi.org/10.1007/978-3-030-31784-3_27">https://doi.org/10.1007/978-3-030-31784-3_27</a>.
  ieee: T. Brázdil, K. Chatterjee, A. Kucera, P. Novotný, and D. Velan, “Deciding
    fast termination for probabilistic VASS with nondeterminism,” in <i>International
    Symposium on Automated Technology for Verification and Analysis</i>, Taipei, Taiwan,
    2019, vol. 11781, pp. 462–478.
  ista: 'Brázdil T, Chatterjee K, Kucera A, Novotný P, Velan D. 2019. Deciding fast
    termination for probabilistic VASS with nondeterminism. International Symposium
    on Automated Technology for Verification and Analysis. ATVA: Automated TEchnology
    for Verification and Analysis, LNCS, vol. 11781, 462–478.'
  mla: Brázdil, Tomás, et al. “Deciding Fast Termination for Probabilistic VASS with
    Nondeterminism.” <i>International Symposium on Automated Technology for Verification
    and Analysis</i>, vol. 11781, Springer Nature, 2019, pp. 462–78, doi:<a href="https://doi.org/10.1007/978-3-030-31784-3_27">10.1007/978-3-030-31784-3_27</a>.
  short: T. Brázdil, K. Chatterjee, A. Kucera, P. Novotný, D. Velan, in:, International
    Symposium on Automated Technology for Verification and Analysis, Springer Nature,
    2019, pp. 462–478.
conference:
  end_date: 2019-10-31
  location: Taipei, Taiwan
  name: 'ATVA: Automated TEchnology for Verification and Analysis'
  start_date: 2019-10-28
date_created: 2019-12-15T23:00:44Z
date_published: 2019-10-21T00:00:00Z
date_updated: 2023-09-06T12:40:58Z
day: '21'
department:
- _id: KrCh
doi: 10.1007/978-3-030-31784-3_27
external_id:
  arxiv:
  - '1907.11010'
  isi:
  - '000723515700027'
intvolume: '     11781'
isi: 1
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: https://arxiv.org/abs/1907.11010
month: '10'
oa: 1
oa_version: Preprint
page: 462-478
project:
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: S 11407_N23
  name: Rigorous Systems Engineering
publication: International Symposium on Automated Technology for Verification and
  Analysis
publication_identifier:
  eissn:
  - '16113349'
  isbn:
  - '9783030317836'
  issn:
  - '03029743'
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: Deciding fast termination for probabilistic VASS with nondeterminism
type: conference
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
volume: 11781
year: '2019'
...