Checking and Classifying Fast Termination in VASS

Vector Addition Systems with States (VASS) consists of a finite state machine equipped with d positive integer-valued counters, where in each transition every counter is incremented, decremented, or left unchanged. In this talk, I will present our results on automated synthesis of tight polynomial asymptotic bounds on termination time of VASS. I will present key proof ideas behind our results as well as some follow-up work.

Joint work with T. Brázdil, K. Chatterjee, A. Kučera, and D. Velan.
https://arxiv.org/abs/1708.09253