The INFINITY 2020 Programme  
The hours are in CEST.
Abstracts and slidesSławomir Lasota: Lower bound for VASS reachability in fixed dimension slidesThe current best lower bound for the space/time complexity of the reachability problem in ddimensional vector addition systems with states (dVASS) is expressed by a tower of exponentials of height O(d). This result underlies the recent TOWER lower bound for the reachability problem in unrestricted dimension. We will discuss an improvement of the construction yielding a slightly better lower bound: a tower of exponentials of height exponential in O(d). Chana WeilKennedy: Branching Immediate Observation Petri nets: a strong class with simple reachability slides Branching Immediate Observation (BIO) nets extend both BPP nets, also called communicationfree nets, and Immediate Observation nets, a class we studied for its applications to population protocols and chemical reaction networks. We show that BIO nets have a nonsemilinear reachability relation but a reachability problem which is PSPACEcomplete. This makes BIO nets the first natural net class with nonsemilinear reachability relation for which the reachability problem is provably simpler than for general Petri nets. Patrick Totzke: 1VASS languages, universality, pumping, open problems slides We study the language universality problem for OneCounter Nets, also known as 1dimensional Vector Addition Systems with States (1VASS), parameterized either with an initial counter value, or with an upper bound on the allowed counter value during runs. The language accepted by an OCN (defined by reaching a final control state) is monotone in both parameters. This yields two natural questions: 1) Does there exist an initial counter value that makes the language universal? 2) Does there exist a sufficiently high ceiling so that the bounded language is universal? Despite the fact that unparameterized universality is Ackermanncomplete and that these problems seem to reduce to checking basic structural properties of the underlying automaton, we show that in fact both problems are undecidable. We also look into the complexities of the problems for several decidable subclasses, namely for unambiguous, and deterministic systems, and for those over a singleletter alphabet. Guillermo A. Perez: Revisiting Synthesis for OneCounter Automata slides Onecounter automata are obtained by extending classical finitestate automata with a counter whose value can range over nonnegative integers and be tested for zero. The updates and tests applicable to the counter can further be made parametric by introducing a set of integervalued variables. We revisit the parameter synthesis problem for such automata. That is, we ask whether there exists a valuation of the parameters such that all infinite runs of the automaton satisfy some omegaregular property. The problem has been shown to be encodable in a restricted onealternation fragment of Presburger arithmetic with divisibility. In this work (i) we argue that said fragment of the logic is unfortunately undecidable. Nevertheless, by reduction to a class of partial observation games, (ii) we prove the synthesis problem is decidable. Finally, (iii) we give a polynomialspace algorithm for the problem if parameters can only be used in tests, and not updates, of the counter. Blaise Genest: Controlling a population slides We introduce a new setting where a population of agents, each modelled by a finitestate system, are controlled uniformly: the controller applies the same action to every agent. The framework is largely inspired by the control of a biological system, namely a population of yeasts, where the controller may only change the environment common to all cells. We study a synchronisation problem for such populations: no matter how individual agents react to the actions of the controller, the controller aims at driving all agents synchronously to a target state. The agents are naturally represented by a nondeterministic finite state automaton (NFA), the same for every agent, and the whole system is encoded as a 2player game. The first player (Controller) chooses actions, and the second player (Agents) resolves nondeterminism for each agent. The game with m agents is called the mpopulation game. This gives rise to a parameterized control problem (where control refers to 2 player games), namely the population control problem: can Controller control the mpopulation game for all m ∈ N whatever Agents does? In this talk, we prove that the population control problem is decidable. As far as we know, this is one of the first results on the control of parameterized systems. Our algorithm, which is not based on cutoff techniques, produces winning strategies which are symbolic, that is, they do not need to count precisely how the population is spread between states. The winning strategies produced by our algorithm are optimal with respect to the synchronisation time: the maximal number of steps before synchronisation of all agents in the target state is at most polynomial in the number of agents m, and exponential in the size of the NFA. Javier Esparza: Verifying qualitative liveness properties of replicated systems with stochastic scheduling slides I present stage graphs, a sound and complete proof technique for replicated systems modeled with VASS, and sketch a practical algorithm for computing them. Alex Dixon: A Tool for Reachability in Petri Nets slides Kosaraju’s algorithm for reachability in Vector Addition Systems is well known, with many advances made in recent years. We introduce KReach, an implementation of Kosaraju’s original reachability algorithm. KReach is, as far as we know, the first implementation of its kind. We can also verify safety properties using KReach by reduction from the coverability problem to reachability. Surprisingly, KReach performs competitively against, or outperforms, coverability solvers on safe instances. Radosław Piórkowski: New geometrical approach to pumping in 2dimensional VASS slides I will present a new pumping technique for 2VASS building on natural geometric properties of runs. We expect it to be useful for settling questions concerning languages of 2VASS, e.g., for establishing decidability status of the regular separability problem. I will show how one may apply it to reprove an exponential bound on the length of the shortest accepting run, and to prove a new pumping lemma for languages of 2VASS. 

