Dominik Velan

dblp:205/2648 · DBLP profile ↗
← Back
3ranked-venue papers
0as first author
0since 2021 · last 2020
—ORCID · none

Domains — the database's venue-derived domains; a paper can count in several

Theory of computation · 2Software engineering, systems software and programming languages · 1

Expertise — from the expertise taxonomy: the topics of the expert's papers under the CCF categories. A weight counts papers with recency: 1 for a paper about the topic, 0.3 when the topic is its context, halved every five years.

Theoretical computer science
2 papers
Automata and formal languages · 58% Computational complexity · 35% Logic in computer science · 8%

Topics — the 3 heaviest of 4, each with the papers that count most for it

TopicWeightPapersLastEvidence papers
Automata and formal languages › petri nets
vector addition systems
0.822020
Efficient Analysis of VASS Termination Complexity · LICS 2020
Efficient Algorithms for Asymptotic Bounds on Termination Time in VASS · LICS 2018
Computational complexity › computability theory
grzegorczyk hierarchy
0.112020
Efficient Analysis of VASS Termination Complexity · LICS 2020
Logic in computer science › program analysis
ranking functions
0.112018
Efficient Algorithms for Asymptotic Bounds on Termination Time in VASS · LICS 2018

Methods — techniques the papers use, named apart from their topics

complexity analysis · 0.4ranking function construction · 0.3cycle analysis · 0.3
YearPublicationVenuePosition
2020 Efficient Analysis of VASS Termination Complexity
abstract
The termination complexity of a given VASS is a function L assigning to every n the length of the longest non-terminating computation initiated in a configuration with all counters bounded by n. We show that for every VASS with demonic nondeterminism and every fixed k, the problem whether L ϵ Gk, where Gk is the k-th level in the Grzegorczyk hierarchy, is decidable in polynomial time. Furthermore, we show that if L ϵ G, then L grows at least as fast as the generator Fk+1 of Gk+1. Hence, for every terminating VASS, the growth of L can be reasonably characterized by the least k such that L ϵ Gk.
Antonín Kucera 0001, Jérôme Leroux, Dominik Velan
LICS3
2019 Deciding Fast Termination for Probabilistic VASS with Nondeterminism
Tomás Brázdil, Krishnendu Chatterjee, Antonín Kucera 0001, Petr Novotný 0001, Dominik Velan
ATVA5
2018 Efficient Algorithms for Asymptotic Bounds on Termination Time in VASS
abstract
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.
Tomás Brázdil, Krishnendu Chatterjee, Antonín Kucera 0001, Petr Novotný 0001, Dominik Velan, Florian Zuleger
LICS5