2017, Kunal Mittal’s internship

The theory of well-structured transition systems (WSTS) allows the automatic verification of safety properties of infinite-state systems, such that parts of reachability sets can be finitely
represented. Termination, boundedness and coverability are decidable for WSTS. The objectives were the following:

1. to analyse the proof of the decidability of boundedness for VASS with resets;

2. to simplify the proofs and build a Karp and Miller procedure;

3. to analyse the downward closed sets in Zn.

Kunal understood and completed the short and incompletely developed proof by Petr Jancar on the decidability of boundedness for 2-Reset Petri Nets (Catherine Dufourd, Petr Jancar, Philippe Schnoebelen: Boundedness of Reset P/T Nets. ICALP 1999: 301-310).

He also understood the construction of a coverability tree for the decidability of place-boundedness for 2-Reset Petri Nets.