Verification of concurrent systems is a difficult task, and often becomes undecidable. In order to allow for certain verification procedures, many computational models for concurrent systems are available, which admit various computational properties.One Counter Nets, also known as 1-dimensional Vector Addition Systems, are a fairly restrictive model, and as such admits several decidable verification problems. In this talk, I will survey some of the relevant computational models, and present some results on universality problems for One Counter Nets, as well as interesting tools that arise in studying them. No prior knowledge is assumed, posterior knowledge is guaranteed.
Shaull Almagor is an assistant professor of Computer Science at the Technion, and a Marie-Curie Fellow. His research focuses on theoretical aspects of automata, and in particular infinite state machines, such as dynamical systems and weighted automata.