---
_id: '143'
abstract:
- lang: eng
  text: 'Vector Addition Systems with States (VASS) provide a well-known and fundamental
    model for the analysis of concurrent processes, parameterized systems, and are
    also used as abstract models of programs in resource bound analysis. In this paper
    we study the problem of obtaining asymptotic bounds on the termination time of
    a given VASS. In particular, we focus on the practically important case of obtaining
    polynomial bounds on termination time. Our main contributions are as follows:
    First, we present a polynomial-time algorithm for deciding whether a given VASS
    has a linear asymptotic complexity. We also show that if the complexity of a VASS
    is not linear, it is at least quadratic. Second, we classify VASS according to
    quantitative properties of their cycles. We show that certain singularities in
    these properties are the key reason for non-polynomial asymptotic complexity of
    VASS. In absence of singularities, we show that the asymptotic complexity is always
    polynomial and of the form Θ(nk), for some integer k d, where d is the dimension
    of the VASS. We present a polynomial-time algorithm computing the optimal k. For
    general VASS, the same algorithm, which is based on a complete technique for the
    construction of ranking functions in VASS, produces a valid lower bound, i.e.,
    a k such that the termination complexity is (nk). Our results are based on new
    insights into the geometry of VASS dynamics, which hold the potential for further
    applicability to VASS analysis.'
alternative_title:
- ACM/IEEE Symposium on Logic in Computer Science
article_processing_charge: No
author:
- first_name: Tomáš
  full_name: Brázdil, Tomáš
  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: Kučera, Antonín
  last_name: Kučera
- first_name: Petr
  full_name: Novotny, Petr
  id: 3CC3B868-F248-11E8-B48F-1D18A9856A87
  last_name: Novotny
- first_name: Dominik
  full_name: Velan, Dominik
  last_name: Velan
- first_name: Florian
  full_name: Zuleger, Florian
  last_name: Zuleger
citation:
  ama: 'Brázdil T, Chatterjee K, Kučera A, Novotný P, Velan D, Zuleger F. Efficient
    algorithms for asymptotic bounds on termination time in VASS. In: Vol F138033.
    IEEE; 2018:185-194. doi:<a href="https://doi.org/10.1145/3209108.3209191">10.1145/3209108.3209191</a>'
  apa: 'Brázdil, T., Chatterjee, K., Kučera, A., Novotný, P., Velan, D., &#38; Zuleger,
    F. (2018). Efficient algorithms for asymptotic bounds on termination time in VASS
    (Vol. F138033, pp. 185–194). Presented at the LICS: Logic in Computer Science,
    Oxford, United Kingdom: IEEE. <a href="https://doi.org/10.1145/3209108.3209191">https://doi.org/10.1145/3209108.3209191</a>'
  chicago: Brázdil, Tomáš, Krishnendu Chatterjee, Antonín Kučera, Petr Novotný, Dominik
    Velan, and Florian Zuleger. “Efficient Algorithms for Asymptotic Bounds on Termination
    Time in VASS,” F138033:185–94. IEEE, 2018. <a href="https://doi.org/10.1145/3209108.3209191">https://doi.org/10.1145/3209108.3209191</a>.
  ieee: 'T. Brázdil, K. Chatterjee, A. Kučera, P. Novotný, D. Velan, and F. Zuleger,
    “Efficient algorithms for asymptotic bounds on termination time in VASS,” presented
    at the LICS: Logic in Computer Science, Oxford, United Kingdom, 2018, vol. F138033,
    pp. 185–194.'
  ista: 'Brázdil T, Chatterjee K, Kučera A, Novotný P, Velan D, Zuleger F. 2018. Efficient
    algorithms for asymptotic bounds on termination time in VASS. LICS: Logic in Computer
    Science, ACM/IEEE Symposium on Logic in Computer Science, vol. F138033, 185–194.'
  mla: Brázdil, Tomáš, et al. <i>Efficient Algorithms for Asymptotic Bounds on Termination
    Time in VASS</i>. Vol. F138033, IEEE, 2018, pp. 185–94, doi:<a href="https://doi.org/10.1145/3209108.3209191">10.1145/3209108.3209191</a>.
  short: T. Brázdil, K. Chatterjee, A. Kučera, P. Novotný, D. Velan, F. Zuleger, in:,
    IEEE, 2018, pp. 185–194.
conference:
  end_date: 2018-07-12
  location: Oxford, United Kingdom
  name: 'LICS: Logic in Computer Science'
  start_date: 2018-07-09
date_created: 2018-12-11T11:44:51Z
date_published: 2018-07-09T00:00:00Z
date_updated: 2025-06-02T08:53:48Z
day: '09'
department:
- _id: KrCh
doi: 10.1145/3209108.3209191
ec_funded: 1
external_id:
  isi:
  - '000545262800020'
isi: 1
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: https://arxiv.org/abs/1804.10985
month: '07'
oa: 1
oa_version: Preprint
page: 185 - 194
project:
- _id: 25892FC0-B435-11E9-9278-68D0E5697425
  grant_number: ICT15-003
  name: Efficient Algorithms for Computer Aided Verification
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '279307'
  name: 'Quantitative Graph Games: Theory and Applications'
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: S 11407_N23
  name: Rigorous Systems Engineering
publication_identifier:
  isbn:
  - 978-1-4503-5583-4
publication_status: published
publisher: IEEE
publist_id: '7780'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Efficient algorithms for asymptotic bounds on termination time in VASS
type: conference
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
volume: F138033
year: '2018'
...