The INFINITY 2020 Programme

The hours are in CEST.

TimeSessionChair
10:00 — 10:10— Opening video
10:10 — 10:50Sławomir Lasota: Lower bound for VASS reachability in fixed dimension videoFilip Mazowiecki
10:50 — 11:30 Chana Weil-Kennedy: Branching Immediate Observation Petri nets: a strong class with simple reachability video
11:30 — 12:00— Break —
12:00 — 12:40 Patrick Totzke: 1-VASS languages, universality, pumping, open problems video
12:40 — 14:00 — Lunch Break —
14:00 — 14:40Guillermo A. Perez: Revisiting Synthesis for One-Counter Automata videoWojciech Czerwiński
14:40 — 15:20Blaise Genest: Controlling a population video
15:20 — 15:50— Break —
15:50 — 16:10Javier Esparza: Verifying qualitative liveness properties of replicated systems with stochastic scheduling video
16:10 — 16:30Alex Dixon: A Tool for Reachability in Petri Nets video
16:30 — 17:10Radosław Piórkowski: New geometrical approach to pumping in 2-dimensional VASS video
17:10 — 17:30— Break —
17:30 — 18:10— Open problems + ending videoFilip Mazowiecki

Abstracts and slides

Sławomir Lasota: Lower bound for VASS reachability in fixed dimension slides
The current best lower bound for the space/time complexity of the reachability problem in d-dimensional vector addition systems with states (d-VASS) 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 Weil-Kennedy: Branching Immediate Observation Petri nets: a strong class with simple reachability slides
Branching Immediate Observation (BIO) nets extend both BPP nets, also called communication-free 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 non-semilinear reachability relation but a reachability problem which is PSPACE-complete. This makes BIO nets the first natural net class with non-semilinear reachability relation for which the reachability problem is provably simpler than for general Petri nets.

Patrick Totzke: 1-VASS languages, universality, pumping, open problems slides
We study the language universality problem for One-Counter Nets, also known as 1-dimensional Vector Addition Systems with States (1-VASS), 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 Ackermann-complete 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 single-letter alphabet.

Guillermo A. Perez: Revisiting Synthesis for One-Counter Automata slides
One-counter automata are obtained by extending classical finite-state automata with a counter whose value can range over non-negative integers and be tested for zero. The updates and tests applicable to the counter can further be made parametric by introducing a set of integer-valued 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 omega-regular property. The problem has been shown to be encodable in a restricted one-alternation 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 polynomial-space 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 finite-state 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 non-deterministic finite state automaton (NFA), the same for every agent, and the whole system is encoded as a 2-player game. The first player (Controller) chooses actions, and the second player (Agents) resolves non-determinism for each agent. The game with m agents is called the m-population 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 m-population 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 cut-off 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 2-dimensional VASS slides
I will present a new pumping technique for 2-VASS building on natural geometric properties of runs. We expect it to be useful for settling questions concerning languages of 2-VASS, 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 2-VASS.