BRÁZDIL, Tomáš, Krishnendu CHATTERJEE, Antonín KUČERA, Petr NOVOTNÝ, Dominik VELAN a Florian ZULEGER. Efficient Algorithms for Asymptotic Bounds on Termination Time in VASS. In Anuj Dawar, Erich Gradel. 2018 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). Oxford, England: ACM, 2018. s. 185-194, 10 s. ISBN 978-1-4503-5583-4. doi:10.1145/3209108.3209191.
Další formáty:   BibTeX LaTeX RIS
Základní údaje
Originální název Efficient Algorithms for Asymptotic Bounds on Termination Time in VASS
Autoři BRÁZDIL, Tomáš (203 Česká republika, domácí), Krishnendu CHATTERJEE (356 Indie), Antonín KUČERA (203 Česká republika, domácí), Petr NOVOTNÝ (203 Česká republika), Dominik VELAN (203 Česká republika, garant, domácí) a Florian ZULEGER (40 Rakousko).
Vydání Oxford, England, 2018 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), od s. 185-194, 10 s. 2018.
Nakladatel ACM
Další údaje
Originální jazyk angličtina
Typ výsledku Stať ve sborníku
Obor 1.2 Computer and information sciences
Stát vydavatele Spojené království
Utajení není předmětem státního či obchodního tajemství
Forma vydání tištěná verze "print"
WWW ACM Digital Library
Kód RIV RIV/00216224:14330/18:00100882
Organizační jednotka Fakulta informatiky
ISBN 978-1-4503-5583-4
ISSN 1043-6871
Doi http://dx.doi.org/10.1145/3209108.3209191
Klíčová slova anglicky vector addition systems with states; termination
Štítky firank_1
Příznaky Mezinárodní význam, Recenzováno
Změnil Změnil: RNDr. Pavel Šmerk, Ph.D., učo 3880. Změněno: 30. 4. 2019 04:27.
Anotace
Vector Addition Systems with States (VASS) provide a well-known and fundamental model for the analysis of concurrent processes, parametrized 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 Theta(n^k), for some integer k\leq 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 Omega(n^k). Our results are based on new insights into the geometry of VASS dynamics, which hold the potential for further applicability to VASS analysis.
Anotace česky
V článku je studován problém asymptotického odhadu maximální délky výpočtu daného VASS systému.
Návaznosti
GA18-11193S, projekt VaVNázev: Algoritmy pro diskrétní systémy a hry s nekonečně mnoha stavy
Investor: Grantová agentura ČR, Standardní projekty
MUNI/A/0854/2017, interní kód MUNázev: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace VII.
Investor: Masarykova univerzita, Grantová agentura MU, Kategorie A - Specifický výzkum - Studentské výzkumné projekty
MUNI/A/1038/2017, interní kód MUNázev: Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity 18
Investor: Masarykova univerzita, Grantová agentura MU, Kategorie A - Specifický výzkum - Studentské výzkumné projekty
VytisknoutZobrazeno: 17. 10. 2019 12:37