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.