Extremal counter programming

The aim is to present a technical core of a recently obtained TOWER lower bound

for the reachability problem of Petri nets, model equivalent to vector addition systems with states

or to nondeterministic counter machines without zero tests.

Using an equivalent syntax of 'counter programs', I will present a program whose output value

is as large as the tower of exponentials of height equal to the size of the program.

This is a joint work with Wojtek Czerwiński, Ranko Lazic, Jerome Leroux and Filip Mazowiecki.