Hi all,

For our third meeting, we will discuss the attached paper and I'll host the discussion.

The meeting will take place in Room 349 on Monday, November 27th at noon.

Mini-intro: This is a classic paper of Petri net theory. Petri nets — or the equivalent model of VASS — are a popular model of concurrency with a number of applications in database theory, business processes, and more (see e.g. surveys below). One of the central decision problems for Petri nets is the coverability problem, that asks whether there is a run from a given initial configuration to some configuration with at least the counter values of a given target configuration. Coverability is useful in the verification of safety conditions. The paper I will present is Rackoff’s 1978 result that coverability is in EXPSPACE, proved by showing that if coverability holds then there exists a run of double-exponential length.

Petri net surveys: https://dl.acm.org/doi/10.1145/2893582.2893585 https://dl.acm.org/doi/10.1145/2893582.2893585 https://link.springer.com/content/pdf/10.1007/3-540-65306-6_20.pdf https://link.springer.com/content/pdf/10.1007/3-540-65306-6_20.pdf

See you,

Chana