---
_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:10.1145/3209108.3209191'
apa: '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
(Vol. F138033, pp. 185–194). Presented at the LICS: Logic in Computer Science,
Oxford, United Kingdom: IEEE. https://doi.org/10.1145/3209108.3209191'
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. https://doi.org/10.1145/3209108.3209191.
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. Efficient Algorithms for Asymptotic Bounds on Termination
Time in VASS. Vol. F138033, IEEE, 2018, pp. 185–94, doi:10.1145/3209108.3209191.
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: 2023-09-11T13:23:42Z
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'
...